[install] Notes on OCaml versions and Coq configuration

Using Coq
1

Hi all,

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

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

Native compilation

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 -native-compiler no.

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.

Best-fit allocator

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)

Performance numbers:

You can see some performance numbers in the wiki , that will give you an idea for your particular use case.

Final words

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!

6 Likes
2

Emilio, does this mean you don’t use dune to build Coq? How do you pass these options using the dune to build Coq?

3

Good point @tchajed , Dune will setup the optimizing options if building in release mode automatically; as it has control over OCaml flags, see the root dune file in the repos; for native indeed we don’t have a full solution in Dune yet, see https://github.com/ocaml/dune/pull/3210 ; precisely the missing bits in that PR is the ones dealing with the configuration of native.

Note that you can call ./configure and then use Dune normally, we use the “promote” mode for config files, so if they are present in the build tree Dune will respect them, otherwise Dune autogenerates a configure file, but meant mostly for developers tho. Packages are expected to call configure as to set the prefix for example.

4

You meant (mode fallback). If it were (mode promote), it would override the files present in the tree.

1 Like
5

Yes, thanks; I mean the promote-as-fallback mode , only used if the file doesn’t exist.

6

Thanks a lot for these precisions Emilio, it’s super useful!

It’s fairly straightforward, but as an Opam newbie I had to track down a few things to figure out what’s the exact way to proceed using Opam, so I just wanted to duplicate it here if other people stumble here. The essential of it has been provided by Emilio over Gitter and added by Jad Hamza to the instructions that can be found here: https://github.com/coq/coq/wiki/Installation-of-Coq-on-Linux

A step by step duplicate of the process described in the link above is hence, for installing for instance Coq 8.11.0 with flambda using the options you suggested:

opam switch create 4.07.1+flambda
eval $(opam env)
opam pin edit coq

The last command will open a text editor, that contains in particular a list of options provided in a build section. Add the following line to it: "-flambda-opts" "-O3 -unbox-closures" and exit the file.
Note: this will report an error. Ignore it and agree to continue, which will start the install.

Additionally, to double check that the flags have been passed on correctly, one can pass the -v flag to the install process and check that indeed the following line is present:
OCaml flambda flags : -O3 -unbox-closures

Best,
Yannick

7 Likes
7

Thanks for the instructions. Did anybody figured out how to automate this (opam pin edit) to use in Travis or other CI script?

Vadim

8

Hi @vzaliva ; we will hopefully make this automatic pretty soon. For now, I think the easiest is to roll out your own opam repos with the modified Coq package.

Kind regards, E.

9

For the record, I have created such an overlay in https://github.com/Blaisorblade/opam-overlay/ — but I only maintain this for my own use, so you’ll want to create your own repo.

10

That’s great, actually @Blaisorblade there is no reason we couldn’t just modify the standard Coq packages in OPAM, when not in flambda mode, this options are just ignored.

We have seen enough testing of these two options that personally I’m comfortable in using them.

1 Like
11

I guess that’s a good point on -flambda-opts '-O3 -unbox-closures' if it’s a no-op, but -native-compiler no disables native_compute so it seems less “safe”. I see a fallback to vm_compute, so maybe that’s good enough?

To play it safer, one can probably add variants of the base coq packages, sth. like coq.8.11.1-no-native (or viceversa), tho you might need to relax a bit version constraints for packages that depend on exact coq versions.

12

Indeed that only applies to the flambda flags; how to handle native is still a bit of an open question.

On the other hand native should not make any difference [modulo bugs], so as of today it is not so important to disable it unless you are actually seeing a bug, in which case we’d rather try to fix it ASAP upstream.

13

I was thinking about doing a hack by setting OPAMEDITOR env. variable to point to a script which uses sed to modify the settings and then using opam pin edit non-interactively.

1 Like
14

Personally I think the hack is not worth it, but I dunno.

15

I’m only seeing the bug you already know, With native_compute, flambda slows Coq (a bit on Linux, a lot on Mac) · Issue #11107 · coq/coq · GitHub. (I haven’t experienced On OS X, Coq with native-compiler is too slow · Issue #11178 · coq/coq · GitHub but that’s also relevant).

16

@ejgallego Actually, instead of passing -native-compiler no when compiling, it’d be enough to default to -native-compiler no at runtime; maybe that already happens in 8.11.1 (but not on master/8.12). https://github.com/coq/coq/issues/11178#issuecomment-617276614

17

Looking at https://github.com/ocaml/opam-repository/blob/master/packages/coq/coq.8.11.2/opam, that still hasn’t happened; meanwhile, we already deal with native-compute well by disabling it on Mac, so I guess it’s now fine to follow your suggestion? I’ve submitted Coq 8.11.2: enable flambda if the compiler supports it by Blaisorblade · Pull Request #16779 · ocaml/opam-repository · GitHub and asked you for review.

1 Like
18

Are these recommendations still up-to-date for Coq 8.12.0?

19

AFAICT yes; 4.10.0 is faster on some benchmarks but slower on others, and it’s still not supported by all plugins. So 4.07.1+flambda seems still what we plan to use as default, also for the official Docker images.

And we’re making some progress towards enabling flambda by default on opam packages. Doing that without exposing users to regressions / without defaulting to unsupported configurations isn’t easy, but we seem to have found a way.

2 Likes
20

Added link to performance numbers in the wiki.