smalltt (and Lean) benchmarks

Stream: lean4

[Yuri de Wit]

Just an FYI ...

Found this interesting : smalltt with benchmarks at the end. At best, this could be a source of hot spots for potential improvements other than any kind of real comparison.

In addition, considering the following, Lean seems already quite fast.

The different systems do somewhat different kinds of work. Smalltt and coqtop only elaborate input, while Agda and Idris do module serialization, and Lean apparently does some compilation according to its profiling output. However, the numbers should be still indicative of how much we have to wait to have the entire input available for interactive use