[install] Notes on OCaml versions and Coq configuration

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.

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

1 Like

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

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



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


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.

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.

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

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.

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.

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

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

I’m only seeing the bug you already know, https://github.com/coq/coq/issues/11107. (I haven’t experienced https://github.com/coq/coq/issues/11178 but that’s also relevant).

@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

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 https://github.com/ocaml/opam-repository/pull/16779 and asked you for review.

1 Like

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

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.


Added link to performance numbers in the wiki.


It seems as of a few months ago 4.07*-flambda images have been removed from Docker Hub for coq:dev

In light of this change, can this post and this wikipage be updated on what is the preferred OCaml version? I see both 4.12 and 4.13 available for coq versions 8.13+, but 8.12 has only up to OCaml 4.11.

cc: @erikmd

The wiki page has been updated now.