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.
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:
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
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.
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.
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.
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.
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.