perf: avoid setTransparency when the transparency is already in effect - #14967
Draft
Kha wants to merge 1 commit into
Draft
perf: avoid setTransparency when the transparency is already in effect#14967Kha wants to merge 1 commit into
setTransparency when the transparency is already in effect#14967Kha wants to merge 1 commit into
Conversation
This PR speeds up elaboration by not rebuilding the `MetaM` context when `withTransparency` or `withAtLeastTransparency` is asked for the transparency setting that is already in effect. `Context.setTransparency` rebuilds `Config`, `ConfigWithKey` and `Context`, so each such call allocated three objects and retraced the `Context`'s pointer fields even when nothing changed. `withTransparency` did this unconditionally, and `withAtLeastTransparency` did it by construction on the branch where the ambient mode already suffices. Both are hot: `withInferTypeConfig` wraps every `inferType` in `withAtLeastTransparency .default`, as does `getFunInfoAux`, and `.default` is usually the ambient mode already. Skipping the rebuild is observationally equivalent: `ConfigWithKey.key` is maintained as `Config.toKey`, whose low three bits are exactly `transparency.toUInt64`, so re-applying the current mode reproduces an identical `Config` and an identical key. Measured over 12 `elab_bench` files, 5 interleaved repetitions per variant against a same-machine baseline build: -0.33% instructions overall, with every file improving (-0.06% to -1.16%). The run-to-run noise floor for this metric is 0.10% per file and 0.00% overall. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Member
Author
|
!bench |
|
Benchmark results for af20c82 against e991a05 are in. There are significant results. @Kha
Medium changes (2✅, 1🟥)
Small changes (292✅, 8🟥)
|
github-actions
Bot
added
toolchain-available
leanprover-bot
added
the
builds-manual
Collaborator
|
Reference manual CI status:
|
mathlib-lean-pr-testing
Bot
added
the
builds-mathlib
|
Mathlib CI status (docs):
|
Member
Author
|
!bench mathlib |
|
Benchmark results for leanprover-community/mathlib4-nightly-testing@3da59b7 against leanprover-community/mathlib4-nightly-testing@78f2465 are in. There are significant results. @Kha
Large changes (1✅)
Small changes (7✅, 7🟥)
|
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 speeds up elaboration by not rebuilding the
MetaMcontext whenwithTransparencyorwithAtLeastTransparencyis asked for the transparency setting that is already in effect.Context.setTransparencyrebuildsConfig,ConfigWithKeyandContext, so each such call allocated three objects and retraced theContext's pointer fields even when nothing changed.withTransparencydid this unconditionally, andwithAtLeastTransparencydid it by construction on the branch where the ambient mode already suffices. Both are hot:withInferTypeConfigwraps everyinferTypeinwithAtLeastTransparency .default, as doesgetFunInfoAux, and.defaultis usually the ambient mode already.Skipping the rebuild is observationally equivalent:
ConfigWithKey.keyis maintained asConfig.toKey, whose low three bits are exactlytransparency.toUInt64, so re-applying the current mode reproduces an identicalConfigand an identical key.