Karl Palmskog (Sep 04 2020 at 13:18): 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?
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
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).
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)
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.
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)
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.
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.
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)
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.
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.
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 ?
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.
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?
Karl Palmskog (Mar 01 2022 at 09:33):I think Erik already has a nice setup for building Docker images based on GitLab CI
Karl Palmskog (Mar 01 2022 at 09:34):I'm not sure it would be worth the hassle to port that to Platform CI
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.
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/
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.
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.
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?
Erik Martin-Dorel (Mar 07 2022 at 23:30):Regarding the size of the Docker images, just a small remark to reassure you:
the standard Docker filesystem driver deduplicates children images efficiently (see https://en.wikipedia.org/wiki/OverlayFS )
so if you download, say, 4 different children images that rely on the same large image coqorg/platform:tag-name, this latter will be stored only once
the size itself is lighter than regular VMs, but the culprit is essentially that of opam switches, see e.g.:
$ du -sh "$(opam var prefix)"
4,2G /home/emartin/.opam/4.07.1+coq-8.12
opam clean -a -c -s --logs like in Docker-Coq's Dockerfile and this is really useful (see below), but this is the only "that effective" optimization I'm aware of:$ opam clean -a -c -s --logs
$ du -sh "$(opam var prefix)"
2,9G /home/emartin/.opam/4.07.1+coq-8.12
You can also pass option -r to opam clean for a bit more cleanup.
Erik Martin-Dorel (Mar 08 2022 at 11:29):Indeed; it seems the corresponding storage-space saving is very small, but thanks @Guillaume Melquiond
Paolo Giarrusso (Mar 08 2022 at 11:58):https://github.com/ocaml/opam/issues/4282 is also relevant, even if the opam maintainers disagree...
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.
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.
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.
Paolo Giarrusso (Mar 08 2022 at 18:04):I guess https://github.com/ocaml/opam/issues/4255#issuecomment-652344614 was more informative:
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.
Erik Martin-Dorel (Mar 08 2022 at 21:38):All in all, it seems that:
opam clean -a -c -r -s --logs for now) should certainly be the first step to implement, for dockerizing the Coq platform;learn-ocaml)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?
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: Jun 03 2023 at 03:01 UTC