Bas Spitters (May 09 2023 at 09:51): Bas Spitters (May 09 2023 at 09:51):Just curious. Has anyone looked more deeply at this.
https://tarides.com/blog/2022-12-27-love-rust-then-ocaml-s-new-eio-library-is-for-you
It claims ocaml with the speed of rust (minus 3%). So, one could naively dream about Coq at the speed of lean.
Gaëtan Gilbert (May 09 2023 at 10:17):is lean fast?
Karl Palmskog (May 09 2023 at 10:20):circa end of 2021, it wasn't, but maybe this has changed with Lean4 milestones? https://leanprover-community.github.io/blog/posts/backstage-with-dillies/
Another thing is that Lean is slow. I notice that I have an upper bound on my coding speed because it takes a while before Lean updates the goal. And it's really painful when you have to wait 3 seconds at each keystroke. Had it been faster, I could have done some random thing in 10 minutes, but I spent 1h30 instead. And this happens for several reasons: long proofs and long files. If Lean could provide support for more granular recompilation of long proofs, that would be great. By now, many of the large files have been split into smaller pieces, and I am working on some of the remaining ones.
Karl Palmskog (May 09 2023 at 10:22):of course "slow" and "fast" changes with the benchmark, and UI issues may play a role in the quote
Bas Spitters (May 09 2023 at 10:58):I remember, at some point is was claimed to be fast, as it was written in C++, but I've never done any comparison myself.
Karl Palmskog (May 09 2023 at 11:03):Lean4 to my knowledge is mostly implemented in Lean(4)
Karl Palmskog (May 09 2023 at 11:05):it would be nice to have a benchmark suite for the "same" big definitions/proofs in comparable systems, e.g., Agda/Coq/Lean. But chance of getting research funding to develop this is probably around zero.
Typeclass resolution / unification are specific examples that come to mind on what to [performance] test.
Paolo Giarrusso (May 09 2023 at 11:07):That blog posts has strong hints that it's about async code for highly concurrent servers
Karl Palmskog (May 09 2023 at 11:08):I once tried to see if anyone had even done a proper software engineering style performance comparison of name binding approaches. Couldn't find any, e.g., de Bruijn only vs. locally nameless on huge terms
Yannick Zakowski (May 09 2023 at 11:17):Not in the context of proof assistants per se, but Stephanie Weirich has done this experiment to try to benchmark capture avoiding substitution implemented in various ways (after an earlier similar experiment by Lennart Augustsson):
https://github.com/sweirich/lambda-n-ways
Pierre-Marie Pédrot (May 09 2023 at 11:48):@Bas Spitters this seems to be a library for IO, which is not the main throttle of Coq processes. Coq is heavily memory-bound, not IO-bound, so this probably wouldn't change anything.
Pierre-Marie Pédrot (May 09 2023 at 11:50):Also, re: lean, I discovered recently that the Lean kernel uses a naive reduction machine (read: O(n) eager substitution) so there is no way this can be fast on non-trivial conversion problems. It seems that the mathlib style works around these issues by relying on HOL-style proofs, but still.
Bas Spitters (May 09 2023 at 14:02):@Pierre-Marie Pédrot Thanks! I may have misread, but I understood that this is about concurrency. Your arguments will likely still apply.
It's build on ocaml 5. I know that ocaml 5.0 slowed down coq, quite a bit. I believe this has been resolved now, but you'll certainly know more than I do.
Michael Soegtrop (May 10 2023 at 11:04):My five cents: I am usually very impressed by the speed of Coq. With reflexive tactics it can do quite complicated proofs in a fraction of a second.
Last updated: Nov 29 2023 at 21:01 UTC