Stream: Coq users

Topic: Ocaml options


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Pierre Castéran (Mar 17 2022 at 16:53):

Reminds me of Lisp machines ...

view this post on Zulip 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: Jan 27 2023 at 01:03 UTC