experiment: persist type class resolution cache across commands - #14316
Draft
Kha wants to merge 3 commits into
Draft
experiment: persist type class resolution cache across commands#14316Kha wants to merge 3 commits into
Kha wants to merge 3 commits into
Conversation
Member
Author
|
!bench |
Member
Author
|
!bench mathlib |
|
Benchmark results for d028112 against 41b2fe8 are in. There are significant results. @Kha
Large changes (4✅)
and 1 hidden Medium changes (52✅, 3🟥) Too many entries to display here. View the full report on radar instead. Small changes (814✅, 6🟥) Too many entries to display here. View the full report on radar instead. |
|
Benchmark results for leanprover-community/mathlib4-nightly-testing@0015b87 against leanprover-community/mathlib4-nightly-testing@de3a9cf are in. There are significant results. @Kha
Large changes (30✅) Too many entries to display here. View the full report on radar instead. Medium changes (189✅) Too many entries to display here. View the full report on radar instead. Small changes (690✅) Too many entries to display here. View the full report on radar instead. |
Kha
force-pushed
the
push-msumqyxslkpk
branch
2 times, most recently
from
July 8, 2026 08:11
51b6cf0 to
4e89424
Compare
github-actions
Bot
added
the
toolchain-available
Collaborator
|
Reference manual CI status:
|
github-actions
Bot
added
the
mathlib4-nightly-available
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 8, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Jul 8, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Jul 9, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Jul 9, 2026
leanprover-bot
added
the
builds-manual
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Jul 10, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Jul 10, 2026
leanprover-bot
added a commit
to leanprover/reference-manual
that referenced
this pull request
Jul 10, 2026
leanprover-bot
added
breaks-manual
mathlib-lean-pr-testing
Bot
added
builds-mathlib
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Jul 11, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Jul 11, 2026
leanprover-bot
added a commit
to leanprover/reference-manual
that referenced
this pull request
Jul 11, 2026
Member
Author
|
!bench mathlib |
|
Benchmark results for 61aa947 against 2065c90 are in. There are significant results. @Kha
Large changes (2✅)
Medium changes (24✅)
Small changes (626✅, 9🟥)
|
Kha
added a commit
that referenced
this pull request
Jul 26, 2026
…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>
Kha
added a commit
that referenced
this pull request
Jul 28, 2026
…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>
Kha
added a commit
that referenced
this pull request
Jul 28, 2026
…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>
Kha
added a commit
that referenced
this pull request
Jul 29, 2026
…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>
Kha
added a commit
that referenced
this pull request
Jul 30, 2026
…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>
Kha
added a commit
that referenced
this pull request
Jul 30, 2026
…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>
Kha
added a commit
that referenced
this pull request
Jul 30, 2026
…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>
Kha
added a commit
that referenced
this pull request
Jul 31, 2026
…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>
This PR makes type class resolution cache entries depend on the options they observed: a query records every result-relevant option lookup (`Lean.Meta.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. By-name option reads are restricted while a query runs (`Lean.OptionsRestriction`): a plain read panics, so nothing can go unrecorded. Type class resolution is a closed system, so the few frameworks whose reads cannot influence a result read through `Options.findUnrestricted?`/`Lean.Option.getUnrestricted` at their accessor, each carrying its one-line argument (trace and profiler collection, diagnostics counters, and limits whose excess throws and is never cached). Contexts captured for later rendering (messages, pretty printing, profiling) drop the restriction at the boundary. Co-Authored-By: Claude Fable 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. 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>
Kha
added a commit
that referenced
this pull request
Aug 9, 2026
…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>
leanprover-bot
added a commit
to leanprover/reference-manual
that referenced
this pull request
Aug 9, 2026
leanprover-bot
removed
the
breaks-manual
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.
Not yet sound, to establish upper threshold