Skip to content

feat: add saveModuleDataIncr/readModuleDataIncr with dep region sharing#13185

Open
Kha wants to merge 3 commits intoleanprover:masterfrom
Kha:push-yzvtzvwsznml
Open

feat: add saveModuleDataIncr/readModuleDataIncr with dep region sharing#13185
Kha wants to merge 3 commits intoleanprover:masterfrom
Kha:push-yzvtzvwsznml

Conversation

@Kha
Copy link
Copy Markdown
Member

@Kha Kha commented Mar 30, 2026

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
Copy link
Copy Markdown
Member Author

Kha commented Mar 30, 2026

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Mar 30, 2026 •
edited
Loading

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.

@github-actions 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
@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Mar 30, 2026 •
edited
Loading

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

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 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 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
@mathlib-lean-pr-testing
Copy link
Copy Markdown

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

Mathlib CI status (docs):

@Kha Kha force-pushed the push-yzvtzvwsznml branch from 510303f to 0f23528 Compare March 30, 2026 13:20
@Kha
Copy link
Copy Markdown
Member Author

Kha commented Mar 30, 2026

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Mar 30, 2026 •
edited
Loading

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-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
@mathlib-lean-pr-testing
Copy link
Copy Markdown

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

Mathlib CI status (docs):

@Kha Kha force-pushed the push-yzvtzvwsznml branch from 0f23528 to 752a5e0 Compare March 30, 2026 15:20
@Kha 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
@mathlib-lean-pr-testing
Copy link
Copy Markdown

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

Mathlib CI status (docs):

@Kha 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
@mathlib-lean-pr-testing
Copy link
Copy Markdown

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

Mathlib CI status (docs):

@Kha Kha marked this pull request as ready for review March 31, 2026 09:28
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 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
@mathlib-lean-pr-testing
Copy link
Copy Markdown

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

Mathlib CI status (docs):

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
9804211
@Kha 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
@mathlib-lean-pr-testing
Copy link
Copy Markdown

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

Mathlib CI status (docs):

Kha added 3 commits April 2, 2026 11:25
@Kha
feat: add saveModuleDataIncr/readModuleDataIncr with dep region sharing
ba85c1f 
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, alongside the existing batch saveModuleDataParts API.

Two sharing mechanisms:
- CompactedRegion dep regions for import sharing (address range check
  with rc==0 fast-reject + binary search)
- CompactorState for same-process chaining (pre-loaded obj_table)
@Kha
fix leak
5b085c4
@Kha
fix segfault on relocation
91e27c1
@Kha 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
@leanprover-bot
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 leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label Apr 3, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

builds-manual CI has verified that the Lean Language Reference builds against this PR builds-mathlib CI has verified that Mathlib builds against this PR changelog-other mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN release-ci Enable all CI checks for a PR, like is done for releases toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@Kha @leanprover-radar @leanprover-bot