verso
verso copied to clipboard
WIP: produce Expr directly for Verso docs instead of term syntax
This should decrease build times. For now, this branch is a way to test that.
Unfortunately, building the manual did not get faster. On main, it's:
Executed in 173.53 secs fish external
usr time 23.52 mins 0.18 millis 23.52 mins
sys time 1.18 mins 1.45 millis 1.18 mins
On this branch, it's:
Executed in 239.06 secs fish external
usr time 28.01 mins 0.25 millis 28.01 mins
sys time 1.29 mins 1.36 millis 1.29 mins
OTOH, elaboration time did improve. With just building oleans, this branch gives:
Executed in 106.62 secs fish external
usr time 789.05 secs 0.24 millis 789.05 secs
sys time 56.35 secs 1.75 millis 56.35 secs
while main gives
Executed in 124.79 secs fish external
usr time 15.96 mins 0.28 millis 15.96 mins
sys time 0.97 mins 2.18 millis 0.97 mins
so this branch is worth testing with the new compiler.
Corresponding branch of reference manual: https://github.com/leanprover/reference-manual/pull/587