Benchmark

Stream: general

[Antoine Chambert-Loir]

When I compare the compilation time of the same file on my computer and on that of a colleague, mine looks really slower.
Is there a standard benchmark file that one could run and which could help decide whether there is a CPU/memory problem, or whether I need to keep one smiling at Lean doing nothing visible for 10-30 seconds…
(I've got a 2015 MacBook Pro running MacOS Monterey with a 3.1Ghz iCore 7 and 16GB of memory.)

[Jireh Loreaux]

are you using Lean 3 or Lean 4?

[Antoine Chambert-Loir]

that was in lean 3.