Images with multiple versions of Rocq?

[JasonGross]

What's the easiest/fastest/best way to get docker images with two versions of Rocq/Coq installed in separate switches? E.g., if the provided docker images could (or already do?) name the switch they use after the version of Rocq/Coq (or even the full ocaml+Rocq/Coq version), then it might be feasible to roll my own docker images that just copies the ~/.opam directories from the two docker base images and merges them.

This is for rocq-prover/bot#346

[erikmd]

Hi @JasonGross,

Thanks for opening this issue;
actually, the first architecture of docker-coq images did rely on 2 ocaml switches (2 ocaml versions + the same coq version).
But this appeared to be a bad idea: there was no good use case for that feature, and above all, a waste of build time / pull time.
So now each Docker-Rocq image is mono-switch.

Can't your feature directly use two different Docker images?

Otherwise, you said you'd like to perform a "merge":
you may want to try using Docker's multi-stage build feature,
(maybe using the special rocq/base:bare that contain the standard configuration but no switch),
or the opam switch create --fake option,
but I'm afraid implementing one such merge won't be easy :-/
(notably as the switch name only depends on the ocaml version,
and if we rename a switch, maybe the binaries aren't relocatable)

[JasonGross]

Can't your feature directly use two different Docker images?

The minimizer needs to run both versions of Rocq hundreds of times each on files, often ones that take less than a second to check. And this needs to be done on GitHub Actions runners. I'm not familiar enough with docker in docker to know how easy it is to get two docker images running in GHA with bindings to the same directory and a single wrapper script for each that, when called from the standard GHA runner/container, invokes Rocq inside the appropriate docker image. Do you know how to do this?

notably as the switch name only depends on the ocaml version,
and if we rename a switch, maybe the binaries aren't relocatable

Right, would it be possible to set up the Coq / Rocq images so that the switch name depends on the version of Coq/Rocq as well? And maybe use a symlink / fake switch for the original name to maintain backwards compatibility? This would make it pretty easy to merge the docker images, IIUC.

[JasonGross]

Do you know how to do this?

Answering my own question, the LLMs think this is straightforward