Miguel Raz Guzmán Macedo (Oct 11 2019 at 02:35):
Also, are there any benchmarks of performance vs Coq?
Mario Carneiro (Oct 11 2019 at 02:41):
It sounds pretty difficult to make any fair comparison
Mario Carneiro (Oct 11 2019 at 02:42):
there would be a thousand confounding factors in any test
Mario Carneiro (Oct 11 2019 at 02:44):
In my experience I don't think there is an order of magnitude difference in either direction, but I don't think I could get more specific than that
Floris van Doorn (Oct 11 2019 at 05:51):
From my subjective experience, executing a single tactic in Lean is a lot faster than in Coq (I wouldn't be surprised if it was an order of magnitude faster). However, the Coq editor modes (I used CoqIDE, but I believe ProofGeneral works the same) ensure that when you are working on proofs, you rarely rerun your tactics, by storing the state in the middle of your tactic proof. On the other hand in Lean, if you change anything in a proof, it will re-elaborate the whole proof, which negates this speed gain.
Last updated: May 08 2021 at 09:11 UTC