perf: restrict and record option accesses during type class resolution - #14932
Draft
Kha wants to merge 11 commits into
Draft
perf: restrict and record option accesses during type class resolution#14932Kha wants to merge 11 commits into
Kha wants to merge 11 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
Member
Author
|
!bench mathlib |
|
Benchmark results for leanprover-community/mathlib4-nightly-testing@dabd0b6 against leanprover-community/mathlib4-nightly-testing@dc2cdbd are in. There are significant results. @Kha
Small changes (21🟥)
|
`Core.instMonadOptionsCoreM.getOptions` is inlined at every `getOptions` call site in the compiler, and `panic!` is `@[inline]`, so each of those sites grew a private copy of the tripwire's message constants: 265 copies of the 173-byte message ended up in `libleanshared.so`, along with a `panic._at_….spec_N` specialization and four `_closed_N` constants per site. Moving the panic into a `@[noinline]` `where` helper leaves one copy. Measured against the merge base, over the whole stage1 stdlib: `libleanshared.so` +0.42% -> +0.15%, `.olean.private` +0.42% -> +0.25%, `.ir` +0.47% -> +0.31%. Per module (`trace.Compiler.stat` sum of `decl.size`), `Lean/Compiler/LCNF/Simp` +2.40% -> +1.06% and `Lean/Elab/App` +0.84% -> +0.58%, with the extra compiled declarations gone entirely in most modules. `Init` modules were and remain unaffected. Co-Authored-By: Claude <noreply@anthropic.com>
Member
Author
|
!bench |
|
Benchmark results for 2d09aa2 against b9c9eb9 are in. There are significant results. @Kha
Large changes (3🟥)
Medium changes (1✅)
Small changes (104🟥)
|
… resolution cache `validateDeps?` ignored its `Environment` argument and always reported the entry as not re-stamped, so `findCachedResult?`'s re-insertion branch was unreachable; both collapse into a `List.find?` over `validOptionAccesses`. The `SynthInstanceCache` and `Meta.Cache` docstrings described an environment-dependency tier that does not exist here, naming `SynthDepLog`, `Lean.EnvExtension.TCResolutionAccess` and `synthInstanceCacheExt`; the former also carried a duplicated half-sentence from a bad edit. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Aug 28, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Aug 28, 2026
leanprover-bot
added a commit
to leanprover/reference-manual
that referenced
this pull request
Aug 28, 2026
Member
Author
|
!bench mathlib |
|
Benchmark results for leanprover-community/mathlib4-nightly-testing@200ab0a against leanprover-community/mathlib4-nightly-testing@dc2cdbd are in. There are significant results. @Kha
Small changes (1✅, 38🟥)
|
`withOptions` hands its transformer the ambient options, so the transformer may derive the value of an option that the search later reads through `getRecordedOption`. The dependency log then records that derived value while `findCachedResult?` validates against the ambient one, and nothing constrains what the transformer would have produced in the validating context, so an entry can be reused where it does not hold. `MonadWithOptions CoreM` now reports a violation when a transformer runs inside a recording computation, and `withSetOption`/`withSetOptionByName` provide the form whose new value cannot depend on the ambient options. The two call sites reachable from a search, the `Meta.isLevelDefEq` trace message and `mkUnfoldAxiomsNote`, use them. The transformer body moves to `Core.withOptionsUnrestricted`, kept `@[inline]` so that codegen is unchanged: instance bodies are inlined at statically resolved call sites, and the generated C for modules calling `withOptions` has the same number of `Kernel.isDiagnosticsEnabled` calls as before. The panic is kept out of line for the same reason as the one in `getOptions`. The guard is partial. Seven sites write `Core.Context.options` directly and bypass it, of which `realizeConst`'s `realizeAndReport` is the one that could plausibly run under a search. `withSetOption` also cannot enforce that its value is independent of the ambient options, only make the dependency explicit. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The flags occupy bits 0 to 8 and `armedBit` bit 15, so `UInt16` fits them exactly, while `UInt32` left a sixteen-bit hole above the sentinel that the docstring did not account for. The layout is now written down: bits 0 to 8 are the flags, 9 to 14 are free for further ones, and 15 is `armedBit`. This does not shrink either object that holds the word. `Meta.Context`'s scalar area goes from 8 to 6 bytes and `SynthInstanceCacheKey`'s from 36 to 34, but both objects round into the same 8-byte bucket, 72 and 80 bytes respectively. `toContextWord` now also records that its result is not interchangeable with the flags it came from: the derived `BEq` and `Hashable` compare raw `bits`, so the armed word and the un-armed one are distinct values denoting the same flags, and only the un-armed form may be stored in `SynthInstanceCacheKey.defEqFlags`. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
A dependency log entry was the value a lookup returned, which is the value in effect where the lookup happened, while a cache entry is validated against the ambient options where the query started. Those differ for a lookup made under an options write that the query itself opened, and because the log is deduplicated by name, such a lookup could take the slot of the ambient one and leave the entry validating in contexts the recorded computation never ran in. `RecordedDeps` now carries the options in effect when recording started, and a lookup is a dependency only when it answers as that watermark does. A lookup served by a write inside the query answers differently and is not recorded at all, which is also correct: its value is independent of the ambient options, so the entry is reusable regardless of them rather than pinned to the written value. The log no longer depends on the order the lookups happen in. `RecordedDeps.mergeInto` applies the same test against the enclosing query's watermark, so a nested query's scope-local value is not injected into a log that is validated without that scope. This mirrors how declaration dependencies are handled, where a change whose target was born after the recorded `constBirthGen` is skipped because the computation cannot have observed it. No behavior changes today: the options that reach a log (`backward.synthInstance.canonInstances`, `synthInstance.maxSize`, `maxSynthPendingDepth`) are disjoint from those written inside a search (`diagnostics`, `pp.instantiateMVars`), so no lookup answers differently from the watermark. The situation also cannot be reached from Lean source, as nothing gives user code a foothold inside a search. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`sameDepIdentity` decides whether a freshly computed type class resolution entry replaces an existing one for the same key or joins it in a list. Its documented meaning is the same option lookups with the same answers, but it is `Array` equality, which is elementwise in order, and the recorded order is the order the search happened to reach each option in rather than a property of the dependency set. Two searches of one key that reach a nested query or a `synthPending` at different points record the same set in a different order, so the new log fails the identity test, both are kept, and every later lookup for that key walks and validates the redundant entry. `insertCachedResult` now sorts the accesses by name, in the same rewrite that already clears the recording watermark, so both operands of `sameDepIdentity` are canonical and comparing the arrays compares the sets. Names are unique within a log, so the order is total. Nothing else depends on the order: `validOptionAccesses` is an `all`, and `RecordedDeps.mergeInto` deduplicates by name membership. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`getRecordedBoolOption` has no call sites, here or on the environment-dependency stack that builds on this one, so unlike the `validateDeps?` parameters it is not scaffolding for later work. `getRecordedOption` covers every option the search reads. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Member
Author
|
!bench |
|
Benchmark results for a660d9e against 0e6944a are in. There are significant results. @Kha
Small changes (75🟥)
|
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.