perf: restrict and record option accesses during type class resolution - #14932
Draft
Kha wants to merge 3 commits into
Draft
perf: restrict and record option accesses during type class resolution#14932Kha wants to merge 3 commits into
Kha wants to merge 3 commits into
Conversation
Member
Author
|
!bench |
Member
Author
|
!bench |
|
Benchmark results for c71b1d3 against b9c9eb9 are in. There are significant results. @Kha
Medium changes (4🟥)
Small changes (190🟥)
|
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>
This PR speeds up type class resolution by storing the definitional-equality flags and resource limits that partition the resolution cache as unboxed words rather than as pointers to records, so that hashing and comparing a cache key no longer walks thirteen boxed fields on every probe. `SynthDefEqFlags` becomes a single `UInt32` bitfield with accessors, which the compiler erases to a bare word, and `SynthLimits` is inlined into `SynthInstanceCacheKey` as four `UInt64` fields. The key therefore carries five unboxed scalars instead of two pointers to freshly allocated records, which also removes two allocations per query. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Member
Author
|
!bench |
|
Benchmark results for 7aa96c2 against b9c9eb9 are in. There are significant results. @Kha
Medium changes (4🟥)
Small changes (182🟥)
|
…word This PR removes a pointer field from `Meta.Context`, which is reconstructed on every `withConfig`/`withTransparency`-style scope, by storing the resolved definitional-equality flags as a sentinel-tagged `UInt32` instead of an `Option`. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
github-actions
Bot
added
toolchain-available
|
Mathlib CI status (docs):
|
leanprover-bot
added
the
builds-manual
Collaborator
|
Reference manual CI status:
|
Member
Author
|
!bench |
|
Benchmark results for 3fbd61b against b9c9eb9 are in. There are significant results. @Kha
Medium changes (4🟥)
Small changes (145🟥)
|
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Aug 27, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Aug 27, 2026
leanprover-bot
added a commit
to leanprover/reference-manual
that referenced
this pull request
Aug 27, 2026
mathlib-lean-pr-testing
Bot
added
the
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.
This PR makes type class resolution cache entries depend on the options they observed, as a first prerequisite for more extensive caching.
A query now 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 directly is forbidden:
getOptionspanics whileCore.Context.recordingDepsis 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 newMonadOptions.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.