perf: lazy IR loading#14145
Draft
Kha wants to merge 5 commits into
Draft
Conversation
This PR threads `BaseIO` through `getModuleIREntries` and the interpreter/codegen lookups that consume imported IR, in preparation for loading imported IR on demand. There is no behavior change yet: the lookups still read the eagerly-imported state. `getModuleIREntries`, `findInterpDecl`/`findInterpDeclBoxed`, `findEnvDecl`/`findEnvDecl'`, `getSorryDep`, and `getRegularInitAttrModIdxs` become `BaseIO`; `findExtEntry?` is split so the non-IR LCNF lookups stay pure and a new `findIRExtEntry?` carries the IR branch. The C-export ABI is unchanged: `BaseIO` compiles to a bare value-return (no world argument, no error wrapper), so `ir_interpreter.cpp` needs no changes. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This PR makes `[inherit_doc]` copy the resolved docstring when a public declaration inherits one from a private declaration, instead of storing an alias to the private name. An importer cannot resolve such an alias because the private target is not exported and has no module index, so the inherited docstring would be lost across modules. Since the source is available where the attribute is applied, its docstring is copied eagerly; all other cases keep the existing alias behavior. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This PR loads a module's interpreter IR (`.ir`) lazily, on first use, instead of eagerly populating the IR extension state for every imported module at import time. Modules whose interpreter IR is already part of the imported `.olean` data are read as before; module-system modules with a separate `.ir` are memory-mapped and cached on first access. `Kernel.Environment`'s `irBaseExts : Array EnvExtensionState` field becomes `irData : Option LazyIR`, holding the per-module `.ir` paths and a mutable `IO.Ref` cache populated via `modifyGet`. `getModuleIREntries` becomes `BaseIO`; the C-export ABI is unchanged because `BaseIO` compiles to a bare value return. A lazy index maps code-generator auxiliary constants discovered while loading `.ir` files, consulted by the interpreter and codegen lookups when `getModuleIdxFor?` misses. `const2ModIdx` auxiliaries are sourced from the already-loaded `.olean` data. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Member
Author
|
!bench |
|
Benchmark results for ecebaec against bc5f89f are in. There are significant results. @Kha
Large changes (25✅, 30🟥) Too many entries to display here. View the full report on radar instead. Medium changes (2✅, 25🟥) Too many entries to display here. View the full report on radar instead. Small changes (21✅, 1880🟥) Too many entries to display here. View the full report on radar instead. |
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):
|
Contributor
|
!bench |
|
Benchmark results for 46ccc24 against bc5f89f are in. There are significant results. @hargoniX
Large changes (26✅, 5🟥) Too many entries to display here. View the full report on radar instead. Medium changes (2✅, 17🟥)
Small changes (44✅, 1440🟥) 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
Jun 22, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Jun 22, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Jun 22, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Jun 22, 2026
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
4 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.