perf: split Core.Context into hot and cold subobjects

[Kha]

-0.5% instrs, -1.3/1.8% wall-clock core/Mathlib

withReader can never reuse the Context record as the caller is owning a reference, so every withRef, withOptions or withIncRecDepth pays one reference count increment per pointer field. Grouping these fields into a subobject makes them cost a single increment together.

[Kha]

!bench

[Kha]

!bench mathlib

[leanprover-radar]

Benchmark results for b76d5ba against e991a05 are in. There are significant results. @Kha

• ✅ build//instructions: -61.2G (-0.53%)

Large changes (20✅, 4🟥)

• 🟥 compiled/deriv//instructions: +21.4M (+0.32%)
• 🟥 compiled/rbmap_checkpoint//instructions: +5.0G (+39.58%)
• 🟥 compiled/rbmap_checkpoint//task-clock: +754ms (+51.80%)
• 🟥 compiled/rbmap_checkpoint//wall-clock: +781ms (+53.40%)
• ✅ elab/big_beq//maxrss: -38MiB (-2.11%)
• ✅ elab/big_beq_rec//maxrss: -38MiB (-2.08%)
• ✅ elab/big_deceq//maxrss: -37MiB (-2.10%)
• ✅ elab/big_deceq_rec//maxrss: -37MiB (-2.08%)
• ✅ elab/big_match//maxrss: -38MiB (-2.12%)
• ✅ elab/big_match_nat//maxrss: -39MiB (-2.20%)
• ✅ elab/delayed_lift//maxrss: -38MiB (-2.08%)
• ✅ elab/delayed_sharing//maxrss: -39MiB (-2.19%)
• ✅ elab/let_to_have_closed_body//maxrss: -38MiB (-2.13%)
• ✅ elab/lift_lets_binders//maxrss: -38MiB (-2.10%)
• ✅ elab/lift_lets_chain//maxrss: -39MiB (-2.17%)
• ✅ elab/lift_lets_dag//maxrss: -38MiB (-2.14%)
• ✅ elab/lift_lets_parallel//maxrss: -38MiB (-2.16%)
• ✅ elab/lift_lets_spine//maxrss: -39MiB (-2.18%)
• ✅ elab/string_simp_ne//maxrss: -39MiB (-2.11%)
• ✅ elab/sym_let_to_have_chain//maxrss: -38MiB (-2.07%)
• and 4 more

Medium changes (17✅, 1🟥)

• ✅ build/profile/elaboration//wall-clock: -11s (-5.18%)
• ✅ build/profile/simp//wall-clock: -10s (-7.83%)
• ✅ build/profile/typeclass inference//wall-clock: -6s (-4.99%)
• 🟥 compiled/const_fold//instructions: +533.3M (+7.39%)
• ✅ compiled/const_fold//maxrss: -2MiB (-0.16%)
• ✅ compiled/rbmap_checkpoint//maxrss: -3MiB (-0.10%)
• ✅ elab/big_do//instructions: -77.0M (-0.42%)
• ✅ elab/big_match_nat_split//maxrss: -40MiB (-2.19%)
• ✅ elab/big_match_partial//maxrss: -34MiB (-1.86%)
• ✅ elab/cbv_divisors//maxrss: -37MiB (-2.07%)
• ✅ elab/cbv_merge_sort//maxrss: -40MiB (-2.19%)
• ✅ elab/delayed_assign//maxrss: -39MiB (-2.15%)
• ✅ elab/grind_bitvec2//task-clock: -8s (-22.89%)
• ✅ elab/let_to_have_chain//maxrss: -38MiB (-2.12%)
• ✅ elab/let_to_have_nested//maxrss: -41MiB (-2.27%)
• ✅ elab/mut_rec_wf//maxrss: -39MiB (-2.09%)
• ✅ elab/sym_let_to_have_closed_body//maxrss: -37MiB (-1.67%)
• ✅ misc/re-elab Init.Data.BitVec.Lemmas//task-clock: -7s (-5.06%)

Small changes (566✅, 3🟥)

• ✅ build//task-clock: -55s (-2.65%)
• ✅ build/module/Init.BinderPredicates//instructions: -14.7M (-0.69%)
• ✅ build/module/Init.Control.Basic//instructions: -15.9M (-0.73%)
• ✅ build/module/Init.Control.Except//instructions: -9.4M (-0.66%)
• ✅ build/module/Init.Control.Lawful.Basic//instructions: -12.6M (-0.59%)
• ✅ build/module/Init.Control.Lawful.Instances//instructions: -50.0M (-0.74%)
• ✅ build/module/Init.Conv//instructions: -22.4M (-0.60%)
• ✅ build/module/Init.Core//instructions: -71.9M (-0.72%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Array.Attach//instructions: -81.4M (-0.79%)
• ✅ build/module/Init.Data.Array.Basic//instructions: -77.5M (-0.71%)
• ✅ build/module/Init.Data.Array.Erase//instructions: -50.1M (-0.70%)
• ✅ build/module/Init.Data.Array.Extract//instructions: -151.7M (-0.45%)
• ✅ build/module/Init.Data.Array.Find//instructions: -80.8M (-0.83%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Array.Lemmas//instructions: -390.4M (-0.74%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Array.Lex.Lemmas//instructions: -75.8M (-0.79%)
• ✅ build/module/Init.Data.Array.MapIdx//instructions: -63.8M (-0.73%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Array.Monadic//instructions: -52.9M (-0.87%)
• ✅ build/module/Init.Data.Array.QSort.Basic//instructions: -61.7M (-0.61%)
• ✅ build/module/Init.Data.Array.Range//instructions: -26.8M (-0.67%)
• ✅ build/module/Init.Data.Array.Sort.Lemmas//instructions: -13.9M (-0.44%)
• and 548 more
• and 1 hidden

[leanprover-radar]

Benchmark results for leanprover-community/mathlib4-nightly-testing@be38686 against leanprover-community/mathlib4-nightly-testing@78f2465 are in. There are significant results. @Kha

• ✅ build//instructions: -728.7G (-0.50%)

Large changes (1✅)

• 1 hidden

Small changes (80✅)

• ✅ build/module/Aesop.Builder.Forward//instructions: -34.2M (-0.66%)
• ✅ build/module/Aesop.Forward.Match//instructions: -43.3M (-0.82%)
• ✅ build/module/Aesop.Frontend.Command//instructions: -39.6M (-0.82%)
• ✅ build/module/Aesop.Frontend.RuleExpr//instructions: -80.8M (-0.92%)
• ✅ build/module/Aesop.Frontend.Tactic//instructions: -32.3M (-0.76%)
• ✅ build/module/Aesop.RuleTac.Forward//instructions: -44.8M (-0.72%)
• ✅ build/module/Aesop.Saturate//instructions: -95.1M (-0.68%)
• ✅ build/module/Aesop.Script.SpecificTactics//instructions: -79.3M (-0.92%)
• ✅ build/module/Aesop.Script.StructureDynamic//instructions: -40.6M (-0.76%)
• ✅ build/module/Aesop.Search.Expansion.Norm//instructions: -82.6M (-0.67%)
• ✅ build/module/Aesop.Search.Main//instructions: -64.3M (-0.69%)
• ✅ build/module/Aesop.Tree.Check//instructions: -40.5M (-0.81%)
• ✅ build/module/Aesop.Tree.ExtractProof//instructions: -30.1M (-0.77%)
• ✅ build/module/Aesop.Tree.ExtractScript//instructions: -41.3M (-0.74%)
• ✅ build/module/Aesop.Tree.Tracing//instructions: -30.7M (-0.61%)
• ✅ build/module/Aesop.Util.Basic//instructions: -63.8M (-0.81%)
• ✅ build/module/Aesop.Util.EqualUpToIds//instructions: -80.7M (-0.89%)
• ✅ build/module/Batteries.CodeAction.Misc//instructions: -54.2M (-0.69%)
• ✅ build/module/Batteries.Control.LawfulMonadState//instructions: -35.6M (-0.85%)
• ✅ build/module/Batteries.Data.Array.Scan//instructions: -71.7M (-0.72%)
• and 60 more

[leanprover-bot]

Reference manual CI status:

• ✅ Reference manual branch lean-pr-testing-14962 has successfully built against this PR. (2026-08-29 10:28:03) View Log
• 🟡 Reference manual branch lean-pr-testing-14962 build against this PR didn't complete normally. (2026-08-29 10:29:25) View Log

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-14962 has successfully built against this PR. (2026-08-29 11:17:12) View Log