Btw, would you suggest to turn on more options besides flambda
? I've seen some mentions that fp
could also be beneficial for Coq.
@Alexander Gryzlov it's well known that the 32-bit OCaml compiler leads to much faster Coq checking than the 64-bit one, but may be inconvenient to set up
Really? That's very interesting. Much as in more than a handful of percents? Is it because of the memory pressure?
see discussion here, if I remember correctly it's definitely > 10% speedup: https://coq.zulipchat.com/#narrow/stream/250632-Coq-Platform-devs-.26-users/topic/32.20bit.20cygwin.20will.20discontinue.20next.20year/near/260004910
Running Coq with 32-bit pointers really can be twice as fast as with 64-bit pointers
Stefan Monnier said:
Really? That's very interesting. Much as in more than a handful of percents? Is it because of the memory pressure?
For the most part, a program like Coq is memory-bound. Thus, if you double the memory throughput (by halving the size of memory words), you double the speed.
I hope we can get special hardware "Coq memory cache" to speed up proof checking in the future...
Reminds me of Lisp machines ...
JVMs also play similar tricks, but there 64-bit JVMs can often use smaller-than-64 bit pointers.
Last updated: Oct 13 2024 at 01:02 UTC