perf: normalize free variables in the type class resolution cache key - #14369
Draft
Kha wants to merge 22 commits into
Draft
perf: normalize free variables in the type class resolution cache key#14369Kha wants to merge 22 commits into
Kha wants to merge 22 commits into
Conversation
Member
Author
|
!bench mathlib |
|
Benchmark results for leanprover-community/mathlib4-nightly-testing@ea9d208 against leanprover-community/mathlib4-nightly-testing@5edfd4c are in. There are significant results. @Kha
Large changes (79✅, 1🟥) Too many entries to display here. View the full report on radar instead. Medium changes (497✅, 1🟥) Too many entries to display here. View the full report on radar instead. Small changes (1199✅, 2🟥) Too many entries to display here. View the full report on radar instead. |
github-actions
Bot
added
toolchain-available
leanprover-bot
added
the
breaks-manual
Collaborator
|
Reference manual CI status:
|
mathlib-lean-pr-testing
Bot
added
the
breaks-mathlib
|
Mathlib CI status (docs):
|
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Jul 12, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Jul 12, 2026
leanprover-bot
added a commit
to leanprover/reference-manual
that referenced
this pull request
Jul 12, 2026
Member
Author
|
!bench |
|
Benchmark results for edd7f81 against 8006bb0 are in. There are significant results. @Kha Warning These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.
Large changes (8✅)
Medium changes (53✅)
Small changes (943✅, 9🟥)
|
Kha
removed
the
mathlib4-nightly-available
Member
Author
|
!bench mathlib |
|
Benchmark results for leanprover-community/mathlib4-nightly-testing@d166862 against leanprover-community/mathlib4-nightly-testing@5edfd4c are in. There are significant results. @Kha
Large changes (74✅, 1🟥)
Medium changes (448✅, 1🟥)
Small changes (1173✅, 2🟥)
|
Member
Author
|
!bench |
|
Benchmark results for 72a4b51 against 8006bb0 are in. There are significant results. @Kha Warning These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.
Large changes (11✅)
Medium changes (68✅, 3🟥)
Small changes (1022✅, 11🟥)
|
Member
Author
|
!bench mathlib |
|
Benchmark results for leanprover-community/mathlib4-nightly-testing@d166862 against leanprover-community/mathlib4-nightly-testing@5edfd4c are in. (These commits have already been benchmarked in a previous command.) There are significant results. @Kha
Large changes (74✅, 1🟥)
Medium changes (448✅, 1🟥)
Small changes (1173✅, 2🟥)
|
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Jul 23, 2026
github-actions
Bot
added
the
mathlib4-nightly-available
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Jul 23, 2026
leanprover-bot
added a commit
to leanprover/reference-manual
that referenced
this pull request
Jul 23, 2026
Member
Author
|
!bench mathlib |
|
Benchmark results for leanprover-community/mathlib4-nightly-testing@c8c70aa against leanprover-community/mathlib4-nightly-testing@5edfd4c are in. There are significant results. @Kha
No significant changes detected. |
Member
Author
|
!bench mathlib |
|
Benchmark results for leanprover-community/mathlib4-nightly-testing@c8c70aa against leanprover-community/mathlib4-nightly-testing@5edfd4c are in. (These commits have already been benchmarked in a previous command.) There are significant results. @Kha
No significant changes detected. |
Member
Author
|
!bench mathlib |
|
Benchmark results for 7bfafa9 against 2065c90 are in. There are significant results. @Kha
Large changes (7✅)
Medium changes (46✅)
Small changes (908✅, 68🟥)
|
|
The original message no longer contains a command. You can edit the original message until the command succeeds. |
|
The adaptation PR for this PR is leanprover/downstream-lean4#15. |
Kha
force-pushed
the
push-umqqwtmwmmyx
branch
8 times, most recently
from
July 31, 2026 18:21
9c96d51 to
22d7140
Compare
leanprover-bot
added a commit
to leanprover/reference-manual
that referenced
this pull request
Aug 9, 2026
leanprover-bot
added
builds-manual
This PR makes type class resolution cache entries depend on the options they observed: a query records every result-relevant option lookup (`Lean.getRecordedOption`), and an entry is served only while its recorded lookups give the same answers, so options no longer have to invalidate the cache wholesale (nor silently fail to). Options resolved once per query, such as the definitional-equality compatibility flags and the resource limits, are part of the cache key instead. Acquiring the options plainly is what a running query forbids: `getOptions` panics while `Core.Context.recordingDeps` is set, so nothing can go unrecorded. Type class resolution is a closed system, so the few readers whose result cannot influence a cached entry acquire them through the new `MonadOptions.getOptionsUnrestricted`, each carrying its one-line argument (trace and profiler collection, message rendering, diagnostics counters, and limits whose excess throws and is never cached). The marker is scoped to the computation rather than carried by the options value or the environment, both of which outlive the query in contexts captured for later rendering. The reachable set was measured rather than estimated: over the full `tests/elab` pile a recording query acquires the options 4.3M times from 17 source sites, all of them either audited unrestricted readers or the cache machinery itself. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…lution cache entries This PR makes type class resolution cache entries depend on the environment state they observed, completing the dependency tracking begun with option accesses. Extensions the search consults are classified at registration: generation-tracked extensions (instances, unification hints) are read through recording accessors that log the observed generation, and covered extensions hold declaration-keyed content whose observable changes are enforced by the write machinery rather than trusted. A read of an unclassified extension during a query panics, and `tests/elab/tc_cache_covered_claims.lean` locks that audit. Declaration-keyed writes are guarded for value stability, and a write some recording query could have observed is appended to a change log validated by constant birth ordering: the environment assigns each constant a per-lineage birth index as it becomes observable, so a change whose target was born after an entry was recorded cannot have affected it. Reducibility attribute changes are the most common such write. `debug.synthInstance.checkCacheHits` additionally re-runs served cache hits from scratch and compares, as a differential soak check. The recording marker gains a second home on the environment (`Environment.isRecordingDeps`) alongside the scoped `Core.Context.recordingDeps` introduced with option recording. Extension reads are pure functions of an environment, with no monad to consult, so this is the only marker they can see; the two are armed together and a captured display context (messages, pretty printing) clears the environment one at the boundary. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
… commands Cache entries whose key contains no metavariables and whose value is closed (no free variables or abstracted metavariables in key or value) are additionally stored in a persistent tier that survives the current command, so identical queries in later commands are served from the cache instead of re-searched. The recorded dependencies introduced in the previous PR replace whole-cache invalidation entirely: an entry from an earlier command is only served while its recorded option lookups, extension generations, and reducibility statuses still give the same answers, so instance declarations, unification hints, and reducibility changes invalidate exactly the affected entries. The persistent tier lives in a dedicated `Environment` field with branch-local value semantics: fills roll back with the environment (e.g. when a speculatively added instance is discarded), parallel elaboration branches never observe each other's fills, and a fill costs one structure copy. Context-sensitive results (metavariable-laden keys, free-variable-dependent entries) stay in the per-command tier; in particular, free-variable-keyed entries must not be persisted, as `FVarId`s recur across commands under fresh name generators (see the `tc_cache_persist_fvar` test). The behavioral test suite for dependency recording arrives here, as most of it is only observable across commands: decl-time vs post-hoc reducibility changes, option partitioning with coexisting entries, fine-grained unification-hint invalidation, and erased-instance scoping. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Persistent cache fills are environment modifications under the current storage design, so entries filled inside rolled-back regions are no longer served afterwards; the affected expectations flip from `cached:` to `new:`. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…nth` The `#14316` merge resolved these two files to their ref-era versions, which expect `#eval`-internal type class queries to hit entries persisted by earlier commands. Under the trust-tier persistent cache, `#eval` rolls back its environment changes including cache fills, so these queries search anew each time. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Free-variable normalization re-instantiates the stored result schema on every cache hit (`SynthNorm.reopen`), so repeated queries in one context receive structurally equal but pointer-distinct instance terms. Consumers that rely on pointer identity for cheap sharing pay deep structural work per copy: `grind`'s alpha-sharing made `Mathlib.Logic.Equiv.Prod` 2.2x slower (one `grind` proof 3.0s -> 6.7s, the file +96% instructions in the full-Mathlib bench) with byte-identical query traces. This PR therefore additionally memoizes the context-level (reopened) result under the unnormalized key in the transient tier, so repeated queries in one context return the same object, exactly as before normalization; cross-context sharing via the normalized key is unchanged. This also restores within-context caching for results that escape the normalization closure, which the normalized tiers cannot hold. Guarded by the new option `backward.synthInstance.rawKeyCache`. With the fix, `Mathlib.Logic.Equiv.Prod` returns to parity (73.2G -> 34.6G instructions locally) and the standard bench file set is unchanged within noise. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…y cache unconditionally The option was a debugging aid while validating the raw-key front-cache; there is no backward-compatibility reason to toggle it. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
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.
Based on #14316