perf: normalize free variables in the type class resolution cache key - #14369
Draft
Kha wants to merge 23 commits into
Draft
perf: normalize free variables in the type class resolution cache key#14369Kha wants to merge 23 commits into
Kha wants to merge 23 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. |
…tions This PR fixes an instance being synthesized in two different, definitionally equal forms in two commands, which can leave a goal such as `x = x` unprovable by `rfl` under a restricted transparency setting. `backward.isDefEq.respectTransparency` and `backward.isDefEq.respectTransparency.types` control whether `isDefEq` bumps the transparency to `.default` when assigning a metavariable, and hence which of several definitionally equal terms an instance's implicit arguments are assigned. The cache persists across commands, which may set the options differently, so add both to the key, as for `backward.synthInstance.canonInstances`. The options are read by name because `Lean.Meta.ExprDefEq`, which declares them, transitively imports `Lean.Meta.SynthInstance`. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This PR lets instance queries whose local context contains a `let` share a cache entry with structurally identical queries in other contexts, instead of falling back to a context-specific key. The free-variable normalization gave up on a let-bound closure variable, because its value is visible to definitional unfolding but was not part of the key. Record the normalized value alongside the normalized type, so that contexts agreeing on the types but not the values stay apart. A nondependent `ldecl` (a `have`) hides its value from unfolding and needs no value in the key. On `Mathlib.RingTheory.DedekindDomain.Different` this removes every let-induced fallback: the queries that fall back to a raw key drop from 32938 to 19192, cache misses from 15420 to 15023, and the heartbeats spent inside missed searches by 5.3%. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…nsion state Replaces the `IO.Ref` indirection in `synthInstanceCacheExt` with the cache map itself: fills and invalidation become plain branch-local environment modifications, so an entry is only ever observable in environments derived from the one it was filled in. This removes the need for any argument that reusing entries across environment rollbacks and parallel elaboration branches is sound: rolled-back fills disappear with the environment, and async elaboration branches (e.g. theorem proofs) never observe each other's fills. To keep within-command backtracking behavior on par with stock `Meta.Cache` semantics (cf. the commit this partially reverts: backtracking-heavy proofs re-ran every typeclass query per failed attempt), persistent entries are now additionally written to the transient `Meta.Cache.synthInstance` tier, which `Meta.SavedState.restore` deliberately does not restore; the transient copy dies with the command. The cost is that fills from theorem proof tasks (async branches) and rolled-back regions no longer persist across commands; this commit exists to measure that cost against the `IO.Ref` variant. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This PR lets an instance query whose class has output parameters share a cache entry with structurally identical queries in other local contexts, and persist across commands, as queries without metavariables already do. The free-variable normalization ran only on `.noMVars` queries, so every other key kept the free variables of the context that created it and could never be shared. Run it on all queries: metavariable identities are left exactly as they are, so only the free variables are canonicalized. The wildcard that `preprocess` puts in output-parameter positions is left alone, being a marker rather than a variable of the local context. The gate on persistence tested `.noMVars`, which is a proxy for what it actually requires: a key without metavariables. Test that directly. An `.mvarsOutputParams` key has its output parameters replaced by a wildcard, so it is metavariable-free whenever every metavariable sits in an output parameter, and is then as context-free as a `.noMVars` key: the wildcard stands for a value the input parameters determine, and a hit re-derives it by unifying the cached result against the query. On `Mathlib.Algebra.Group.Basic` the misses drop from 1230 to 944 and the heartbeats spent inside missed searches by 45%. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Kha
removed
the
mathlib4-nightly-available
Member
Author
|
!bench mathlib |
|
Waiting until the label
mathlib4-nightly-available
You can edit the original message until the command succeeds. |
Member
Author
|
!bench |
|
Benchmark results for 26520e1 against 2065c90 are in. There are significant results. @Kha
Large changes (3✅)
Medium changes (35✅, 4🟥)
Small changes (822✅, 46🟥)
|
…behind `MetaM`'s back Context-free entries are written to both the persistent tier and the transient `Meta.Cache.synthInstance` tier, so a cached failure could be served even after an instance was added through an environment modification the current `Meta.State` cannot observe. `#eval`'s automatic `Repr` derivation hit exactly this: the deriving handlers run via `liftCommandElabM`, whose internal resets cannot clear the calling `MetaM`'s transient tier, so the retry kept seeing the stale failure (`tests/elab/eval.lean`, and the likely cause of the Mathlib build failure on the previous push). `resetSynthInstanceCache` is now a `MetaM` function clearing both tiers, restoring its stock behavior of also clearing the transient cache; `resetSynthInstanceCacheCore` remains for `CoreM` callers, which can only reach the persistent tier. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Member
Author
|
!bench |
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🟥)
|
|
Waiting until the label
mathlib4-nightly-available
You can edit the original message until the command succeeds. |
|
The adaptation PR for this PR is leanprover/downstream-lean4#15. |
PRs labeled `skip-tests` skip the `ctest` step so CI still produces the `pr-release` toolchain for experimental branches with known-failing tests, e.g. for Mathlib benchmarking. The dependent summary and binary-check steps already handle a skipped test step. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…options The cache key listed hand-picked option values (`backward.synthInstance.canonInstances` and the `backward.isDefEq.respectTransparency` pair, the latter read by name to avoid an import cycle), leaving any other option read on the search path unkeyed; `maxSynthPendingDepth` was such a gap. The key now contains the canonical sequence of all result-relevant options (`synthInstance.*`, `backward.*`, `smartUnfolding`, `maxSynthPendingDepth`), and the search runs under an access-restricted options object: `Options` gains a `restriction` flag (`Options.restrict .tcResolution`, a constant-time update), and the by-name accessors panic on access to an option outside the allowed set. Any other option is thus invisible to the search by construction, and a new option read on the search path only takes effect once added to `isSynthRelevantOption`, which also keys the cache by it. The allowed set is the result-relevant options plus declaredly inert ones: tracing, pretty printing and formatting (messages and trace nodes capture the ambient options object and are rendered later), profiling, diagnostics, debugging, realization infrastructure, limits (exceeding them throws, and exceptions are not cached, e.g. `exponentiation.threshold` reached via `Lean.checkExponent` during cached-result application), and the `_inPattern` pseudo-option read by the delaborator. Setting a relevant option explicitly to its default value creates a fresh cache partition (the key does not resolve defaults); this only costs a re-derivation. Measured on `Init.Data.Vector.Lemmas` and `Std.Data.HashMap.Lemmas`: about +0.3% instructions over the plain persistent-cache baseline, the per-access cost of the enforcement check on the hot `backward.*` reads inside `isDefEq`; validated panic-free over all of `src/` with `LEAN_ABORT_ON_PANIC`. 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