max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/compile
History
Exact
Sebastian Ullrich 895752dc2e
feat: add Lean.CompactedRegion.save/read supporting cross-file object sharing (#13185) 
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`)
2026-05-16 12:53:20 +00:00
..
.gitignore feat: add Lean.CompactedRegion.save/read supporting cross-file object sharing (#13185) 2026-05-16 12:53:20 +00:00
534.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
534.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
append.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
append.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
arity_bug1.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
arity_bug1.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
array.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
array.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
array_test.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
array_test.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
array_test2.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
arrayMk.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
arrayMk.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
bigctor.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
bigctor.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
bytearray_bug.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
bytearray_bug.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
char_escape.lean fix: handling of EmitC for small hex string literals (#13435) 2026-04-17 15:16:28 +00:00
char_escape.lean.out.expected fix: handling of EmitC for small hex string literals (#13435) 2026-04-17 15:16:28 +00:00
closure_bug1.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
closure_bug1.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
closure_bug2.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
closure_bug2.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
closure_bug3.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
closure_bug3.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
closure_bug4.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
closure_bug4.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
closure_bug5.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
closure_bug5.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
closure_bug6.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
closure_bug6.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
closure_bug7.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
closure_bug7.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
closure_bug8.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
closure_bug8.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
compactor_chain.lean feat: add Lean.CompactedRegion.save/read supporting cross-file object sharing (#13185) 2026-05-16 12:53:20 +00:00
compactor_chain.lean.no_compile feat: add Lean.CompactedRegion.save/read supporting cross-file object sharing (#13185) 2026-05-16 12:53:20 +00:00
dep_regions.lean feat: add Lean.CompactedRegion.save/read supporting cross-file object sharing (#13185) 2026-05-16 12:53:20 +00:00
dep_regions.lean.no_compile feat: add Lean.CompactedRegion.save/read supporting cross-file object sharing (#13185) 2026-05-16 12:53:20 +00:00
dep_regions_miss.lean feat: add Lean.CompactedRegion.save/read supporting cross-file object sharing (#13185) 2026-05-16 12:53:20 +00:00
dep_regions_miss.lean.no_compile feat: add Lean.CompactedRegion.save/read supporting cross-file object sharing (#13185) 2026-05-16 12:53:20 +00:00
escape.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
escape.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
expr.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
expr.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
extractClosedMutualBlock.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
extractClosedMutualBlock.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
file_read_overflow.lean fix: file read buffer overflow (#13392) 2026-04-13 17:56:27 +00:00
float.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
float.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
float_cases_bug.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
float_cases_bug.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
init.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
init.lean.no_interpret chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
init.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
initUnboxed.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
initUnboxed.lean.no_interpret chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
initUnboxed.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
large_closure_bug.lean feat: add instance validation checks in addInstance (#13389) 2026-04-16 17:48:16 +00:00
large_closure_bug.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
lazylist.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
lazylist.lean.no_interpret chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
lazylist.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
link_lake.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
map_big.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
map_big.lean.no_interpret chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
map_big.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
module.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
module.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
nat_shiftr.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
nat_shiftr.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
overflow1.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
overflow1.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
overflow2.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
overflow2.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
overflow3.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
overflow3.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
partial.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
partial.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
phashmap.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
phashmap.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
phashmap2.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
phashmap2.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
phashmap3.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
phashmap3.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
print_error.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
print_error.lean.init.sh chore: migrate pkg tests (#12889) 2026-03-11 18:55:46 +00:00
print_error.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
qsortBadLt.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
qsortBadLt.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
rbmap_library.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
rbmap_library.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
reduceArity_overapp.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
reduceArity_overapp.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
reusebug.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
reusebug.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
run_bench.sh feat: add Lean.CompactedRegion.save/read supporting cross-file object sharing (#13185) 2026-05-16 12:53:20 +00:00
run_test.sh chore: fixes from #13103 "enable separate codegen" (#13241) 2026-04-02 11:13:22 +00:00
StackOverflow.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
StackOverflow.lean.init.sh chore: migrate pkg tests (#12889) 2026-03-11 18:55:46 +00:00
StackOverflow.lean.no_interpret chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
StackOverflow.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
StackOverflowTask.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
StackOverflowTask.lean.init.sh chore: migrate pkg tests (#12889) 2026-03-11 18:55:46 +00:00
StackOverflowTask.lean.no_interpret chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
StackOverflowTask.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
str.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
str.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
strictAndOr.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
strictAndOr.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
t1.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
t1.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
t2.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
t2.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
t4.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
t4.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
thunk.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
thunk.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
trie.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
trie.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
trigraphs.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
trigraphs.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
tuple.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
tuple.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
typeFormerPolymorphism.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
typeFormerPolymorphism.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
uint_fold.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
uint_fold.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
unreachable.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
uset.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
uset.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
utf8Path.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
utf8Path.lean.英語 chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
wait_dedicated.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
wait_dedicated.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00