The Coq mailing list

[Emilio Jesús Gallego Arias <e AT x80.org>]

Dear Andrew,

Andrew Appel 
<appel AT CS.Princeton.EDU>
 writes:

> Coq 8.8.0 is 14% faster than Coq 8.7.2 (this measurement was made on
> Travis-CI, whatever hardware they are running).

Thank you very much for the feedback and performance measurements and
insights; let me add a few remarks:

- Travis tends to be not the most reliable platform for measuring
  performance, you are not even guaranteed to get two jobs to run in the
  same CPU, and system load on the shared server will influence the
  results. Based on my own 8.8 testing, the 14% delta seems a lot.

> Summary: 32-bit Coq is 17% faster than 64-bit Coq on my machine.

> You might ask, "why is the choice of 32-bit or 64-bit distribution
> only available for Microsoft Windows users, and the Mac users get only
> the 64-bit distribution?" Well, maybe 17% performance difference is
> not important to Mac users, I don't know.

- Note that for Linux OPAM users, we do ensure that the `+32bit`
  switches do function correctly, so that's a possible solution [OPAM
  32bit OCaml used to have issues in OSX in the past tho].

- but talking about OPAM brings me to the next point: FLambda and
  Coq. In my own measurements, compiling Coq with aggressive flambda
  optimizations tends to bring an extra 5%-10% performance.

  IMHO, this is an extremely low-hanging fruit to pick for intensive
  users.

Best regards,
Emilio