verso icon indicating copy to clipboard operation
verso copied to clipboard

WIP: produce Expr directly for Verso docs instead of term syntax

Open david-christiansen opened this issue 6 months ago • 3 comments

This should decrease build times. For now, this branch is a way to test that.

david-christiansen avatar Jun 25 '25 04:06 david-christiansen

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

david-christiansen avatar Jun 25 '25 04:06 david-christiansen

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.

david-christiansen avatar Jun 25 '25 05:06 david-christiansen

Corresponding branch of reference manual: https://github.com/leanprover/reference-manual/pull/587

robsimmons avatar Sep 18 '25 13:09 robsimmons