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

[david-christiansen]

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

[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]

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.

[robsimmons]

This could be called "examplesEnv"?

[david-christiansen]

Yes, that's a better name

[robsimmons]

Corresponding branch of reference manual: leanprover/reference-manual#587