dev versions of old versions of Coq

[JasonGross]

Would it be possible to provide images for 8.8.dev, 8.9.dev, etc, tracking the tip of the v8.8, v8.9, etc branches? I'd like to use these for https://github.com/coq-community/coq-performance-tests after merging rocq-prover/rocq#16238, rocq-prover/rocq#16236, rocq-prover/rocq#16235, rocq-prover/rocq#16234, rocq-prover/rocq#16233, rocq-prover/rocq#16232, rocq-prover/rocq#16231

[Alizter]

The opam packages for the dev branch don't work completely IIRC. They are missing upper bounds on some deps. I opened an issue in the opam archive repo about this. rocq-prover/opam#1775

[erikmd]

Hi @JasonGross ! thanks, yes, that looks both sensible and feasible.

Regarding the feasibility, this would just amount to implementing in docker-coq the same feature as this one discussed on Zulip for all branches by default, and without disabling these "alpha" / dev images when the rc1 version goes live.

---

Two questions (Cc @Zimmi48 @palmskog):

Q1) Do we prefer to:

1. use git opam pinning (so that the reference .opam file is just that of the coq/coq git repository):

   → git pin add -n -y -k git coq.8.8 git+https://github.com/coq/coq#v8.8

2. use version pinning with opam-coq-archive (so the coq/coq git repo just provides the code, and opam-coq-archive the .opam)

   → git pin add -n -y -k version coq.8.8.dev (which would require to add core-dev in the image… unlike choice 1.)

?

At first sight, I'd vote 1, but YMMV…

Q2) What naming convention would be relevant?

1. coqorg/coq:8.8-dev
2. coqorg/coq:8.8-git
3. coqorg/coq:8.8-alpha

?

Likewise, I'd vote 1., or 2. (the choice 3. being inspired by the Zulip discussion above, but would not be that sensible from my viewpoint)

[palmskog]

The problem I see here is that the opam packages in old Coq repo branches are not maintained, and our coq.X.YZ.dev packages in the core-dev opam repo are only marginally maintained (see discussion in rocq-prover/opam#1775). If opam packages in Coq repo branches are suddenly being used for various tasks such as producing Docker images, how will it be ensured that these are up to date with:

• the packages for coq.X.YZ.dev in core-dev
• the packages for released Coq version in the OCaml opam repo

If every kind of opam package for essentially the same software version has its own quirks and incompatibilities, this has the potential to generate trouble and maintenance work.

[Zimmi48]

It seems to me that the only way that could work would be to use the package definitions in opam-coq-archive. If issues are detected while trying to build the Docker images, this could allow reporting and fixing the issue in the opam-coq-archive, so the "marginally maintained" status would probably suffice.

[palmskog]

@erikmd regarding Q2, I think the best name for these images would be following the format from the opam packages as far as possible: coqorg/coq:X.Y.dev. That is, we would have coqorg/coq:8.8.dev, coqorg/coq:8.16.dev, etc.