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

Image for 8.14 #29

Closed palmskog closed 3 years ago

palmskog commented 3 years ago

The V8.15+alpha tag was put around two months ago, but due to the new release cycle, there hasn't been (and won't be) any beta for 8.14. This makes testing with 8.14 in CI very difficult - basically the only feasible option is to use Théo's new Nix CI, which works well for standalone project without dependencies but not for personal projects with complicated dependencies.

Any chance that the usual nightly image based on v8.XX could be activated for 8.14?

erikmd commented 3 years ago

Hi @palmskog; sorry for not replying earlier, and thanks for opening this issue!

Any chance that the usual nightly image based on v8.XX could be activated for 8.14?

Sure! I'm still on vacation this week (and addressing some deadlines for the start-of-term) so I cannot promise a precise ETA yet but I was precisely planning to spend time on docker-coq very soon, addressing @clarus' request #30 as well. I'll let you informed ASAP.

palmskog commented 3 years ago

Just a note that the V8.14+rc1 tag is now available, so it may make sense to wait for the opam package for this tag before setting up the 8.14 image.

Zimmi48 commented 3 years ago

And I've created the V8.14.0 tag for bignums as well.

palmskog commented 3 years ago

SerAPI for 8.14 is not merged or released yet. Also, if released before 8.14.0, SerAPI for 8.14 can't be packaged as usual, since 8.14+rc1 will not be in the regular OCaml opam repo. So to make things easier I suggest to only add SerAPI to 8.14 images after 8.14.0 has been released.

Zimmi48 commented 3 years ago

It's a bit odd to me that SerAPI is packaged in the main opam repo rather than the Coq one. For including SerAPI in the platform, this is certainly going to be problematic if it isn't released before 8.14.0 is out.

palmskog commented 3 years ago

We could package the SerAPI release for 8.14 in the extra-dev repo until 8.14.0 is released. But then we should really monitor when the "proper" coq-serapi package in the OCaml opam repo gets merged and remove it from extra-dev, or there may be strange behavior for the (admittedly small number of) people using the extra-dev repo.

erikmd commented 3 years ago

Hi all, thanks for your help and for this heads-up! I'm not sure I have understood why the integration of coq-serapi would be more problematic than for coq-bignums; so just to recall what we were doing previously for 8.13: before 8.13.0 is released and packaged in Docker-Coq (using coq/stable/Dockerfile), we had pushed an image for 8.13+beta1 in Docker-Coq using this other coq/beta/Dockerfile, which precisely comes with extra-dev and core-dev. So putting coq-serapi in extra-dev for the time being would make sense I guess. Finally maybe that the last corner case you raised in your last comment, @palmskog, due to a potential conflict between extra-dev and the default opam repository, could be solved by adding a more restrictive coq version constraint in the coq-serapi extra-dev package? WDYT?

palmskog commented 3 years ago

If we only want to allow installation of SerAPI for 8.14 with rc1 when coq-serapi lives in extra-dev, I think the only bound that will work is

"coq" {= "8.14+rc1"}

This is because we set up opam versions so that 8.14+rcX < 8.14.0 < 8.14.dev. With this caveat, I think it will indeed work to perform the planned packaging of SerAPI in extra-dev after its release.

palmskog commented 3 years ago

Now that coq/opam-coq-archive#1816 is merged, I think we have every ingredient available to get a regular "beta-style" Docker image for 8.14+rc1.

Otherwise, let us know if we can help @erikmd.