Distribute Coq 8.11 (etc.) as from the alpha phase

[erikmd]

As suggested by @palmskog on Gitter:

any chance of a (nightly refreshing) Docker image based on the 8.11.dev OPAM package? Would be super useful for CI for plugins now that v8.11 is frozen.

I've started looking into, this looks definitely feasible! but I guess I won't rely on the 8.11.dev opam core-dev package (because in each Docker images, two different switches are built sequentially, so there is a small risk that the Coq version between the two switches is different 😃), fortunately I can reuse the setup I had written for the coq.dev nightly refreshing Docker image − basically, using some build Docker Hub hook + some opam git pinning:

COQ_BRANCH="v8.11"
COQ_VERSION="8.11+alpha"
COQ_COMMIT=$(curl -fsL -X GET -H "Accept: application/vnd.github.v3.sha" https://api.github.com/repos/coq/coq/commits/${COQ_BRANCH})
opam pin add -n -y -k git coq.${COQ_VERSION} "git+https://github.com/coq/coq#${COQ_COMMIT}"

I'll close that issue as soon as the image is ready and the wiki updated, hopefully in a couple of hours.

[palmskog]

This is great, but I believe this means that this means that the Docker image will use the dune-based OPAM file in the Coq repository, which is subtly different from the non-dune build of Coq. For example, I don't think the dune build supports bytecode currently (not a problem in my projects). Just a heads up to document this on the wiki.

[erikmd]

Dear @palmskog,

this means that the Docker image will use the dune-based OPAM file in the Coq repository

Ah OK! thanks for the remark, I was not aware of that :-/ so indeed the following files are different:

• https://github.com/coq/opam-coq-archive/blob/master/core-dev/packages/coq/coq.8.11.dev/opam
• https://github.com/coq/coq/blob/v8.11/coq.opam

Cc @Zimmi48 @ejgallego

[…] For example, I don't think the dune build supports bytecode currently

OK; but to overcome this opam config difference (and even if the Dune-based build is going to supersede the make-based build system very soon), do you think that a small PR modifying the coq.opam file only in the v8.11 branch (to have the same build commands as the core-dev opam file) would be accepted? or do you have another suggestion? (maybe keeping the coq.opam file as is and documenting the issue as Karl suggests is the simplest solution)

[palmskog]

@ejgallego can likely correct any details I get wrong here, but my understanding from asking around is that the opam file in the Coq repo is used for benchmarking (coq-bench), while the one in the opam archive repo is what users are supposed to generally use for installation. These files may become in synch at some future point when the release managers fully commit to using dune (which did not happen for 8.11). Dune can then even generate the opam file, so it doesn't have to live in the repo.

I believe coq-bench is still used on the v8.11 branch, so I'm not sure what the best solution is w.r.t. opam files in the Coq repo.

[ejgallego]

I don't think the dune build supports bytecode currently (not a problem in my projects).

I'm not sure what you mean but it should support bytecode right; only difference is support for native compute and that plugins are built differently but the new way is more robust.

I'm unsure how to solve this OPAM discrepancy problem.

[erikmd]

Hi @ejgallego and @palmskog, OK thanks for your feedback! so let's say we keep the two opam files as is for now, and in any case that issue will disappear with the beta (as it will rely on the core-dev opam file, not on the git branch)

[palmskog]

Right, I mixed up bytecode and native compute. Indeed the opam discrepancy shouldn't be a blocker for an experimental Docker image, so I agree with @erikmd here.

[ejgallego]

Sounds good @erikmd , we should really remove the discrepancy tho.

[erikmd]

Done (closing the issue now):

$ docker run --rm -it coqorg/coq:8.11 opam pin
coq.8.11+alpha    git  git+https://github.com/coq/coq#a613ea5c48bb486e71382afa8e4a1b772beda58a

FYI I wrote this in the wiki:

Remark: coqorg/coq:8.11 currently points to a Docker image for coq.8.11+alpha, nightly rebuilt from the v8.11 branch of Coq using Dune, so this pre-release image could behave differently w.r.t. other stable Docker images (in particular, lack of support for native_compute).

(but feel free to suggest another phrasing if need be)