feat: add `Lean.CompactedRegion.save`/`read` supporting cross-file object sharing by Kha · Pull Request #13185 · leanprover/lean4

Kha · 2026-03-30T08:59:11Z

This PR adds new incremental module serialization functions that save/load a single module at a time with explicit sharing via dep regions and compactor state, generalizing the existing batch saveModuleDataParts API.

Two sharing mechanisms that can be mixed:

CompactedRegion dep regions for sharing with loaded regions
CompactorState for same-process chaining (pre-loaded m_obj_table)

Kha · 2026-03-30T08:59:17Z

!bench

leanprover-radar · 2026-03-30T08:59:26Z

Benchmark results for 510303f against 4786e08 are in. Significant changes detected! @Kha

🟥 build//instructions: +17.1G (+0.14%)
🟥 other exited with code 2

Large changes (5🟥)

🟥 size/Init/.olean.private//bytes: +42MiB (+17.46%)
🟥 size/Init/.olean.server//bytes: +7MiB (+69.46%)
🟥 size/all/.olean.private//bytes: +143MiB (+11.98%)
🟥 size/all/.olean.server//bytes: +23MiB (+82.96%)
🟥 size/install//bytes: +166MiB (+6.77%)

Small changes (51🟥)

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

leanprover-bot · 2026-03-30T09:59:44Z

Reference manual CI status:

❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-25 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-30 09:59:44)
✅ Reference manual branch lean-pr-testing-13185 has successfully built against this PR. (2026-04-03 10:24:49) View Log
🟡 Reference manual branch lean-pr-testing-13185 build against this PR didn't complete normally. (2026-04-03 10:25:50) View Log
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 8c82f9ed4ae09b165342b24a6461ccc097caae50 --onto ed0d50fcf0efa8c9a32e1ccb3603ce43edce6926. You can force reference manual CI using the force-manual-ci label. (2026-05-13 17:37:07)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 8c82f9ed4ae09b165342b24a6461ccc097caae50 --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-05-14 14:36:12)

mathlib-lean-pr-testing · 2026-03-30T10:45:14Z

Mathlib CI status (docs):

❌ Mathlib branch lean-pr-testing-13185 built against this PR, but linting failed. (2026-03-30 10:45:12) View Log
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 8c82f9ed4ae09b165342b24a6461ccc097caae50 --onto ed0d50fcf0efa8c9a32e1ccb3603ce43edce6926. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-13 17:37:05)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 8c82f9ed4ae09b165342b24a6461ccc097caae50 --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-14 14:36:09)

Kha · 2026-03-30T13:20:24Z

!bench

leanprover-radar · 2026-03-30T13:20:47Z

Benchmark results for 0f23528 against 4786e08 are in. There are no significant changes. @Kha

🟥 build//instructions: +98.6M (+0.00%)

Small changes (2🟥)

🟥 build/module/Lean.Environment//instructions: +120.3M (+0.73%)
🟥 elab/big_beq_rec//task-clock: +36ms (+2.76%)

mathlib-lean-pr-testing · 2026-03-30T15:18:07Z

Mathlib CI status (docs):

❌ Mathlib branch lean-pr-testing-13185 built against this PR, but testing failed. (2026-03-30 15:18:05) View Log

mathlib-lean-pr-testing · 2026-03-30T18:22:59Z

Mathlib CI status (docs):

❌ Mathlib branch lean-pr-testing-13185 built against this PR, but testing failed. (2026-03-30 18:22:58) View Log

mathlib-lean-pr-testing · 2026-03-30T22:13:28Z

Mathlib CI status (docs):

❌ Mathlib branch lean-pr-testing-13185 built against this PR, but testing failed. (2026-03-30 22:13:26) View Log

mathlib-lean-pr-testing · 2026-04-01T11:18:15Z

Mathlib CI status (docs):

✅ Mathlib branch lean-pr-testing-13185 has successfully built against this PR. (2026-04-01 11:18:13) View Log

mathlib-lean-pr-testing · 2026-04-03T11:15:17Z

Mathlib CI status (docs):

✅ Mathlib branch lean-pr-testing-13185 has successfully built against this PR. (2026-04-03 11:15:15) View Log

Kha · 2026-05-13T15:59:52Z

!bench

leanprover-radar · 2026-05-13T16:00:20Z

Benchmark results for d14a467 against 8c82f9e are in. There are significant results. @Kha

🟥 build//instructions: +3.7G (+0.03%)

Large changes (1🟥)

🟥 size/compile/.out//bytes: +211MiB (+10.72%)

Small changes (2✅, 3🟥)

🟥 build/module/Lean.Environment//instructions: +84.3M (+0.57%)
🟥 elab/bv_decide_large_aig//instructions: +248.1M (+0.62%)
✅ misc/import Lean//instructions: -7.2M (-0.48%)
✅ misc/import Std.Data.Internal.List.Associative//task-clock: -779ms (-7.18%)
🟥 size/all/.cpp//lines: +90.0 (+0.31%)

Kha · 2026-05-14T20:27:01Z

!bench

leanprover-radar · 2026-05-14T20:27:07Z

Benchmark results for 95e7047 against 8c82f9e are in. There are significant results. @Kha

🟥 build//instructions: +3.7G (+0.03%)

Large changes (1🟥)

🟥 size/compile/.out//bytes: +211MiB (+10.72%)

Small changes (1✅, 3🟥)

🟥 build/module/Lean.Environment//instructions: +111.0M (+0.75%)
🟥 elab/bv_decide_large_aig//instructions: +227.7M (+0.57%)
✅ elab/grind_bitvec2//task-clock: -2s (-6.66%)
🟥 size/all/.cpp//lines: +90.0 (+0.31%)

This PR adds `Lean.CompactedRegion.save` and `Lean.CompactedRegion.read` as the primary low-level olean save/load primitives, generic in the serialized data type. The existing `ModuleData`-typed functions (`saveModuleData`/`readModuleData` and the `*Parts` variants) become thin wrappers around them. Two sharing mechanisms are supported: * `CompactedRegion` dep regions: objects already present in a loaded dep region are emitted as cross-region pointers rather than re-serialized, and the loader's `fix_object_ptr` resolves them via a binary search over deps sorted by saved `base_addr`. * A `Compactor` chaining handle: consecutive saves with the same `Compactor` reuse the prior call's pointer-identity and structural-sharing tables so objects shared across parts are emitted exactly once. The reader maps oleans `MAP_PRIVATE | PROT_READ | PROT_WRITE` so the pointer-fixup walk can write the loaded buffer in place when needed (`MAP_PRIVATE` keeps unwritten pages shared with the page cache, so the write protection is free when no fixup happens). On Linux, `MAP_FIXED_NOREPLACE` is OR'd in when available (with a `#define` fallback for older glibc) to let the kernel atomically reject collisions at the saved `base_addr`; macOS doesn't expose the flag, and the post-check + cleanup `munmap` handles the same case there. The fast path in `compacted_region::read()` skips the full object walk when both the region itself and every dep region landed at their saved addresses; otherwise it falls through to the full fix-up walk. The `compacted_region` constructor rejects overlapping saved `base_addr` ranges to avoid silent translation through the wrong region.

… tests `tests/compile/run_bench.sh` only emitted `<test>.measurements.jsonl` from the `if [[ -n $DO_COMPILE ]]` block, and the earlier `rm -f` removed any stale file. With `.no_compile` set, the file never existed, and `combine.py` later crashed with `FileNotFoundError` when reading the expected per-test jsonl. Truncate-or-create the file unconditionally before the block so an empty measurements file is always available.

Kha · 2026-05-16T11:21:52Z

 fi

-rm -f "$1.measurements.jsonl"
+: > "$1.measurements.jsonl"  # always create (possibly empty) so `combine.py` finds it


FYI @Garmelon; not sure using .no_compile in compile/ really is the best approach, could be a new pile run/ instead?

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

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

Update lean-toolchain for testing leanprover/lean4#13185

7d9bfaf

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 30, 2026

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

Update lean-toolchain for testing leanprover/lean4#13185

ab56571

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 30, 2026

Kha force-pushed the push-yzvtzvwsznml branch from 510303f to 0f23528 Compare March 30, 2026 13:20

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

Update lean-toolchain for leanprover/lean4#13185

6989b6a

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

Update lean-toolchain for leanprover/lean4#13185

0b990f9

Kha force-pushed the push-yzvtzvwsznml branch from 0f23528 to 752a5e0 Compare March 30, 2026 15:20

Kha added the release-ci Enable all CI checks for a PR, like is done for releases label Mar 30, 2026

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

Update lean-toolchain for leanprover/lean4#13185

049a276

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

Update lean-toolchain for leanprover/lean4#13185

a5fe6b7

Kha force-pushed the push-yzvtzvwsznml branch from 5d58fca to c82dd26 Compare March 30, 2026 19:05

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

Update lean-toolchain for leanprover/lean4#13185

de9cf04

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

Update lean-toolchain for leanprover/lean4#13185

4921837

Kha marked this pull request as ready for review March 31, 2026 09:28

Kha added the changelog-other label Mar 31, 2026

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

Update lean-toolchain for leanprover/lean4#13185

283bcc7

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

Update lean-toolchain for leanprover/lean4#13185

ef788b9

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 31, 2026

Kha force-pushed the push-yzvtzvwsznml branch from 360f75a to 0849a2b Compare April 1, 2026 08:33

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 1, 2026

Update lean-toolchain for leanprover/lean4#13185

6d7e61d

mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 1, 2026

Update lean-toolchain for leanprover/lean4#13185

ac031f7

Kha force-pushed the push-yzvtzvwsznml branch from 0849a2b to 91e27c1 Compare April 3, 2026 08:41

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 3, 2026

Update lean-toolchain for leanprover/lean4#13185

44a628a

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

Update lean-toolchain for testing leanprover/lean4#13185

866bf4c

mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 3, 2026

Update lean-toolchain for leanprover/lean4#13185

e4ac2e1

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

Kha force-pushed the push-yzvtzvwsznml branch 2 times, most recently from 17a86da to d14a467 Compare May 13, 2026 15:47

Kha force-pushed the push-yzvtzvwsznml branch from d14a467 to 95e7047 Compare May 14, 2026 12:33

Kha force-pushed the push-yzvtzvwsznml branch from 95e7047 to 59b9ac3 Compare May 15, 2026 12:12

Kha enabled auto-merge May 15, 2026 12:12

Kha changed the title ~~feat: add saveModuleDataIncr/readModuleDataIncr with dep region sharing~~ feat: add Lean.CompactedRegion.save/read supporting cross-file object sharing May 15, 2026

Kha force-pushed the push-yzvtzvwsznml branch from 59b9ac3 to fc26234 Compare May 15, 2026 12:19

Kha added 2 commits May 16, 2026 10:42

Kha force-pushed the push-yzvtzvwsznml branch 2 times, most recently from 8100976 to e609d91 Compare May 16, 2026 11:17

Kha commented May 16, 2026

View reviewed changes

Kha added this pull request to the merge queue May 16, 2026

Merged via the queue into leanprover:master with commit 895752d May 16, 2026
22 checks passed

Kha deleted the push-yzvtzvwsznml branch May 29, 2026 09:30

Conversation

Kha commented Mar 30, 2026

Uh oh!

Kha commented Mar 30, 2026

Uh oh!

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

Uh oh!

Uh oh!

leanprover-bot commented Mar 30, 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 30, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Kha commented Mar 30, 2026

Uh oh!

leanprover-radar commented Mar 30, 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 30, 2026

Uh oh!

mathlib-lean-pr-testing Bot commented Mar 30, 2026

Uh oh!

mathlib-lean-pr-testing Bot commented Mar 30, 2026

Uh oh!

mathlib-lean-pr-testing Bot commented Apr 1, 2026

Uh oh!

mathlib-lean-pr-testing Bot commented Apr 3, 2026

Uh oh!

Kha commented May 13, 2026

Uh oh!

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

Uh oh!

Uh oh!

Kha commented May 14, 2026

Uh oh!

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

Uh oh!

Uh oh!

Kha May 16, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

leanprover-radar commented Mar 30, 2026 •

edited

Loading

leanprover-bot commented Mar 30, 2026 •

edited

Loading

mathlib-lean-pr-testing Bot commented Mar 30, 2026 •

edited

Loading

leanprover-radar commented Mar 30, 2026 •

edited

Loading

leanprover-radar commented May 13, 2026 •

edited

Loading

leanprover-radar commented May 14, 2026 •

edited

Loading