Stream: Coq Platform devs & users

Topic: Docker images for the Coq Platform


view this post on Zulip Karl Palmskog (Sep 04 2020 at 13:18):

@Erik Martin-Dorel an initial release of the Coq Platform (https://github.com/MSoegtropIMC/coq-platform/blob/master/charter.md) will soon appear for Coq 8.12.0, containing both Coq itself and many large packages such as VST, Flocq, and CompCert. We would like there to be Linux-based Docker images containing all the packages in the platform pre-installed, as defined in a custom OPAM repository (https://github.com/MSoegtropIMC/coq-platform/tree/master/opam). How would you recommend we set up the building and hosting of Docker images so they can be used in (Travis and Actions) CI?

view this post on Zulip Erik Martin-Dorel (Sep 10 2020 at 17:49):

Hi @Karl Palmskog (Cc @Michael Soegtrop), sorry for the delay (hopefully It's not too late w.r.t. the upcoming coq-platform release?)

I guess that for distributing the coq-platform via Docker, you'd be interested in having the ability to rebuild the images on-demand (or with a nightly build), deploying automatically the images containing all the selected opam packages to Docker Hub?

In this case, the docker-keeper tooling I had presented in the Coq Workshop is definitely the way to go I'd say.

The main question is: what would be the target Docker Hub namespace to host these coq-platform images? (I propose coqorg/platform or coqorg/coq-platform, (i.e. in the same coqorg organization as that of coq), but feel free to suggest other ideas)

There is a first version of the docker-keeper documentation here: https://gitlab.com/erikmd/docker-keeper-template#note-to-maintainers

I would like to migrate that README documentation to a proper wiki and give a few more details in this doc., but the tool itself is stable.

Anyway, feel free to ping me on Zulip/GitHub/GitLab for any docker-keeper-related question :)

See also these three examples of use:
https://gitlab.com/coq-community/docker-base/pipelines
https://gitlab.com/coq-community/docker-coq/pipelines
https://gitlab.com/math-comp/docker-mathcomp/pipelines

view this post on Zulip Karl Palmskog (Sep 10 2020 at 17:55):

thanks @Erik Martin-Dorel, my vote would be for coqorg/coq-platform. We would probably only need to rebuild on demand (not nightly).

view this post on Zulip Karl Palmskog (Sep 10 2020 at 18:03):

(for the record, the Platform release for 8.12 has not happened yet, not least could there be licensing issues that are stumble blocks in distributing .vo files)

view this post on Zulip Michael Soegtrop (Sep 11 2020 at 07:06):

Yes, for docker licensing issues need to be clarified. The Coq platform itself is source only which is more relaxed than binary distributions. It is likely that in the docker image one cannot deliver the complete platform but has to exclude certain parts which are then build from sources if needed.

view this post on Zulip Karl Palmskog (Sep 10 2021 at 08:57):

so will a Platform Docker image happen for 2021.09? It's stated in the release cycle CEP, but I don't see any discussion beyond the previous posts in this topic (a year ago)

view this post on Zulip Michael Soegtrop (Sep 10 2021 at 09:09):

@Karl Palmskog : I am not a Docker expert (not even a regular user) so I would need help from someone with experience in this area.

view this post on Zulip Théo Zimmermann (Sep 10 2021 at 09:11):

Indeed, for this we would need the involvement of @Erik Martin-Dorel. But this being the start of a new semester and all, I'm not sure how likely he is to be available for that during the month of September.

view this post on Zulip Karl Palmskog (Sep 10 2021 at 09:16):

my question was prompted by Erik planning to do some changes to the official Docker images, such as including coq-serapi (https://github.com/coq-community/docker-coq-action/issues/57#issuecomment-916228433). But I had no intention of filling up his plate with more work. However, since Erik is planning to include coq-serapi in all Docker images, I think this would be a good time to include SerAPI officially in the Platform (https://github.com/coq/platform/issues/13)

view this post on Zulip Karl Palmskog (Sep 10 2021 at 09:19):

in any case, the general concern is that I would like to test against the platform in projects in CI and coq-community and elsewhere (possibly something like 10-15 projects). However, this requires the platform being available either as a Docker image or in Nix.

view this post on Zulip Erik Martin-Dorel (Sep 12 2021 at 00:09):

Hi! thanks for your comments on this thread.
Indeed, the CEP mentioned by Karl already gathers most answers required for packaging the Coq platform in Docker; there are one or two remaining questions to address though, so I guess it would be nice to discuss this in the upcoming weeks (with a video call? and maybe some Zulip chat session).
Anyway, due to teaching and several deadlines, this won't be possible for me before Sept 22.
Last, regarding the on-going upgrade mentioned by Karl (including but not limited to adding coq-serapi), it should go live very soon indeed.

view this post on Zulip Erik Martin-Dorel (Sep 12 2021 at 14:29):

Hi. FYI I've just closed the issue https://github.com/coq-community/docker-coq-action/issues/57 (after migrating it to https://github.com/coq-community/docker-coq/issues/32)

As an aside, as I mentioned in the last-but-one comment, I took the opportunity to bump the pinned dependencies (including dune and opam), but I only did a patchlevel bump of opam, to 2.0.9:

I know opam 2.1.0 is now available, but I noticed with my tests that migrating couldn't be fully straightforward, at least because of opam-depext.

Maybe the only patch to apply on the coqorg/base Dockerfile would amounts to removing this line

but I'd like to have more feedback, to be sure not to break anything downstream → maybe @Michael Soegtrop or some of you did some experiments with opam 2.1.0 ?

view this post on Zulip Michael Soegtrop (Sep 12 2021 at 17:19):

@Erik Martin-Dorel : the opam 2.1.0 issue is solved in 2021.09.0. The development branch is here (https://github.com/MSoegtropIMC/platform/tree/2021.09). I think I should move it to the main repo since it is basically working now.

view this post on Zulip Michael Soegtrop (Mar 01 2022 at 07:54):

@Erik Martin-Dorel, @Karl Palmskog : I wanted to pick this up and provide docker images for Coq Platform (probably for all available picks). Can you summarize what is missing? Should I just dig into the existing coq-docker infrastructure and try to forge a PR or are you aware of any substantial difficulties. One might be that the CI build time is rather long. Do you think the images should be built in Coq Platform CI or somewhere else?

view this post on Zulip Karl Palmskog (Mar 01 2022 at 09:33):

I think Erik already has a nice setup for building Docker images based on GitLab CI

view this post on Zulip Karl Palmskog (Mar 01 2022 at 09:34):

I'm not sure it would be worth the hassle to port that to Platform CI

view this post on Zulip Karl Palmskog (Mar 01 2022 at 09:34):

the main problem as I see it are the sizes of the Docker images. We could easily be looking at several GB if we include all large projects like UniMath. And if people have to spend lots of time to download images, then this limits the usefulness.

view this post on Zulip Karl Palmskog (Mar 01 2022 at 09:45):

to be more specific, I think we want to use Erik's Docker-Keeper infrastructure: https://gitlab.com/erikmd/docker-keeper/

view this post on Zulip Théo Zimmermann (Mar 01 2022 at 10:05):

Karl Palmskog said:

the main problem as I see it are the sizes of the Docker images. We could easily be looking at several GB if we include all large projects like UniMath. And if people have to spend lots of time to download images, then this limits the usefulness.

Agreed, it might be even more important than before to define several tiers (also based on size) and to produce several Docker images based on those.

view this post on Zulip Michael Soegtrop (Mar 01 2022 at 16:13):

Yes, I also think that we should split also a bit by size/compile effort, although for VST we are currently discussing to reduce what it shipped in the opam package. For Unimath I can't say much about optimization options, though.

Long term I would like to make the binary installers such that they download modules. For Windows this would likely mean to switch from NSIS to WIX. For macOS I have not much of a clue how this could be done. But I guess for docker it shouldn't be that hard to download extra packages as needed.

view this post on Zulip Erik Martin-Dorel (Mar 07 2022 at 23:29):

Hi all, sorry for replying late. Yes I'd be happy to help setting up a proper way to package Coq-platform using Docker (and support several tiers and picks as desired), and I also guess docker-keeper would make this easy to maintain within the Coq-platform repository (in particular, every change in the images would just need some small editing of docker-kepeer's dedicated spec - in YAML).

A corresponding issue is already opened: https://github.com/coq-community/docker-coq/issues/35 :
I believe the first step is done ("Wait that the Coq Platform repo changes its default branch to master or main")
but the other steps are still pending indeed.

Maybe we could arrange some date for addressing this evolution together, this month?

view this post on Zulip Erik Martin-Dorel (Mar 07 2022 at 23:30):

Regarding the size of the Docker images, just a small remark to reassure you:

$ du -sh "$(opam var prefix)"
4,2G    /home/emartin/.opam/4.07.1+coq-8.12
$ opam clean -a -c -s --logs
$ du -sh "$(opam var prefix)"
2,9G    /home/emartin/.opam/4.07.1+coq-8.12

view this post on Zulip Guillaume Melquiond (Mar 08 2022 at 06:44):

You can also pass option -r to opam clean for a bit more cleanup.

view this post on Zulip Erik Martin-Dorel (Mar 08 2022 at 11:29):

Indeed; it seems the corresponding storage-space saving is very small, but thanks @Guillaume Melquiond

view this post on Zulip Paolo Giarrusso (Mar 08 2022 at 11:58):

https://github.com/ocaml/opam/issues/4282 is also relevant, even if the opam maintainers disagree...

view this post on Zulip Paolo Giarrusso (Mar 08 2022 at 12:00):

My goal there was to shrink the Docker image to reduce build times, but I'll admit I haven't personally investigated the savings in time.

view this post on Zulip Michael Soegtrop (Mar 08 2022 at 13:15):

@Paolo Giarrusso : Since we want opam to stay operational, I am not a big fan of deleting stuff which will make consecutive opam commands fail. I would say the most sensible options are:

1.) keep opam fully operational (but delete everything not required for this)

2.) only keep the installed files and delete everything else

What you propose in https://github.com/ocaml/opam/issues/4282 appears to be somewhere in between. It does not become clear from the issue description what one can delete in addition to what opam clean (with all bells and whistles) does without breaking opam.

For Coq Platform it might make sense to have option 2 images - many people might be happy with what Coq Platform provides and won't call opam any more - of course in case they need in the future there should be a trivial upgrade path.

view this post on Zulip Paolo Giarrusso (Mar 08 2022 at 18:00):

I'm not claiming this is a perfect solution; but the only "downside" I'm aware of is that afterwards I need to call "opam update" again, which I'd expect still satisfies 1. When I wrote it, the intention is that everything I was removing was merely a cache.

view this post on Zulip Paolo Giarrusso (Mar 08 2022 at 18:04):

I guess https://github.com/ocaml/opam/issues/4255#issuecomment-652344614 was more informative:

view this post on Zulip Paolo Giarrusso (Mar 08 2022 at 18:04):

In the case of source-pinned packages, we were expecting at some point to use the data in the left-over build dir to e.g. check the git refs w.r.t. the current source; but apparently it's not used at the moment.

Note that another reason to keep the build dir could be debug options and when the build failed, so that you can troubleshoot.

view this post on Zulip Erik Martin-Dorel (Mar 08 2022 at 21:38):

All in all, it seems that:

and after implementing option 0., we could try to validate the feasibility and the storage saving brought by option 2., and if it is worth it, I'd suggest we provide then two different image flavors: those for option 0, those for option 2. (…-slim)

or ultimately, if the discussions for option 1. succeed, providing only option 1.

WDYT?

view this post on Zulip Michael Soegtrop (Mar 09 2022 at 07:31):

Sounds good to me. So I would say we start with option 0 since it is most flexible and other options are optimizations.


Last updated: Jan 30 2023 at 10:03 UTC