Automated prefix state sharing optimization - #110

Open

augustepoiroux wants to merge 24 commits into

leanprover-community:masterfrom

augustepoiroux:auto-prefix-optimization

Commits on Jul 16, 2026

Improve `LocalContext` and `LocalInstance` extraction for sorries
augustepoiroux
committed
84f9821
Add test
augustepoiroux
committed
b5539d2
Fix test v4.28.0-rc1
augustepoiroux
committed
88643c1
First attempt at doing incremental processing of commands
augustepoiroux
committed
b782b23
Implement incrmental collection of sorries
augustepoiroux
committed
bf335d8
Fix test output
augustepoiroux
committed
d0b990f
Update tests
augustepoiroux
committed
b0058e8
Improving fine-grained environment
augustepoiroux
committed
5d0e118
Revert constant replay
augustepoiroux
committed
a93db5d
Fix v4.22.0-rc2
augustepoiroux
committed
789f087
Fix test v4.24.0-rc1
augustepoiroux
committed
35c2347
Fix test v4.25.0-rc1
augustepoiroux
committed
1065c13
Fix test v4.28.0-rc1
augustepoiroux
committed
0f713f2
Init commit
augustepoiroux
committed
2a69e28
Implement trie-based prefix matching
augustepoiroux
committed
b019882
Add test example
augustepoiroux
committed
ddd16bc
Fix sensitivity to comments and whitespaces in the header
augustepoiroux
committed
7b8e2bb
Fix trie stack overflow issue
augustepoiroux
committed
31b6a52
Make incrementality optional
augustepoiroux
committed
bf7e45b
Update incrementality test
augustepoiroux
committed
7bc1e48
Fix compilation warning
augustepoiroux
committed
b09478e
Fix `trim` -> `trimAscii.toString` (Lean v4.27.0-rc1)
augustepoiroux
committed
a7242fb
Fix test v4.28.0-rc1
augustepoiroux
committed
f02746c
Fix test v4.33.0-rc1
augustepoiroux
committed
6b9582f