perf: move more rarely-updated Core.Context field into the cold subobject - #15017
Merged
Conversation
Member
Author
|
!bench |
|
Benchmark results for a05f18d against 5877442 are in. There are significant results. @Kha
Medium changes (2✅)
Small changes (305✅, 4🟥)
|
github-actions
Bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
leanprover-bot
added
the
builds-manual
Collaborator
|
Reference manual CI status:
|
Kha
added
the
downstream-force
Kha
marked this pull request as ready for review
September 4, 2026 12:55
Kha
changed the title
Core.Context field into the cold subobjectCore.Context field into the cold subobject
…bobject This PR cuts the reference count traffic paid by the recursion-depth and `withRef` steps that dominate elaboration, from ten increments per reconstruction to three. Measured against master it saves between 0.35% and 1.24% of elaboration instructions across match-, simp- and grind-heavy workloads. `withReader` can never reuse the `Context` record, so every reconstruction pays one increment per pointer field. The original split classified fields by their number of update *sites*; this classifies them by measured update *frequency* instead. On a representative module `withIncRecDepth` runs about 1.0M times and `withRef` about 31k, while `withOptions` runs once, so `options`, `maxRecDepth`, `currNamespace`, `openDecls`, `initHeartbeats`, `maxHeartbeats` and `currMacroScope` join the cold group and only `currRecDepth` and `ref` stay hot. The `Context` constructor goes from `(0, 10, 2)` to `(0, 3, 2)`. Rebuilding the wider cold record does make the rare paths that update those fields more expensive: `withCurrHeartbeats` goes from ten increments to fourteen. At roughly 4.9k such calls against 1.05M reconstructions, the trade is strongly positive. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Kha
force-pushed
the
core-context-cold-wide
branch
from
September 4, 2026 13:28
a05f18d to
82db66b
Compare
Kha
enabled auto-merge
September 4, 2026 13:28
leanprover-bot
added a commit
to leanprover/reference-manual
that referenced
this pull request
Sep 4, 2026
|
The adaptation PR for this PR is leanprover/downstream-lean4#43. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR further cuts the reference count traffic paid by the recursion-depth and
withRefsteps that dominate elaboration, from ten increments per reconstruction to three. mathlib4 -0.82% instructions/-1.73% task-clock/-2.03% wall-clock.