[#15017] perf: move every rarely-updated Core.Context field into the cold subobject

[downstream-lean4]

This is the adaptation PR for leanprover/lean4#15017.

[Kha]

!bench mathlib

[leanprover-radar]

Benchmark results for 284926b against dfa0830 are in. There are significant results. @Kha

• ✅ build//instructions: -1.2T (-0.82%)

Large changes (1✅)

• 1 hidden

Medium changes (1✅)

• ✅ build/module/Mathlib.Geometry.Convex.ConvexSpace.Module//instructions: -1.1G (-1.80%)

Small changes (323✅)

• ✅ build/module/Aesop.Builder.Forward//instructions: -84.7M (-1.65%)
• ✅ build/module/Aesop.BuiltinRules.DestructProducts//instructions: -33.4M (-1.11%)
• ✅ build/module/Aesop.BuiltinRules.Subst//instructions: -25.0M (-0.95%)
• ✅ build/module/Aesop.EMap//instructions: -32.7M (-1.06%)
• ✅ build/module/Aesop.Forward.Match//instructions: -77.4M (-1.49%)
• ✅ build/module/Aesop.Forward.State.ApplyGoalDiff//instructions: -20.6M (-1.03%)
• ✅ build/module/Aesop.Forward.State//instructions: -337.1M (-1.69%)
• ✅ build/module/Aesop.Frontend.Command//instructions: -53.1M (-1.12%)
• ✅ build/module/Aesop.Frontend.Extension//instructions: -31.8M (-1.17%)
• ✅ build/module/Aesop.Frontend.RuleExpr//instructions: -149.3M (-1.73%)
• ✅ build/module/Aesop.Frontend.Saturate//instructions: -41.9M (-1.06%)
• ✅ build/module/Aesop.Frontend.Tactic//instructions: -62.9M (-1.51%)
• ✅ build/module/Aesop.Index.RulePattern//instructions: -34.3M (-1.13%)
• ✅ build/module/Aesop.Index//instructions: -51.4M (-1.15%)
• ✅ build/module/Aesop.Main//instructions: -40.7M (-1.11%)
• ✅ build/module/Aesop.RulePattern//instructions: -67.1M (-1.30%)
• ✅ build/module/Aesop.RuleSet//instructions: -201.2M (-1.72%)
• ✅ build/module/Aesop.RuleTac.Apply//instructions: -25.5M (-1.14%)
• ✅ build/module/Aesop.RuleTac.Forward//instructions: -94.3M (-1.55%)
• ✅ build/module/Aesop.RuleTac.GoalDiff//instructions: -50.8M (-1.35%)
• and 303 more

[downstream-lean4]

Build report for downstream: follow upstream PR

Stayed green

Repo	Critical	Build	Test	Lint
aesop	✅	✅ in 17s	✅ in 5s	⏭️
batteries	✅	✅ in 14s	✅ in 4s	✅ in 2s
import-graph	✅	✅ in 3s	✅ in 3s	⏭️
lean4-cli	✅	✅ in 3s	✅ in 0s	⏭️
mathlib4	✅	✅ in 1157s	✅ in 46s	✅ in 90s
plausible	✅	✅ in 3s	✅ in 2s	⏭️
ProofWidgets4	✅	✅ in 5s	✅ in 1s	⏭️
quote4	✅	✅ in 6s	✅ in 1s	⏭️
reference-manual	✅	✅ in 77s	⏭️	⏭️
BibtexQuery		✅ in 3s	⏭️	⏭️
comparator		✅ in 3s	⏭️	⏭️
cslib		✅ in 35s	✅ in 8s	✅ in 3s
doc-gen4		✅ in 15s	⏭️	⏭️
illuminate		✅ in 8s	✅ in 10s	⏭️
lean4-unicode-basic		✅ in 4s	⏭️	⏭️
lean4export		✅ in 3s	✅ in 7s	⏭️
LeanSearchClient		✅ in 2s	✅ in 0s	⏭️
leansqlite		✅ in 9s	✅ in 15s	⏭️
repl		✅ in 4s	✅ in 57s	⏭️
verso		✅ in 127s	✅ in 84s	⏭️
verso-slides		✅ in 18s	✅ in 6s	⏭️
verso-web-components		✅ in 34s	⏭️	⏭️

View run

[downstream-lean4]

The upstream PR has landed. This adaptation PR is being closed because it has no changes.