refactor: move inductive information in compiler from lazily filled local caches to eager persistent environment extensions#13882
Merged
Conversation
Member
Author
|
!bench |
|
Benchmark results for 52e598e against c47a0c7 are in. There are significant results. @Kha
No significant changes detected. |
github-actions
Bot
added
the
toolchain-available
Collaborator
|
Reference manual CI status:
|
Member
Author
|
!bench |
|
Benchmark results for a9515da against c47a0c7 are in. There are significant results. @Kha
Small changes (20✅, 4🟥) 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
May 29, 2026
github-actions
Bot
added
the
mathlib4-nightly-available
mathlib-lean-pr-testing
Bot
added
the
builds-mathlib
|
Mathlib CI status (docs):
|
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
May 29, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
May 29, 2026
This PR lets the compiler handle public types whose constructor field types are not available in importing modules — for example a public structure with a `private` field whose type is only privately imported. Compiling code that uses such a type in another module previously failed because the compiler tried to inspect field types it could not see. The LCNF representation information derived from constructor fields — trivial-structure info, mono and impure types, and constructor layouts — is now computed and persisted in each inductive's defining module and reused by importers instead of being recomputed there. Inductive types are compiled eagerly (`compileInductives`) from `compileDecls`, and the information is stored in `MapDeclarationExtension`s read by strict lookups.
Kha
changed the title
Member
Author
|
!bench |
|
Benchmark results for 79779f6 against c47a0c7 are in. There are significant results. @Kha
Large changes (1🟥)
Medium changes (1🟥)
Small changes (383✅, 45🟥) 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
May 29, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
May 29, 2026
mathlib-lean-pr-testing
Bot
added
breaks-mathlib
This PR fixes a regression where compiling code that uses a `noncomputable` definition could fail with an internal compiler error. `noncomputable` definitions reach `getOtherDeclMonoType` the same way inductive types and constructors do — they have no LCNF code, so `getDecl?` returns `none` — but they are not eagerly compiled, so the strict reader reported them as not compiled. `getOtherDeclMonoType` now keeps the strict gap-detection only for inductive types and constructors (which are eagerly compiled by `compileInductives`), and falls back to lazily computing the mono type from the signature for any other no-LCNF-code declaration (`noncomputable` definitions, foreign functions, opaques, ...), persisting it for declarations of the current module.
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Jun 1, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Jun 1, 2026
mathlib-lean-pr-testing
Bot
added
builds-mathlib
Member
Author
|
!bench |
|
Benchmark results for 6d690ec against c47a0c7 are in. There are significant results. @Kha
Large changes (1🟥)
Medium changes (1🟥)
Small changes (383✅, 56🟥) Too many entries to display here. View the full report on radar instead. |
Member
Author
|
!bench |
|
Benchmark results for b13596b against c47a0c7 are in. There are significant results. @Kha
Large changes (1🟥)
Medium changes (1✅, 1🟥)
Small changes (391✅, 43🟥) 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 2, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Jun 2, 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
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 is in preparation for - and already enables in part - correctly compiling code using public types with private constructors and thus potentially inaccessible type references. A follow-up PR will have to further restrict the trivial structure optimization, which is the only case where even this early analysis can still lead to dangling references.