search

coq-community / docker-coq

Docker images of the Coq proof assistant (see also: https://github.com/coq-community/docker-coq-action) [maintainers=@erikmd,@himito]
https://hub.docker.com/r/coqorg/coq/
BSD 3-Clause "New" or "Revised" License
37 stars 3 forks source link

dev versions of old versions of Coq #49

Open JasonGross opened 2 years ago

JasonGross commented 2 years ago

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 https://github.com/coq/coq/pull/16238, https://github.com/coq/coq/pull/16236, https://github.com/coq/coq/pull/16235, https://github.com/coq/coq/pull/16234, https://github.com/coq/coq/pull/16233, https://github.com/coq/coq/pull/16232, https://github.com/coq/coq/pull/16231

Alizter commented 2 years ago

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. https://github.com/coq/opam-coq-archive/issues/1775

erikmd commented 2 years ago

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 commented 2 years ago

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 https://github.com/coq/opam-coq-archive/issues/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:

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 commented 2 years ago

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 commented 2 years ago

@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.