perf: cache elaboration of section variables across commands - #14595
Closed
marcelolynch wants to merge 2 commits into
Closed
perf: cache elaboration of section variables across commands#14595marcelolynch wants to merge 2 commits into
marcelolynch wants to merge 2 commits into
Conversation
marcelolynch
force-pushed
the
sectionvars-cache-pr
branch
from
July 29, 2026 15:54
03fd3bc to
dc65ebd
Compare
Contributor
Author
|
!bench mathlib |
|
Benchmark results for leanprover-community/mathlib4-nightly-testing@1bd09a6 against leanprover-community/mathlib4-nightly-testing@51fd0ce are in. There are significant results. @marcelolynch
Large changes (2✅)
Medium changes (11✅, 1🟥)
Small changes (62✅)
|
github-actions
Bot
added
toolchain-available
leanprover-bot
added
the
builds-manual
Collaborator
|
Reference manual CI status:
|
mathlib-lean-pr-testing
Bot
added
the
builds-mathlib
|
Mathlib CI status (docs):
|
marcelolynch
force-pushed
the
sectionvars-cache-pr
branch
from
July 29, 2026 19:23
dc65ebd to
c393a43
Compare
Contributor
Author
|
!bench mathlib |
|
Benchmark results for leanprover-community/mathlib4-nightly-testing@1bd09a6 against leanprover-community/mathlib4-nightly-testing@51fd0ce are in. (These commits have already been benchmarked in a previous command.) There are significant results. @marcelolynch
Large changes (2✅)
Medium changes (11✅, 1🟥)
Small changes (62✅)
|
Contributor
Author
|
!bench mathlib |
|
Benchmark results for leanprover-community/mathlib4-nightly-testing@1bd09a6 against leanprover-community/mathlib4-nightly-testing@51fd0ce are in. (These commits have already been benchmarked in a previous command.) There are significant results. @marcelolynch
Large changes (2✅)
Medium changes (11✅, 1🟥)
Small changes (62✅)
|
marcelolynch
force-pushed
the
sectionvars-cache-pr
branch
2 times, most recently
from
August 31, 2026 20:23
0cbb9f9 to
407548a
Compare
Contributor
Author
|
!bench mathlib |
|
Benchmark results for leanprover-community/mathlib4-nightly-testing@1bd09a6 against leanprover-community/mathlib4-nightly-testing@51fd0ce are in. (These commits have already been benchmarked in a previous command.) There are significant results. @marcelolynch
Large changes (5✅)
Medium changes (37✅, 1🟥)
Small changes (116✅, 109🟥)
|
Contributor
Author
|
!bench |
|
Benchmark results for 407548a against c8e19cc are in. There are significant results. @marcelolynch
Large changes (2✅)
Medium changes (13✅)
Small changes (42✅, 54🟥)
|
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
A reuse of the cached section variables reopens the telescope, which makes new free variables. The language server finds the binder of a free variable through its info node, so the reuse path adds a binder info node for each new free variable. It takes the binder syntax from `Term.elabBindersEx` and adds the nodes with `Term.addLocalVarInfo`, as `MutualDef` does after it reopens the telescope of a declaration. Without the nodes, go-to-definition, document highlight and find-references stop working on the section variables. The cache key also holds the revision of the default instance table. `attribute [default_instance]` changes the synthesis that runs inside the binder types without a change of the instance table, so the key alone could keep a stale elaboration. A scope without section variables skips the cache. Such a scope has nothing to reuse, and the work of the cache costs more than the elaboration of the empty block. The cache also stores a negative outcome. A block whose elaboration a telescope cannot reproduce, for example a block that auto-binds a universe name, built and discarded a telescope for every command of the scope. The cache now records the outcome once, and the later commands elaborate the binders without that work. The cache takes one field of the command state. A named `SectionVarsCacheKey` holds the scope and the two revisions, and both the stored entry and the last miss use it, after the `SynthInstanceCacheKey` convention. The number of section variables bounds the reopened telescope. Add tests for the type-class synthesis that finds a section-variable instance on the reuse path, the binder annotations, the erasure of an instance, the auto-bound implicit blocks, the temporary scope of a `set_option ... in` prefix, and the invalidation by a default instance. Add a server test for go-to-definition and document highlight on a section variable. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
marcelolynch
force-pushed
the
sectionvars-cache-pr
branch
from
August 31, 2026 23:24
407548a to
9c4b01e
Compare
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Aug 31, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Aug 31, 2026
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 caches the elaboration of section variables. Before this change,
runTermElabMelaborated the binders of everyvariablecommand in scope for each command. The elaboration of a binder type can run type-class synthesis, and every command of a section repeats that work. In long Mathlib sections, this cost reaches 20–30% of the instructions of a module (see the analysis in the discussion of leanprover-community/mathlib4#42214, which removes dead binders for this reason; live binders pay the same cost).The cache holds the binders of the current scope as a closed telescope in the command state. A command reuses the telescope when the cache key agrees. The key holds the scope, the revision of the instance table and the revision of the default instance table, and
Meta.InstancesandMeta.DefaultInstanceseach get arevisioncounter for it. The key compares scopes by pointer identity, so any change of the scope gives a different key. Each reuse makes fresh level metavariables, so every command constrains the universes of the section variables on its own. The cache does not take a block when the elaboration auto-binds an implicit variable or a universe name, leaves a metavariable or a postponed universe constraint, or containssorry. The reuse path repeats the universe checkpoint and the recursion depth of the elaboration path.A reuse reopens the telescope, which makes new free variables. The language server finds the binder of a free variable through its info node, so
runTermElabMadds a binder info node for each new free variable. It takes the binder syntax fromTerm.elabBindersExand adds the nodes withTerm.addLocalVarInfo.MutualDefuses the same pattern after it reopens the telescope of a declaration. Without the nodes, go-to-definition, document highlight and find-references stop working on the section variables.A scope without section variables skips the cache, because it has nothing to reuse and the work of the cache costs more than the elaboration of the empty block. The cache also stores a negative outcome. A block whose elaboration a telescope cannot reproduce, for example a block that auto-binds a universe name with
Type*, built and discarded a telescope for every command of the scope. The cache records the outcome once, and the later commands of the scope elaborate the binders without that work.The cache is an approximation, not an exact replay. It tracks the changes of the environment that can change the result of the type-class synthesis in the binder types, and it does not track the other changes. A new instance or a new default instance therefore invalidates the cache. A declaration that shadows a name in a binder type does not invalidate it, and a change of reducibility does not either. The visible consequence is the resolution of identifiers: with the cache, a declaration between two commands of a scope does not change how the identifiers in the binder types of earlier
variablecommands resolve. Set the optionElab.cacheSectionVarstofalsefor the old behavior.This criterion needs a decision from the reviewers. No document states when the binder types of a
variablecommand resolve, and the present behavior follows from the storage of the binders as syntax. Thevariablecommand discussion on Zulip lists the current behavior as a defect, because the variables "elaborate to different expressions in different declarations", and it proposes a cache as one remedy. The cache removes that difference for identifiers and keeps it for instances. A full freeze is the other coherent option: it drops both revision counters and is simpler and faster, but it also stops a later instance from reaching an earlier binder, which is more likely to affect real code.Validation: a differential run of all 3097 files in
tests/elabwith the option on and off converged to no behavioral differences. The remaining diffs are environmental (timings, backtrace addresses, random bytes, pointer values, task interleavings), one metavariable index in an error message (the test driver strips these), and the documented resolution change. The differential run also found the need for three of the guards above, which shows the method works. A microbenchmark (80 trivial theorems under 20 instance binders) drops from 0.17s to 0.08s, against a 0.07s floor without binders. No test of the suite depends on the old resolution behavior. A!benchrun of an earlier revision measured -0.34% of the instructions of the build, with -10.45% forStd.Data.DHashMap.Lemmasand similar gains for the otherStd.Datalemma modules. The same run showed small regressions for modules without section variables, and the two paragraphs above remove that cost.tests/elab/sectionVarsCache.leandocuments the invariants and the resolution change. It also covers the type-class synthesis that finds a section-variable instance on the reuse path, the binder annotations that survive the telescope, the addition and the erasure of an instance, the invalidation by a default instance, the blocks that the cache does not take, and the temporary scope of aset_option ... inprefix.tests/server_interactive/sectionVarsCacheInfo.leanchecks go-to-definition and document highlight on a section variable in a command that reuses the cache.This is a draft to run the Mathlib benchmarks through a
lean-pr-testingtoolchain and measure the real-world gain.🤖 Generated with Claude Code