Compiling library against multiple versions of Coq at the same time

[Alizter]

Here is a small guide for something you can do in Dune which is compile a library against multiple opam switches at the same time. This feature was originally designed for building an OCaml library against multiple compiler versions, however we can make use of it for Coq.

The idea is to use the (context ...) stanza which is able to go in either your .config/dune/config file or in a dune-workspace file, at or above the level of the repo. You can write something like this:

(lang dune 3.7)

(context
 (opam
  (switch coq.8.16.1)))

(context
 (opam
  (switch coq.8.16.0)))

Now when you do dune build, Dune will also simultaneously build the other switches. You can observe the artifacts in _build. Here default is the "default" build context and the other build contexts will have their own directories.

In order to create a mono-version opam switch it is as simple as doing

opam switch create coq.8.16.1

Furthermore, you can also build against more recent versions of Coq, following the master branch by first adding the opam repository:

opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev

and then doing

opam switch create coq.dev

Then adding the corresponding context stanza to your config or workspace file will let you build against all the versions of Coq at the same time.

cc @jdchristensen @jarlg who might be interested