Alexander Gryzlov (Mar 17 2022 at 13:38): Alexander Gryzlov (Mar 17 2022 at 13:38):Btw, would you suggest to turn on more options besides flambda? I've seen some mentions that fp could also be beneficial for Coq.
Karl Palmskog (Mar 17 2022 at 13:51):@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
Stefan Monnier (Mar 17 2022 at 14:11):Really? That's very interesting. Much as in more than a handful of percents? Is it because of the memory pressure?
Karl Palmskog (Mar 17 2022 at 14:13):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
Karl Palmskog (Mar 17 2022 at 14:14):Running Coq with 32-bit pointers really can be twice as fast as with 64-bit pointers
Guillaume Melquiond (Mar 17 2022 at 14:42):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.
Karl Palmskog (Mar 17 2022 at 15:04):I hope we can get special hardware "Coq memory cache" to speed up proof checking in the future...
Pierre Castéran (Mar 17 2022 at 16:53):Reminds me of Lisp machines ...
Paolo Giarrusso (Mar 17 2022 at 18:05):JVMs also play similar tricks, but there 64-bit JVMs can often use smaller-than-64 bit pointers.
Last updated: Apr 19 2024 at 06:02 UTC