rocq/rocq-prover:9.0 installs a RC version and has spurious "dev" OPAM repositories

[xavierleroy]

$ sudo docker run -it rocq/rocq-prover:9.0 bash
rocq@f692eb3e664d:~$ rocq --version
The Rocq Prover, version 9.0+rc1
compiled with OCaml 4.14.2

Now that Rocq 9.0.0 is officially out, could we please have 9.0.0 instead of a RC in this 9.0 tag? CompCert doesn't like RC.

rocq@f692eb3e664d:~$ opam remote -v
[NOTE] These are the repositories in use by the current switch. Use '--all' to
       see all configured repositories.

<><> Repository configuration for switch 4.14.2+flambda <><><><><><><><><><><><>
 1 rocq-core-dev  https://coq.inria.fr/opam/core-dev
 2 rocq-extra-dev https://coq.inria.fr/opam/extra-dev
 3 rocq-released  https://coq.inria.fr/opam/released
 4 default        https://opam.ocaml.org

As a consequence, opam install menhir will install a "dev" version of Menhir that CompCert doesn't recognize.

Once this docker uses 9.0.0, could we please get rid of the rocq-core-dev and rocq-extra-dev OPAM repositories, and keep only the default and rocq-released repositories?

[erikmd]

Dear Xavier,

Now that Rocq 9.0.0 is officially out, could we please have 9.0.0 instead of a RC in this 9.0 tag? CompCert doesn't like RC.

Sure! I was precisely planning to bump the rocq/rocq-prover:9.0 image this WE.
I'm working on this (#11). I'll let you know (and close the issue) as soon as the 9.0 tag refers to 9.0.0 instead of 9.0-rc1.

could we please get rid of the rocq-core-dev and rocq-extra-dev OPAM repositories, and keep only the default and rocq-released repositories?

Yes! These {core-dev,extra-dev} repos are needed for building the release candidate,
but I confirm that in docker-rocq's release process, these 2 repos are removed when
the stable release goes live (we just switch the underlying Dockerfile).

Thanks for opening the issue!

[erikmd]

Deployment of 9.0.0 done:

• https://hub.docker.com/r/rocq/rocq-prover#supported-tags
• https://hub.docker.com/repository/docker/rocq/rocq-prover/tags?name=9.0

[xavierleroy]

Thanks a lot, Erik ! The new image works great with CompCert and will be used for its CI on Github.