here are some (personal) informal observations regarding OCaml versions and installation. Note this information may quickly get outdated, and represents solely my personal opinion.
TL;DR: Use OCaml 4.07.1+flambda, compile Coq with
./configure -flambda-opts '-O3 -unbox-closures' -native-compiler no
First of all, the OCaml version and setup you use for running Coq may have a large impact in terms of performance; for users that spend considerable daily time doing proofs this can amount to a large number of hours spent waiting for Coq to answer.
Supported OCaml versions:
As you may know, Coq can run in OCaml [4.05.0 - 4.10.0]. Versions 4.05.0 / 4.06.1 may work fine, however they don’t have any known advantage over 4.07.1; moreover, when using flambda 4.05 / 4.06 have a middle-end bug that makes usage very difficult. @palmskog notes that https://github.com/ocaml/ocaml/issues/7472 did also impact the compilation of 3rd party packages on < 4.07.
OCaml versions >= 4.08 have a performance bug due to different GC strategies, we don’t recommend its use; see https://github.com/ocaml/ocaml/issues/9326 . If you must use OCaml >= 4.08 then wait for Coq 8.11.1 and use OCaml 4.10.0
So far, OCaml 4.07.1 has proven to be solid, so that’s what we recommend.
flambda or not to
Flambda is an optimizing OCaml backend; it must be installed as a different compiler. Measurements in 4.07.1 show general improvements from the order of 0% to 15% percent; we thus recommend using it by default. Coq’s CI runs most expensive developments using the flambda variant, so it is reasonably well-tested.
In order for Coq to take most advantage of
flambda optimizations you may want to pass some extra options to Coq’s configure, in particular
-flambda-opts '-O3 -unbox-closures'; you can do this with
opam pin edit coq for example. See step-by-step instructions in @Yannick 's comment below
Coq does support compiling modules in two different formats, one is the regular
mod.vo , and the other is the so-called “native compilation”, where a
.v file is compiled to an OCaml
.ml file, the
ocamlopt is invoked to produce an object file.
As of today, this mode seems undocumented, and it has caused problems for some users in OSX; unless you have a specific need for it I recommend disabling it by adding to Coq’s configure
Doing this will greatly speed up the compilation of Coq itself [so if you track master that will save you quite amount of time]. In a normal use case, you shouldn’t notice any difference, but due to the bugs mentioned above you may want to try and see if you get faster compilation times, specially if are on OSX.
If you are into bleeding-edge stuff, see https://caml.inria.fr/pub/docs/manual-ocaml/flambda.html as on how to enable the best-fit allocator (you’d need a patched Coq for 4.10)
You can see some performance numbers in the wiki , that will give you an idea for your particular use case.
Again, this is my setup and what works best for me; YMMV. For example you may find better
-flambda-opts or my setup may slow you down. Please don’t hesitate to comment and provide feedback!