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

Request: Add 8.15.dev image #41

Closed LasseBlaauwbroek closed 2 years ago

LasseBlaauwbroek commented 2 years ago

Now that 8.15.dev has landed in coq-core-dev, it would be useful to have a corresponding Docker image to track this release.

Thanks!

Zimmi48 commented 2 years ago

Unfortunately, now that we have SerAPI in these images, we are waiting for an 8.15 compatible release (see https://github.com/ejgallego/coq-serapi/issues/264).

@palmskog @erikmd Given that SerAPI (contrary to bignums) is not in Coq's CI and that we are dependent on Emilio to create a new compatible version at each new major release of Coq, this has the potential to disrupt and significantly slow down the process of making CI testing possible for many projects. I wonder if we shouldn't revise our rules on how / when to publish the image. A solution could be to publish a new image as soon as Coq + Bignums are released, and to add SerAPI to the image once it becomes available.

Alizter commented 2 years ago

Why isn't SerAPI in Coq's CI? It seems like the logical thing to do?

Zimmi48 commented 2 years ago

It has been proposed many times, but Emilio has always refused this option. Here is his explanation the last time he replied to such a suggestion:

I don't have SerAPI in CI because it would be too much pain for devs having to do overlays; it is way more efficient for me to port to a released version.

(Source: https://github.com/coq/coq/pull/15220#issuecomment-991105961)

Alizter commented 2 years ago

Would it really be that much pain? Worst case, SerAPI will have more maintainers which is a good thing if we want the general coq ecosystem to rely on it. It seems to be an arbitrary bottleneck for Emilio to be the sole maintainer. Perhaps I am failing to understand the work involved...

Zimmi48 commented 2 years ago

I cannot comment on this further, other than involving @ejgallego in the discussion. I am also not so fond of the current status quo. The plan has been (for some time now) that parts of SerAPI that lots of projects rely on would be integrated into Coq and that other parts would be kept separate, but I don't see this happening in the very short term.

ejgallego commented 2 years ago

As always there is a tradeoff here, quite a non-trivial fear is that SerAPI depends on tricky part of the ppx stack which is now undergoing a transition, so pulling that into the CI also pulls a lot of other tricky stuff, YMMV; I'm open to any option, but my reluctance to go to Coq's CI is IMHO a bit justified as I don't want to be the target of frustated devs having to deal with it.

Now I have to deal with frustated Docker packagers XDDD but indeed, I dunno what can I do.

erikmd commented 2 years ago

Hi @SkySkimmer @Zimmi48 @palmskog @anton-trunov @ejgallego @LasseBlaauwbroek @Alizter @proux01,

Happy New Year 2022 ✨✨✨ !

FYI, coqorg/coq:8.15-ocaml-* (with coq 8.15+rc1) is now available on Docker Hub. This issue can then be closed since PR #42 has been deployed successfully.

Sorry for not being able to do it more quickly, but it happens there is currently a blocking issue related to the opam PGP key: https://github.com/ocaml/opam.ocaml.org/issues/23

Because of that, it is not feasible to build new base images in coqorg/base… cf. this URL with the failing pipelines: https://gitlab.com/coq-community/docker-base/-/pipelines

As a workaround, I just built coqorg/coq:8.15-ocaml-* with existing versions ocaml-{4.12.0, 4.11.2, 4.07.1, 4.05.0} for now…

But when the issue will be resolved, I'll obviously be able to bump these to ocaml-{4.13.1, 4.12.1, 4.07.1, 4.05.0} (to comply with the policy we had documented in the docker-coq wiki)

LasseBlaauwbroek commented 2 years ago

Great! Thank you @erikmd!