What's a convenient way to install multiple Coq versions side by side?

Using Coq
1

Hi all,

I work with multiple projects that require different versions of Coq. In the past I built Coq by hand, and switching version was just a matter of changing a few variables in proof-general. Now I use OPAM, but I haven’t found an easy way to switch between Coq versions.

I tried using per-project OPAM switches (in the style of Python virtualenvs), but since I also do a bit of OCaml programming along most Coq projects this requires per-project copies of Merlin, Dune, Batteries or Core, and so on. In the end each local switch takes anywhere between 500MB and 1.5GB, so having one per project isn’t ideal.

Is there a convenient way to install multiple version of Coq and switch between them with OPAM?

Bonus question, assuming that switches are the best option. In a manual build of Coq 8.8.1, coqtop is 18MB and coqc is 2.2MB. In an OPAM install of the same version, coqtop is 24MB and coqc is 3MB, and there’s an additional coqtop.byte worth 42MB. Additionally, there are two copies of most binaries, byte-compiled and native compiled. Why is Coq larger with OPAM and how can I tell OPAM to install just one copy of every binary instead of two?

1 Like
2

I use the following function to update my emacs environment to keep track of the current opam switch:

(defun opam-env ()
 (interactive nil)
  (dolist (var (car (read-from-string (shell-command-to-string "opam config env --sexp"))))
    (setenv (car var) (cadr var))))

I can’t recall any particular instances where I’ve had to deal multiple versions of Coq, but it does seem to solve most problems I encounter with opam switches (I can definitely confirm it works with merlin issues).

1 Like
3

The medium-term plan is to have OPAM aware of the Dune cache, so objects are shared among the same filesystem. I think some people have managed to get that resonably working [but not for Coq as it is outside the cache]

I recall that there was some discussion about this in OCaml’s discourse, may be worth posting there too. https://discuss.ocaml.org/t/bounty-for-compilation-cache-in-opam/2482

4

I’ll describe my personal setup, in case it’s useful. I use opam switches for OCaml versions, but since I have 55 versions of Coq installed, taking about 20 GB, spread across only two or three versions of OCaml†, using separate switches for each version of Coq would be infeasible without on-disk sharing. So I’ve set up a folder ~/.local/coq and I install each version of Coq into a subfolder there, such as ~/.local/coq/coq-8.11.1/. Then I make ~/.local/coq/coq a symlink to one of the folders. There are a couple of ways to do the next step: one is to just add $HOME/.local/coq/coq to PATH. Another is to add symlinks in /usr/local/bin (or similar) to each of the binaries in ~/.local/coq/coq/bin. (I’ve also added symlinks making /usr/local/lib/coq point to ~/.local/coq/coq/lib/coq, and symlinks in /usr/local/share/man/man1 pointing to each of the corresponding files in ~/.local/coq/coq/share/man/man1.) Regardless, once you set this up, changing the default version of Coq is just (cd ~/.local/coq && rm coq && ln -s coq-$version coq), and I often don’t even need to do that and can just pass COQBIN="$HOME/.local/coq/coq-$version/bin/" to make and, since I’ve set proof-prog-name-ask to t, can just manually selecet the version of coqtop I want to run. (Hypothetically, one could even make this a bit easier by adding symlinks in /usr/local/bin of, e.g., coqtop8.11 pointing to the 8.11 version of coqtop, etc, a la python3 and python2, etc.)

† Mostly I bump the version of OCaml only when either the newest version of Coq has dropped compatibility with the OCaml I’m using (I’m currently on 4.06.1+fp, I use 4.02.3+fp for < 8.8~, 3.12.1 for <= 8.4pl4, and I’ve tried 3.10.2 for 8.3* to varying degrees of success). I very rarely will also compile a Coq PR with a different version of OCaml if there’s some OCaml-version-specific testing going on there.

1 Like
5

My setup uses OPAM switches, but not per-project ones (because I reuse a switch for multiple projects). The downside is having to call manually opam env --set-switch=SWITCH_NAME where SWITCH_NAME is a metavariable; one probably could automate that, but I don’t think OPAM itself lets you specify per-folder global switches.

Here’s an answer sketch.

OPAM packages for Coq just call configure and make with some options; you must modify those to disable the bytecode version of Coq. Concretely, drop calls to make byte and make install-byte in the package file — see
https://github.com/ocaml/opam-repository/blob/8e2724d01eb50b00f2cf27158e526cd4af8221e8/packages/coq/coq.8.11.2/opam#L39 for the current copy.

The easiest way to apply those changes is to invoke opam pin edit, which lets you modify the package description in your $EDITOR.

But since that’s not very automatable, I store modified packages descriptions in my own opam repo, with variants of the coq package, and you could create yours. It’s GitHub - Blaisorblade/opam-overlay: My Opam overlay; it’s not very documented (beyond the opam docs) but the structure should be relatively self-explanatory (opam only cares for repo and for the folders under packages). My copies uses different version names; e.g. I provide coq.8.11.1+variant, so you can easily pick the variant to use. I’m not sure if you could reuse the usual version names.

1 Like
6

Thanks! Tuareg already has a function, so that’s not too much of an issue. My problem is mostly have many switches in the first place.

Yes, that would be nice…

Thanks, that’s nice, and could probably be made even nicer with update-alternatives and the like. Ny issue with this is how it interacts with packages — I like the package management part of OPAM (it’s convenient to be able to install e.g. ltac2 in 8.10 with OPAM)

Thanks, that’s very useful, but also quite terrible, since it’s not just Coq that’s guilty of this.

7

One can use opam switch link SWITCH_NAME for that I believe.

1 Like
8

Could we ask for opam package flags to address this, by having a bytecode flag? I’ve wanted them for a while, but it wasn’t bad enough to bug people.

I’ve wanted package flags in opam for a while, but said nothing.

Looking at the manual, however, you can encode such flags through (fake) packages, and the existing conditional compilation. Those packages can even define variables.

Then one would “just” (lol) have to introduce and use such a configuration package in all the Ocaml packages of interest.