experiment: consolidate all TC opts#14339
Draft
Kha wants to merge 15 commits into
Draft
Conversation
…ation) Minimal variant for stage2/Mathlib experimentation: the `synthInstance` cache is moved from `Meta.Cache` into a new environment extension `synthInstanceCacheExt` (`asyncMode := .local`) so that results are reused across commands within a file instead of being discarded with the per-command `Meta.State`. This variant performs *no* automatic invalidation: changes to the instance table (additions, erasures, scoped activation via `open`, local instances), reducibility statuses, or unification hints do not discard stale entries; `resetSynthInstanceCache` (now a `CoreM` operation clearing the extension state) is the only way to invalidate. `SynthInstanceCacheKey` now includes the effective `maxResultSize`, `backward.synthInstance.canonInstances`, and `Environment.isExporting` since these can vary during the (now longer) lifetime of the cache, e.g. a failure cached under `synthInstance.maxSize 128` must not shadow a later attempt under a larger limit. Note that `example`s are elaborated inside `withoutModifyingEnv` and therefore read the cache without contributing entries; similarly, cache fills on async elaboration branches (e.g. theorem proofs) remain branch-local. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Alternative to the pointer-identity fingerprint variant: the cache extension is registered in `Lean.Meta.Instances` so that `addInstance` and the `instance` attribute erase handler can reset it explicitly after modifying the instance table. Not covered by this variant: activating scoped instances via `open` (or entering their namespace), closing a section containing local instances, reducibility status changes of pre-existing declarations, and unification hints. These require an explicit `resetSynthInstanceCache`. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Scoped instance activation (e.g. `open Classical in` as produced by the `by_cases` expansion of the `if h : c` tactic) changes typeclass resolution results without going through `addInstance`, so the explicit cache reset there does not cover it; this broke `Init.Data.List.Sublist` in stage2. Instead of invalidating the cache on activation, the set of activated namespaces that have scoped instances becomes part of `SynthInstanceCacheKey`: entries from outside a scope stay valid after the scope ends, and re-entering an equal scope (e.g. repeated `by_cases`) reuses the entries cached inside the previous one. Namespaces without scoped instances are omitted from the key so that plain `open`s do not fragment the cache; this is sound because adding the first scoped instance to a namespace goes through `addInstance`, which resets the whole cache. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Typeclass queries whose resolution gets stuck on an unassignable metavariable (`isDefEqStuck`) are retried by the elaborator whenever any progress is made (e.g. each `synthesizeSyntheticMVars` round), and each retry re-runs the full search setup — goal preprocessing, instance collection and priority-sorting via `getUnify` (which returns all instances of the class when the discriminating argument is a metavariable) — only to throw again on the first candidate. Measured on an early Mathlib slice, these doomed searches account for ~21% of all typeclass-search heartbeats (~800 heartbeats per call, 41K calls). Stuckness is now memoized in a new transient `Meta.Cache.synthStuck` set: a repeated query with the same key fails fast with `isDefEqStuck` instead of re-running the search. This is sound with the lifetime of `Meta.Cache`: the cache key is built from the `instantiateMVars`-normalized goal, so once the blocking metavariable is assigned the retry uses a different key, and goal metavariables are never assignable inside the search regardless of the caller (`SynthInstance.main` runs in `withNewMCtxDepth`), so stuckness does not depend on the ambient depth. Instance table changes clear `Meta.Cache` as before. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Storing the cache map directly in the environment extension meant every cache fill was an environment modification, discarded by `Core.SavedState.restore` (`env := b.env`) on each failed tactic attempt. Backtracking-heavy proofs (e.g. aesop rule search) thus re-ran every typeclass query per attempt: in `Mathlib.CategoryTheory.Center.Linear`, the same `CommMagma R` query ran 686 times and a later query that stock elaboration serves from results accumulated across failed attempts had to redo the entire search inside a single `synthInstance.maxHeartbeats` budget, failing deterministically (also `Mathlib.Algebra.Ring.Subring.Basic`, `Mathlib.GroupTheory.Transfer`). Stock does not have this problem because `Meta.SavedState.restore` deliberately does not restore `Meta.Cache`. The extension state is now an `IO.Ref` around the cache map: fills mutate the ref and survive environment rollbacks (matching `Meta.Cache` semantics, including its accepted imprecision that fills made during a rolled-back attempt survive), while invalidation replaces the ref, which remains an environment modification and is thus correctly reverted together with a rolled-back instance addition. Fills also become cheaper (no extension-state array copy per insert). Environment values derived from the same environment share the ref; isolating contexts that should not share the cache (async branches, incremental reuse) by replacing the ref at fork points is left for later. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The memoized stuck queries allocate fewer metavariables during `exact?` elaboration, shifting the metavariable counter exposed in a `Completion-Id` info node. Co-Authored-By: Claude <noreply@anthropic.com>
`attribute [local instance] X in`/section scopes previously leaked cache entries computed with the local instance out of the scope (the scope close restores the instance table but no `addInstance` hook runs): in `Mathlib.Data.Set.Functor`, theorems following `attribute [local instance] Set.monad in ...` were elaborated with the `Monad Set`-based coercion instead of the `Subtype.val` image. Analogous to the treatment of scoped instance activation, `Instances` now records the names of instances added with the `local` attribute kind, and the cache key includes this list. Closing the scope restores the previous `Instances` state and thus the previous key partition, so entries never leak into or out of scopes with local instances. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…dingDepth` The type class resolution cache is keyed by `synthPendingDepth` (issue #2522), which partitions the whole cache by depth even though the depth can only influence a query through the `synthPending` give-up check. Track whether a query ever reached a `synthPending` decision (via a non-backtrackable `IO.Ref` in `Meta.Context`, so discarded search branches still count); results of queries that never did are now cached with `synthPendingDepth := none` and shared across all depths. Depth-sensitive results remain keyed by their exact depth as before. The `Meta.synthInstance.cache` trace now includes the depth when it is nonzero. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The stuck-query memoization allocates fewer metavariables during elaboration, shifting the hardcoded unique name in the completion item data from `f_uniq.51` to `f_uniq.33`. Co-Authored-By: Claude <noreply@anthropic.com>
Results with abstracted metavariables are only valid relative to the elaboration context that created them: degrees of freedom not determined by the cache key (e.g. universe metavariables of intermediate instances, cf. `Small`) are resolved by ambient unification constraints. Persisting such entries and reusing them in a different context (a later command, or a different elaboration phase of the same declaration) produces incorrectly instantiated terms: in `Mathlib.Condensed.Discrete.Module`, a cached `(sheafToPresheaf _ _).IsRightAdjoint` result was reused with universe instantiations from the wrong context, yielding kernel-rejected declarations. The cache is now split into two tiers: the persistent environment extension only receives entries with a metavariable-free key and a closed result, which are context-free (free universe parameters and fvar references are pinned by the key). All other entries go to a reintroduced transient `Meta.Cache.synthInstance` tier with the previous per-`Meta.State` lifetime and semantics, the scope for which such sharing was originally designed. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…epth Instead of a single depth-invariant class, each shared type class resolution cache entry now records the maximal `synthPendingDepth` (relative to the query) at which a `synthPending` decision was reached during synthesis, and is reused at any depth at which no such decision can reach the `maxSynthPendingDepth` give-up threshold. Only results whose synthesis actually hit the threshold remain keyed to their exact depth. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The stuck-query memoization assumed stuckness is a pure function of the cache key: the blocking metavariable was expected to occur in the instantiated query, so any assignment would invalidate the entry by changing the key. This does not hold in general. Local instances participate in the key only by their `FVarId`, so a query stuck on a metavariable inside a local instance type (e.g. from a binder `[NeZero ofNat(m)]` during signature elaboration) keeps hitting the memoized entry even after default-instance resolution assigns that metavariable, and elaboration reports "typeclass instance problem is stuck" for code that used to succeed (observed in Mathlib in `Mathlib/Data/Fin/Basic.lean` and `Mathlib/CategoryTheory/EffectiveEpi/Comp.lean`). Memoize stuckness only when it is a pure function of the key: all local instance types must be metavariable-free, and all metavariables in the query must be natural and not delayed-assigned (non-natural ones can be resolved by the search itself via `synthPending`). Level metavariables at the caller's depth may additionally be assigned during the search (`allowLevelAssignments`), so record the set of assignable level metavariables of the key and consult the memoized entry only when that set is unchanged. Also revert the `info_trees` expectation to its original value: with the purity guard, the memoization no longer fires in that scenario. Co-Authored-By: Claude <noreply@anthropic.com>
Normalize the free variables of `.noMVars` type class resolution queries so that structurally identical queries in different local contexts can share a persistent cache entry. The free variables of the query type and `localInsts` are renamed to canonical positional variables for the cache key, and the result is stored abstracted over that closure as loose bound variables (`Expr.abstract`) and re-instantiated with the current context on a hit, analogously to how `abstractMVars` produces a closed schema. Checkpoint: on core algebra, order, and logic modules this cuts misses noticeably (e.g. `Algebra.Group.Basic` from 58% to 46%), but a `grind` instance-canonicalization regression in `Mathlib.Logic.Equiv.Prod` still needs fixing, where a reopened instance is not definitionally equal to a fresh synthesis. Set `LEAN_NO_FVAR_NORM=1` to disable it for A/B measurement. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Member
Author
|
!bench |
|
Benchmark results for 61fc909 against da19ea0 are in. There are significant results. @Kha
Large changes (5✅)
and 1 hidden Medium changes (56✅) Too many entries to display here. View the full report on radar instead. Small changes (937✅, 14🟥) Too many entries to display here. View the full report on radar instead. |
github-actions
Bot
added
toolchain-available
Member
Author
|
!bench mathlib |
|
Benchmark results for leanprover-community/mathlib4-nightly-testing@742a28b against leanprover-community/mathlib4-nightly-testing@d87691e are in. There are significant results. @Kha
No significant changes detected. |
leanprover-bot
added
the
builds-manual
Collaborator
|
Reference manual CI status:
|
mathlib-lean-pr-testing
Bot
added
the
breaks-mathlib
|
Mathlib CI status (docs):
|
`SynthNorm.normExpr` and the `hasAnyFVar` escape check in `abstractOverClosure?` recursed over query terms as trees, so `.noMVars` queries whose types are heavily DAG-shared (as built by `grind`'s e-matching via substitution, e.g. nested `if`s in `Mathlib.Logic.Equiv.Prod`) burned exponential allocations, exhausting the heartbeat budget and failing `grind` with a deterministic `whnf` timeout. Memoize `normExpr` on `ExprStructEq`-keyed subterms (sound since canonical positions are assigned by first occurrence and never change) with a `hasFVar` fast path, and rewrite `abstractOverClosure?` to abstract first (DAG-cached in C++) and check the O(1) `hasFVar` flag of the result, keeping both linear in the DAG size of the query. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Member
Author
|
!bench mathlib |
|
Benchmark results for leanprover-community/mathlib4-nightly-testing@742a28b against leanprover-community/mathlib4-nightly-testing@d87691e are in. (These commits have already been benchmarked in a previous command.) There are significant results. @Kha
No significant changes detected. |
Kha
removed
the
mathlib4-nightly-available
Member
Author
|
!bench mathlib |
|
Benchmark results for leanprover-community/mathlib4-nightly-testing@df4c7ab against leanprover-community/mathlib4-nightly-testing@d87691e are in. There are significant results. @Kha
Large changes (26✅, 1🟥) Too many entries to display here. View the full report on radar instead. Medium changes (286✅, 1🟥) Too many entries to display here. View the full report on radar instead. Small changes (983✅, 3🟥) Too many entries to display here. View the full report on radar instead. |
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Jul 9, 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 9, 2026
leanprover-bot
added a commit
to leanprover/reference-manual
that referenced
this pull request
Jul 9, 2026
mathlib-lean-pr-testing
Bot
added
builds-mathlib
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.
No description provided.