feat: support `#print axioms` under the module system by nomeata · Pull Request #13117 · leanprover/lean4

nomeata · 2026-03-25T14:24:01Z

This PR re-enables #print axioms under the module system by computing axiom dependencies at olean export time. It reverts #8174 and replaces it with a proper fix.

A PersistentEnvExtension with a custom exportEntriesFnEx computes axiom dependencies when the olean is written. At export time, it walks bodies of all public declarations in the current module (still available via env.setExporting false) to collect axiom dependencies, and stores the results sorted for binary search. Downstream modules look up pre-computed axiom data from imported oleans, so axiom collection never crosses module boundaries. During elaboration of the current module, collectAxioms walks bodies directly since they are always available locally.

The extension exports entries for all public declarations (not just stripped ones) to ensure downstream collect calls terminate at module boundaries without redundant body traversal of imported declarations.

Since axiom data is inherently body-dependent, the pkg/rebuild test (which checks that body-only changes don't trigger downstream rebuilds) requires stage2, where Init modules have extension entries. On stage1 (built with stage0 which lacks the extension), theorems in Init appear as axioms in the kernel environment, inflating the axiom sets.

🤖 Generated with Claude Code

This reverts commit 4c497ea.

Record axiom dependencies eagerly at `addDecl` time in a persistent environment extension (`exportedAxiomsExt`) so that `#print axioms` can report them accurately even after declaration bodies have been stripped on export. Uses a non-blocking collection strategy that avoids accessing `env.checked` (which would deadlock with async `addDecl`), instead consulting previously-recorded axioms for current-module constants and the import env for imported constants. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

nomeata · 2026-03-25T14:29:39Z

!radar

leanprover-radar · 2026-03-25T14:29:47Z

Benchmark results for 3bd2969 against e6df474 are in. Significant changes detected! @nomeata

🟥 build//instructions: +271.0G (+2.23%)

Large changes (14✅, 7🟥)

Too many entries to display here. View the full report on radar instead.

Medium changes (2✅, 37🟥)

Too many entries to display here. View the full report on radar instead.

Small changes (8✅, 1579🟥)

Too many entries to display here. View the full report on radar instead.

Instead of eagerly recording axiom dependencies at addDecl time, compute them lazily in the extension's exportEntriesFn when the olean is written. This is simpler because: - No writes to the extension during elaboration (no async concerns) - No special non-blocking collection logic needed - The extension is empty during local development (bodies are available) - Axiom data is only computed for declarations that actually need it At export time, we compare the exported and private views to find constants whose bodies were stripped, then walk their bodies (still available in env.checked.get) to compute axiom dependencies. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

nomeata · 2026-03-25T15:08:28Z

!radar

leanprover-radar · 2026-03-25T15:08:35Z

Benchmark results for c94e491 against e6df474 are in. Significant changes detected! @nomeata

🟥 build exited with code 2
🟥 other exited with code 2

No significant changes detected.

leanprover-bot · 2026-03-25T15:57:17Z

Reference manual CI status:

❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-24 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-03-25 15:57:17)

mathlib-lean-pr-testing · 2026-03-25T16:41:08Z

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-13117 build failed against this PR. (2026-03-25 16:41:06) View Log

…llection This PR changes the `exportedAxiomsExt` to use `registerPersistentEnvExtension` directly with a custom state type that holds a merged lookup map of all imported modules' extension entries. The `addImportedFn` builds this map at import time, making it available to both `exportEntriesFnEx` (at export time) and `collect` (at query time) without circular references or IO.Ref hacks. At export time, imported stripped declarations are resolved via their source modules' extension entries (containing only real axioms), while current-module declarations are traversed directly with caching to avoid redundant work. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…cation This PR rewrites the axiom collection logic to use a cleaner design: - State uses `seen : NameMap (Array Name)` as a per-constant cache and `axioms : NameSet` as a deduplicating accumulator - Each constant's axioms are computed by temporarily clearing the accumulator, recursing, then caching the sorted result and merging back - Extension state stores raw imported module entry arrays (no merge in addImportedFn), with lookup via getModuleIdxFor? + binary search - exportEntriesFnEx processes all stripped names via forM with shared cache Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…portEntriesFnEx Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

nomeata · 2026-03-26T12:51:48Z

!radar

leanprover-radar · 2026-03-26T12:51:54Z

Benchmark results for 7999de4 against e6df474 are in. Significant changes detected! @nomeata

🟥 build//instructions: +334.1G (+2.75%)

Large changes (4🟥)

🟥 build/profile/.olean serialization//wall-clock: +41s (+49.52%)
🟥 elab/delayed_sharing//instructions: +153.4M (+3.29%)
🟥 size/Init/.olean//bytes: +1MiB (+1.41%)
🟥 size/all/.olean//bytes: +4MiB (+1.26%)

Medium changes (16🟥)

🟥 build//instructions: +334.1G (+2.75%)
🟥 build/module/Init.Data.Array.Extract//instructions: +2.5G (+6.24%) (reduced significance based on absolute threshold)
🟥 build/module/Init.Data.Array.Lemmas//instructions: +1.4G (+2.23%)
🟥 build/module/Init.Data.BitVec.Bitblast//instructions: +1.7G (+2.79%) (reduced significance based on absolute threshold)
🟥 build/module/Init.Data.BitVec.Lemmas//instructions: +3.7G (+2.81%) (reduced significance based on absolute threshold)
🟥 build/module/Init.Data.Int.DivMod.Lemmas//instructions: +1.4G (+3.20%) (reduced significance based on absolute threshold)
🟥 build/module/Init.Data.Range.Polymorphic.Lemmas//instructions: +1.0G (+1.95%) (reduced significance based on absolute threshold)
🟥 build/module/Init.Data.SInt.Lemmas//instructions: +1.0G (+1.62%)
🟥 build/module/Init.Data.Vector.Extract//instructions: +2.0G (+7.10%) (reduced significance based on absolute threshold)
🟥 build/module/Std.Data.DHashMap.RawLemmas//instructions: +1.2G (+0.76%)
🟥 build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: +2.7G (+1.28%) (reduced significance based on absolute threshold)
🟥 build/module/Std.Data.DTreeMap.Internal.Operations//instructions: +1.0G (+2.31%)
🟥 build/module/Std.Data.DTreeMap.Internal.WF.Lemmas//instructions: +1.0G (+2.20%)
🟥 build/module/Std.Data.ExtDHashMap.Lemmas//instructions: +1.1G (+1.92%) (reduced significance based on absolute threshold)
🟥 build/module/Std.Data.Internal.List.Associative//instructions: +1.3G (+1.52%)
🟥 elab/delayed_assign//instructions: +152.6M (+2.84%)

and 1 hidden

Small changes (1877🟥)

Too many entries to display here. View the full report on radar instead.

This tests that `#print axioms` correctly reports axiom dependencies for imported stripped declarations across module boundaries, including diamond imports with same-named private axioms and import chains where axiom dependencies propagate through stripped definitions. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

This moves the `#print axioms` module tests from `pkg/module/PrintAxioms.lean` to the dedicated `pkg/collectAxioms` test and adds coverage for axiom-free defs, opaques, axioms whose types mention other axioms, and multiple axiom dependencies. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

mathlib-lean-pr-testing · 2026-03-26T13:00:24Z

Mathlib CI status (docs):

✅ Mathlib branch lean-pr-testing-13117 has successfully built against this PR. (2026-03-26 13:00:21) View Log

This pre-computes axiom dependencies for every exported declaration, not just stripped ones. Downstream modules can then look up any imported declaration in the extension without walking its body, keeping axiom collection module-local and avoiding redundant cross-module body traversal. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

nomeata · 2026-03-26T13:42:08Z

!radar

leanprover-radar · 2026-03-26T13:42:35Z

Benchmark results for fe5e9a2 against e6df474 are in. Significant changes detected! @nomeata

🟥 build//instructions: +123.6G (+1.02%)

Large changes (4🟥)

🟥 build/profile/.olean serialization//wall-clock: +16s (+20.11%)
🟥 elab/delayed_sharing//instructions: +153.4M (+3.29%)
🟥 size/Init/.olean//bytes: +2MiB (+2.07%)
🟥 size/all/.olean//bytes: +6MiB (+1.98%)

Medium changes (15🟥)

🟥 build/module/Init.Data.Array.Extract//instructions: +2.5G (+6.13%) (reduced significance based on absolute threshold)
🟥 build/module/Init.Data.Array.Lemmas//instructions: +1.4G (+2.22%)
🟥 build/module/Init.Data.BitVec.Bitblast//instructions: +1.7G (+2.85%) (reduced significance based on absolute threshold)
🟥 build/module/Init.Data.BitVec.Lemmas//instructions: +3.9G (+2.95%) (reduced significance based on absolute threshold)
🟥 build/module/Init.Data.Int.DivMod.Lemmas//instructions: +1.4G (+3.29%) (reduced significance based on absolute threshold)
🟥 build/module/Init.Data.Range.Polymorphic.Lemmas//instructions: +1.0G (+2.01%) (reduced significance based on absolute threshold)
🟥 build/module/Init.Data.SInt.Lemmas//instructions: +1.0G (+1.65%)
🟥 build/module/Init.Data.Vector.Extract//instructions: +2.0G (+6.91%) (reduced significance based on absolute threshold)
🟥 build/module/Std.Data.DHashMap.RawLemmas//instructions: +1.2G (+0.80%)
🟥 build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: +2.7G (+1.27%) (reduced significance based on absolute threshold)
🟥 build/module/Std.Data.DTreeMap.Internal.Operations//instructions: +1.1G (+2.48%) (reduced significance based on absolute threshold)
🟥 build/module/Std.Data.ExtDHashMap.Lemmas//instructions: +1.2G (+2.05%) (reduced significance based on absolute threshold)
🟥 build/module/Std.Data.Internal.List.Associative//instructions: +1.5G (+1.67%)
🟥 build/stat/imported bytes//bytes: +2GiB (+1.45%)
🟥 elab/delayed_assign//instructions: +153.9M (+2.86%)

Small changes (893🟥)

Too many entries to display here. View the full report on radar instead.

nomeata and others added 2 commits March 25, 2026 10:50

Revert "chore: disable #print axioms under the module system (#8174)"

74f74ac

This reverts commit 4c497ea.

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Mar 25, 2026

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Mar 25, 2026

Update lean-toolchain for testing leanprover/lean4#13117

4af8e0d

github-actions bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Mar 25, 2026

mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Mar 25, 2026

Update lean-toolchain for testing leanprover/lean4#13117

b7983f4

mathlib-lean-pr-testing bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Mar 25, 2026

nomeata and others added 8 commits March 26, 2026 09:09

refactor: extract insertArray helper and add design comment

44ef56b

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

test: update collectAxioms expected output for sorted results

377b3e7

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

refactor: use mapM and run' in exportEntriesFnEx

1b1d189

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

refactor: extract collectAndGet helper shared by collectAxioms and ex…

2b30bb7

…portEntriesFnEx Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

refactor: add runM helper for CollectAxioms.M

0b6ed77

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

fix: panic instead of silently returning #[] if seen cache is missing

36c1540

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Mar 26, 2026

Update lean-toolchain for leanprover/lean4#13117

4a8fafd

mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Mar 26, 2026

Update lean-toolchain for leanprover/lean4#13117

ff36b0d

nomeata added 2 commits March 26, 2026 12:30

Request a stage0 update

6cf1caf

Remove debugging

7999de4

nomeata and others added 2 commits March 26, 2026 12:52

mathlib-lean-pr-testing bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Mar 26, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: support `#print axioms` under the module system#13117

feat: support `#print axioms` under the module system#13117
nomeata wants to merge 16 commits intonightly-with-mathlibfrom
joachim/module-axioms

nomeata commented Mar 25, 2026 •

edited

Loading

Uh oh!

nomeata commented Mar 25, 2026

Uh oh!

leanprover-radar commented Mar 25, 2026 •

edited

Loading

Uh oh!

nomeata commented Mar 25, 2026

Uh oh!

leanprover-radar commented Mar 25, 2026 •

edited

Loading

Uh oh!

leanprover-bot commented Mar 25, 2026

Uh oh!

mathlib-lean-pr-testing bot commented Mar 25, 2026

Uh oh!

nomeata commented Mar 26, 2026

Uh oh!

leanprover-radar commented Mar 26, 2026 •

edited

Loading

Uh oh!

mathlib-lean-pr-testing bot commented Mar 26, 2026

Uh oh!

nomeata commented Mar 26, 2026

Uh oh!

leanprover-radar commented Mar 26, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

nomeata commented Mar 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

nomeata commented Mar 25, 2026

Uh oh!

leanprover-radar commented Mar 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

nomeata commented Mar 25, 2026

Uh oh!

leanprover-radar commented Mar 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-bot commented Mar 25, 2026

Uh oh!

mathlib-lean-pr-testing bot commented Mar 25, 2026

Uh oh!

nomeata commented Mar 26, 2026

Uh oh!

leanprover-radar commented Mar 26, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mathlib-lean-pr-testing bot commented Mar 26, 2026

Uh oh!

nomeata commented Mar 26, 2026

Uh oh!

leanprover-radar commented Mar 26, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

nomeata commented Mar 25, 2026 •

edited

Loading

leanprover-radar commented Mar 25, 2026 •

edited

Loading

leanprover-radar commented Mar 25, 2026 •

edited

Loading

leanprover-radar commented Mar 26, 2026 •

edited

Loading

leanprover-radar commented Mar 26, 2026 •

edited

Loading