perf: bundle `Init` into a single big .olean file #11965

Kha · 2026-01-10T11:08:49Z

This PR optimizes file operations and size for importing Init by bundling all its module files into a single file with cross-sharing. Specifically, it reduces the cumulative size from 325MB to 264MB and openat calls for import Init on Linux from ~2000 to ~80.

TODO:

Think about Lake integration
Think about module system interaction
Think about what to do when submodules are visited before bundle main module

leanprover-bot · 2026-01-13T10:16:03Z

Reference manual CI status:

✅ Reference manual branch lean-pr-testing-11965 has successfully built against this PR. (2026-01-13 10:16:01) View Log
🟡 Reference manual branch lean-pr-testing-11965 build against this PR didn't complete normally. (2026-01-13 10:16:27) View Log
✅ Reference manual branch lean-pr-testing-11965 has successfully built against this PR. (2026-01-14 15:56:18) View Log
🟡 Reference manual branch lean-pr-testing-11965 build against this PR didn't complete normally. (2026-01-14 15:57:41) View Log

Kha · 2026-01-13T12:51:44Z

!bench

leanprover-radar · 2026-01-13T12:51:50Z

Benchmark results for b24acae against d92cdae are in! @Kha

Warnings (2)

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

Runner for run build has different system configurations between commits.
Runner for run other has different system configurations between commits.

Runs (1🟥)

🟥 build exited with code 1

Large changes (7✅)

✅ big_do//instructions: -152.5M (-0.5%)
✅ grind_ring_5.lean//instructions: -124.0M (-1.3%)
✅ import Lean//instructions: -91.9M (-4.8%)
✅ iterators (elab)//instructions: -118.4M (-3.1%)
✅ iterators (interpreted)//instructions: -343.9M (-1.0%)
✅ lake build clean//instructions: -225.6G (-10.5%)
✅ omega_stress.lean async//instructions: -129.4M (-2.4%)

Medium changes (20✅)

✅ big_beq//instructions: -114.8M (-1.0%)
✅ big_beq_rec//instructions: -116.3M (-0.5%)
✅ big_deceq//instructions: -117.4M (-2.3%)
✅ big_deceq_rec//instructions: -117.3M (-1.6%)
✅ big_match//instructions: -119.6M (-1.0%)
✅ big_match_nat//instructions: -117.1M (-1.5%)
✅ big_match_nat_split//instructions: -115.4M (-0.8%)
✅ big_match_partial//instructions: -114.5M (-0.6%)
✅ big_omega.lean MT//instructions: -193.7M (-0.7%)
✅ big_omega.lean//instructions: -192.4M (-0.7%)
✅ bv_decide_rewriter.lean//instructions: -152.4M (-1.0%)
✅ grind_bitvec2.lean//instructions: -1.4G (-0.7%)
✅ lake config elab//instructions: -116.7M (-3.7%)
✅ lake config import//instructions: -112.5M (-7.5%)
✅ lake config tree//instructions: -111.8M (-7.3%)
✅ lake env//instructions: -121.2M (-8.0%)
✅ mut_rec_wf//instructions: -152.1M (-0.5%)
✅ reduceMatch//instructions: -129.8M (-0.7%)
✅ simp_arith1//instructions: -116.2M (-3.6%)
✅ tests/bench/ interpreted//instructions: -2.4G (-1.1%)

Small changes (11✅)

✅ bv_decide_large_aig.lean//instructions: -160.2M (-0.4%)
✅ bv_decide_mul//instructions: -97.6M (-0.2%)
✅ charactersIn//instructions: -88.9M (-0.2%)
✅ grind_list2.lean//instructions: -333.0M (-0.5%)
✅ identifier auto-completion//instructions: -130.3M (-0.2%)
✅ lake build no-op//instructions: -114.9M (-1.9%)
✅ simp_bubblesort_256//instructions: -123.4M (-0.8%)
✅ simp_congr//instructions: -118.5M (-1.1%)
✅ simp_local//instructions: -107.8M (-0.2%)
✅ simp_subexpr//instructions: -115.6M (-0.7%)
✅ workspaceSymbols//instructions: -84.8M (-0.3%)

Kha · 2026-01-14T12:54:01Z

!bench

leanprover-radar · 2026-01-14T12:54:12Z

Benchmark results for 71ad73c against d92cdae are in! @Kha

Warnings (2)

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

Runner for run build has different system configurations between commits.
Runner for run other has different system configurations between commits.

Runs (1🟥)

🟥 build exited with code 1

Large changes (8✅)

✅ big_do//instructions: -154.6M (-0.5%)
✅ grind_ring_5.lean//instructions: -117.2M (-1.2%)
✅ import Lean//instructions: -91.1M (-4.8%)
✅ iterators (elab)//instructions: -118.2M (-3.1%)
✅ iterators (interpreted)//instructions: -343.3M (-1.0%)
✅ lake build clean//instructions: -224.4G (-10.5%)
✅ omega_stress.lean async//instructions: -128.8M (-2.4%)
✅ tests/bench/ interpreted//instructions: -2.4G (-1.1%)

Medium changes (19✅)

✅ big_beq//instructions: -116.9M (-1.0%)
✅ big_beq_rec//instructions: -113.7M (-0.5%)
✅ big_deceq//instructions: -117.8M (-2.3%)
✅ big_deceq_rec//instructions: -117.0M (-1.6%)
✅ big_match//instructions: -119.9M (-1.0%)
✅ big_match_nat//instructions: -116.9M (-1.5%)
✅ big_match_nat_split//instructions: -115.9M (-0.8%)
✅ big_match_partial//instructions: -112.3M (-0.6%)
✅ big_omega.lean MT//instructions: -188.0M (-0.7%)
✅ big_omega.lean//instructions: -195.9M (-0.7%)
✅ bv_decide_rewriter.lean//instructions: -156.1M (-1.0%)
✅ grind_bitvec2.lean//instructions: -1.4G (-0.7%)
✅ lake config elab//instructions: -116.9M (-3.7%)
✅ lake config import//instructions: -112.9M (-7.6%)
✅ lake config tree//instructions: -111.3M (-7.3%)
✅ lake env//instructions: -119.8M (-7.9%)
✅ mut_rec_wf//instructions: -148.2M (-0.5%)
✅ reduceMatch//instructions: -134.7M (-0.7%)
✅ simp_arith1//instructions: -119.5M (-3.8%)

Small changes (11✅)

✅ bv_decide_large_aig.lean//instructions: -158.3M (-0.4%)
✅ bv_decide_mul//instructions: -112.7M (-0.2%)
✅ charactersIn//instructions: -87.2M (-0.2%)
✅ grind_list2.lean//instructions: -334.5M (-0.5%)
✅ identifier auto-completion//instructions: -128.0M (-0.2%)
✅ lake build no-op//instructions: -111.6M (-1.8%)
✅ simp_bubblesort_256//instructions: -116.6M (-0.8%)
✅ simp_congr//instructions: -114.7M (-1.0%)
✅ simp_local//instructions: -103.6M (-0.2%)
✅ simp_subexpr//instructions: -101.5M (-0.7%)
✅ workspaceSymbols//instructions: -79.9M (-0.3%)

Kha · 2026-01-14T13:30:16Z

!bench

leanprover-radar · 2026-01-14T13:30:26Z

Benchmark results for a165160 against d92cdae are in! @Kha

Warnings (2)

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

Runner for run build has different system configurations between commits.
Runner for run other has different system configurations between commits.

Runs (1🟥)

🟥 build exited with code 1

Large changes (8✅)

✅ big_do//instructions: -154.3M (-0.5%)
✅ grind_ring_5.lean//instructions: -124.4M (-1.3%)
✅ import Lean//instructions: -89.4M (-4.7%)
✅ iterators (elab)//instructions: -118.0M (-3.1%)
✅ iterators (interpreted)//instructions: -344.2M (-1.0%)
✅ lake build clean//instructions: -223.2G (-10.4%)
✅ omega_stress.lean async//instructions: -127.0M (-2.3%)
✅ tests/bench/ interpreted//instructions: -2.4G (-1.1%)

Medium changes (19✅)

✅ big_beq//instructions: -115.2M (-1.0%)
✅ big_beq_rec//instructions: -114.4M (-0.5%)
✅ big_deceq//instructions: -117.3M (-2.3%)
✅ big_deceq_rec//instructions: -117.3M (-1.6%)
✅ big_match//instructions: -120.5M (-1.0%)
✅ big_match_nat//instructions: -117.0M (-1.5%)
✅ big_match_nat_split//instructions: -115.8M (-0.8%)
✅ big_match_partial//instructions: -112.8M (-0.6%)
✅ big_omega.lean MT//instructions: -187.1M (-0.7%)
✅ big_omega.lean//instructions: -192.9M (-0.7%)
✅ bv_decide_rewriter.lean//instructions: -154.6M (-1.0%)
✅ grind_bitvec2.lean//instructions: -1.4G (-0.7%)
✅ lake config elab//instructions: -117.0M (-3.7%)
✅ lake config import//instructions: -112.5M (-7.5%)
✅ lake config tree//instructions: -111.6M (-7.3%)
✅ lake env//instructions: -121.5M (-8.0%)
✅ mut_rec_wf//instructions: -150.4M (-0.5%)
✅ reduceMatch//instructions: -129.3M (-0.7%)
✅ simp_arith1//instructions: -115.8M (-3.6%)

Small changes (11✅)

✅ bv_decide_large_aig.lean//instructions: -169.0M (-0.4%)
✅ bv_decide_mul//instructions: -111.0M (-0.2%)
✅ charactersIn//instructions: -90.2M (-0.2%)
✅ grind_list2.lean//instructions: -332.2M (-0.5%)
✅ identifier auto-completion//instructions: -132.4M (-0.2%)
✅ lake build no-op//instructions: -117.9M (-1.9%)
✅ simp_bubblesort_256//instructions: -115.0M (-0.8%)
✅ simp_congr//instructions: -118.8M (-1.1%)
✅ simp_local//instructions: -108.6M (-0.2%)
✅ simp_subexpr//instructions: -95.5M (-0.6%)
✅ workspaceSymbols//instructions: -86.5M (-0.3%)

Kha · 2026-01-14T14:14:19Z

!bench

leanprover-radar · 2026-01-14T14:14:27Z

Benchmark results for dc05e0b against d92cdae are in! @Kha

Warnings (2)

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

Runner for run build has different system configurations between commits.
Runner for run other has different system configurations between commits.

Large changes (8✅)

✅ big_do//instructions: -154.9M (-0.5%)
✅ grind_ring_5.lean//instructions: -116.9M (-1.2%)
✅ import Lean//instructions: -90.9M (-4.8%)
✅ iterators (elab)//instructions: -118.0M (-3.1%)
✅ iterators (interpreted)//instructions: -343.7M (-1.0%)
✅ lake build clean//instructions: -225.0G (-10.5%)
✅ omega_stress.lean async//instructions: -130.0M (-2.4%)
✅ tests/bench/ interpreted//instructions: -2.4G (-1.1%)

Medium changes (19✅)

✅ big_beq//instructions: -113.3M (-1.0%)
✅ big_beq_rec//instructions: -112.7M (-0.5%)
✅ big_deceq//instructions: -118.3M (-2.3%)
✅ big_deceq_rec//instructions: -117.7M (-1.6%)
✅ big_match//instructions: -119.7M (-1.0%)
✅ big_match_nat//instructions: -117.4M (-1.5%)
✅ big_match_nat_split//instructions: -115.8M (-0.8%)
✅ big_match_partial//instructions: -116.4M (-0.6%)
✅ big_omega.lean MT//instructions: -191.0M (-0.7%)
✅ big_omega.lean//instructions: -191.2M (-0.7%)
✅ bv_decide_rewriter.lean//instructions: -154.6M (-1.0%)
✅ grind_bitvec2.lean//instructions: -1.4G (-0.7%)
✅ lake config elab//instructions: -116.7M (-3.7%)
✅ lake config import//instructions: -112.5M (-7.5%)
✅ lake config tree//instructions: -111.4M (-7.3%)
✅ lake env//instructions: -120.8M (-8.0%)
✅ mut_rec_wf//instructions: -146.8M (-0.5%)
✅ reduceMatch//instructions: -129.9M (-0.7%)
✅ simp_arith1//instructions: -115.7M (-3.6%)

Small changes (24✅, 7🟥)

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

leanprover-community-bot · 2026-01-14T16:53:45Z

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-11965 build failed against this PR. (2026-01-14 16:53:43) View Log
✅ Mathlib branch lean-pr-testing-11965 has successfully built against this PR. (2026-01-15 13:15:34) View Log

Kha · 2026-01-15T14:18:00Z

!bench mathlib

leanprover-radar · 2026-01-15T14:18:17Z

Benchmark results for leanprover-community/mathlib4-nightly-testing@d8627a2 against leanprover-community/mathlib4-nightly-testing@160f573 are in! @Kha

Warnings (2)

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

Runner for run main has different system configurations between commits.
Runners for run main differ between commits.

No significant changes detected.

Kha force-pushed the push-rnszpsskxkqq branch from fae7866 to 876ac4d Compare January 12, 2026 15:07

perf: bundle Init into a single big .olean file

1ffc3da

Kha force-pushed the push-rnszpsskxkqq branch from 876ac4d to 1ffc3da Compare January 12, 2026 21:43

fix

b24acae

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

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 13, 2026

Update lean-toolchain for testing leanprover/lean4#11965

4d0fe35

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 Jan 13, 2026

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jan 13, 2026

Update lean-toolchain for testing leanprover/lean4#11965

eb7ff0c

leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Jan 13, 2026

Update lean-toolchain for testing leanprover/lean4#11965

7f4d909

leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label Jan 13, 2026

fix bench

dc05e0b

Kha force-pushed the push-rnszpsskxkqq branch from cbdcc9f to dc05e0b Compare January 14, 2026 14:13

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 14, 2026

Update lean-toolchain for leanprover/lean4#11965

53d61c1

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jan 14, 2026

Update lean-toolchain for leanprover/lean4#11965

91e9674

leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Jan 14, 2026

Update lean-toolchain for leanprover/lean4#11965

e86782f

leanprover-community-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Jan 14, 2026

leanprover-community-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 Jan 15, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

perf: bundle `Init` into a single big .olean file #11965

perf: bundle `Init` into a single big .olean file #11965

Kha commented Jan 10, 2026 •

edited

Loading

Uh oh!

leanprover-bot commented Jan 13, 2026 •

edited

Loading

Uh oh!

Kha commented Jan 13, 2026

Uh oh!

leanprover-radar commented Jan 13, 2026 •

edited

Loading

Uh oh!

Kha commented Jan 14, 2026

Uh oh!

leanprover-radar commented Jan 14, 2026 •

edited

Loading

Uh oh!

Kha commented Jan 14, 2026

Uh oh!

leanprover-radar commented Jan 14, 2026 •

edited

Loading

Uh oh!

Kha commented Jan 14, 2026

Uh oh!

leanprover-radar commented Jan 14, 2026 •

edited

Loading

Uh oh!

leanprover-community-bot commented Jan 14, 2026 •

edited

Loading

Uh oh!

Kha commented Jan 15, 2026

Uh oh!

leanprover-radar commented Jan 15, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

perf: bundle Init into a single big .olean file #11965

Are you sure you want to change the base?

perf: bundle Init into a single big .olean file #11965

Conversation

Kha commented Jan 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-bot commented Jan 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Kha commented Jan 13, 2026

Uh oh!

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

Uh oh!

Uh oh!

Kha commented Jan 14, 2026

Uh oh!

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

Uh oh!

Uh oh!

Kha commented Jan 14, 2026

Uh oh!

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

Uh oh!

Uh oh!

Kha commented Jan 14, 2026

Uh oh!

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

Uh oh!

Uh oh!

leanprover-community-bot commented Jan 14, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Kha commented Jan 15, 2026

Uh oh!

leanprover-radar commented Jan 15, 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!

4 participants

perf: bundle `Init` into a single big .olean file #11965

perf: bundle `Init` into a single big .olean file #11965

Kha commented Jan 10, 2026 •

edited

Loading

leanprover-bot commented Jan 13, 2026 •

edited

Loading

leanprover-radar commented Jan 13, 2026 •

edited

Loading

leanprover-radar commented Jan 14, 2026 •

edited

Loading

leanprover-radar commented Jan 14, 2026 •

edited

Loading

leanprover-radar commented Jan 14, 2026 •

edited

Loading

leanprover-community-bot commented Jan 14, 2026 •

edited

Loading

leanprover-radar commented Jan 15, 2026 •

edited

Loading