feat: lake: `precompileLibrary` & `precompileImports` - #15015

Merged

tydeu merged 5 commits into

leanprover:masterfrom

tydeu:lake/precompile-split

Sep 5, 2026

Commits on Sep 4, 2026

feat: lake: `precompileLibrary`

tydeu
and
claude
committed
d92888b
feat: lake: `precompileImports`

tydeu
and
claude
committed
1a31150
refactor: simplify `shouldPrecompileSelf` to `shouldPrecompile`
tydeu
committed
84ac79e
chore: add new options to TOML schema

tydeu
and
claude
committed
a9a452f
refactor: simplify `computePrecompileImportsAux`
tydeu
committed
77bef28