Yannick Forster (Nov 30 2020 at 09:55): Yannick Forster (Nov 30 2020 at 09:55):We had good experiences with using caching + opam for dependencies, both for MetaCoq and the Undecidability Library. I like that approach in comparison to the docker approach, because there is no overhead for dependencies once the cache is saved
Fabian Kunze (Nov 30 2020 at 09:57):There might be a way to also cache docker images to get the best of both worlds, but I'm not a docker user.
Assia Mahboubi (Nov 30 2020 at 09:59):Is there some doc somewhere about the docker vs caching+opam choice?
Théo Zimmermann (Nov 30 2020 at 10:00):There is no doc on how to setup CI with opam+caching AFAIK.
Christian Doczkal (Nov 30 2020 at 10:01):I was going to ask for that, so can someone briefly elaborate what this setup is and what its advantages and shortcomings are?
Yannick Forster (Nov 30 2020 at 10:02):Here's our build file: https://github.com/uds-psl/coq-library-undecidability/blob/coq-8.12/.github/workflows/build.yml
Karl Palmskog (Nov 30 2020 at 10:03):for most projects in coq-community, caching is not really necessary, they build in 1-5 min
Théo Zimmermann (Nov 30 2020 at 10:04):BTW, our hope with the Nix templates is also to improve the caching possibilities a lot
Christian Doczkal (Nov 30 2020 at 10:05):Just to understand, is this about caching for the project being tested or also for their dependencies? (I will likely add coq-fourcolor as a dependency sooner rather than later, and that one does not build in 5min)
Yannick Forster (Nov 30 2020 at 10:05):The advantage of our is that you can depend on things that do not have a docker image without overhead. For instance MetaCoq doesn't have docker images, so the Undecidability Library would have to install MetaCoq every single time, which takes a lot of time. Instead we install MetaCoq once from opam and then cache the result. But I agree, this only becomes important for projects with long compile times
Yannick Forster (Nov 30 2020 at 10:06):So Christian, in my understanding you could either create a docker image for coq-fourcolor, or cache the .opam directory like we do and then install coq-fourcolor from opam. I found the opam approach more flexible, because most projects nowadays have opam files for new Coq versions but do not create docker images by default
Théo Zimmermann (Nov 30 2020 at 10:08):Long ago, before there were the Docker-Coq and coq-community templates solution, people were using Travis CI with opam caching and this sometimes led to CI running on outdated versions of dependencies (Coq in particular). Do you think that there is also such a risk with your GH Actions-based caching approach?
Karl Palmskog (Nov 30 2020 at 10:10):we have also had problems with caching in the Coq opam archive
Christian Doczkal (Nov 30 2020 at 10:10):@Yannick Forster , thank you, and indeed I considered building an image for that, but it's good to know that there are other alternatives.
Yves Bertot (Nov 30 2020 at 10:12):@Christian : would it make sense to separate coq-fourcolor in two different packets, where one only contains the mathematical proof part and the second one contains the computation part?
Yannick Forster (Nov 30 2020 at 10:13):@Théo Zimmermann I think the outdated version problem is completely fixable in the GH actions setup by understanding cache keys properly. In our current setup caching might be broken sometimes in that successful updates are not propagated to the cache, but if I understand correctly there is a guarantee that everything is tested wrt the most up-to-date versions of the dependencies specified in the opam file
Yannick Forster (Nov 30 2020 at 10:13):Travis dis not have cache keys and did the import manually, whereas on GH it's an action the user can specify
Christian Doczkal (Nov 30 2020 at 10:15):@Yves Bertot I briefly considered this, but I will derive a version of the four-color theorem for simple graphs, so I will depend on the computation heavy part as well. So this would not help me.
Christian Doczkal (Nov 30 2020 at 10:48):@Yannick Forster I'm trying to understand your action, do I understand correctly, that you carry out the opam actions in any event but that they are virtually no-ops if you had a cache hit and everything is already installed in the most up-to-date version. Also, do I understand correctly that the cache (for the key of the current run) is always updated after successful completion of of the job, making it unnecessary to ever manually check for changes in the dependencies?
Yannick Forster (Nov 30 2020 at 10:59):Yes, the opam actions are noops if the cache was loaded and there were no remote updates for the dependencies. The cache update is less trivial: We want what you describe, and we thought we have what you describe. It's also possible to obtain what you describe, but not like we do it right now. The issue is that when a cache is imported with the exact cache key, it is never overwritten. So cache keys should be something like <fixed string>-<base branch>-<PR id>-<commit id>. That way caches are properly overwritten and you never have to check dependencies manually
Yannick Forster (Nov 30 2020 at 11:00):The mentioned issue with caching we have currently however only leads to more compilations of dependencies than necessary, not to CI running with old dependencies. So it's a sound CI in a sense
Christian Doczkal (Nov 30 2020 at 11:36):@Yannick Forster Thank you for pointing out the caveat about caches not being updated when there was an exact match.
Erik Martin-Dorel (Dec 04 2020 at 12:59):(@Théo Zimmermann just told me about this stream)
Yannick Forster said:
The advantage of our is that you can depend on things that do not have a docker image without overhead. For instance MetaCoq doesn't have docker images, so the Undecidability Library would have to install MetaCoq every single time, which takes a lot of time.
indeed; but FYI with the latest architecture used to deploy coqorg/base and coqorg/coq, it becomes easy to automate the build Docker images (for MetaCoq or other dependencies) and automatically push them to Docker Hub (without needing to have docker locally), so this "docker caching" of the dependencies can be reused for several other projects.
If you'd be interested in trying this approach, the main requirement would be to fork this repo: https://gitlab.com/erikmd/docker-keeper-template − see also https://coq-workshop.gitlab.io/2020/#talk-1-2-2 for details, and the doc URL is https://gitlab.com/erikmd/docker-keeper/-/wikis/home (but this wiki still needs to be extended and exemplified…!)
again, this is mostly useful if the build time of the dependencies is significant (which was the case of mathcomp for instance)
Christian Doczkal (Dec 04 2020 at 13:20):Hmm, "fork this repository" (requires GitLab account), create docker-hub account, do this, to that, etc. pp. This seems to be a lot more work than just one single file that's local to the repository. And this all doesn't get easier if one has a real build matrix (say with 3 versions of mathcomp on different versions of coq + dev) :tired:
Erik Martin-Dorel (Dec 04 2020 at 13:26):@Christian Doczkal indeed, the initial setup is longer. The "build matrix" feature is supported though.
as well as the ability to rebuild manually any image, or to make them update as soon as a branch has been modified in a given GitLab repo (which is what we currently use to automatically sync with coq@master and coq@v8.13 (since this commit: https://github.com/coq-community/docker-coq/commit/6e6da72c3f613283f92926f20968b97a8ed26b60))
Yannick Forster (Dec 04 2020 at 13:27):Is there any chance to centralise this e.g. as part of coq-community? If there would be a central repo where I have to submit a PR with a couple of lines (stating which repo should be included, and which branches) once, and then get automated docker images of my projects without maintaining a repo, that would be amazing
Erik Martin-Dorel (Dec 04 2020 at 13:29):@Yannick Forster indeed, good idea… currently only docker-base and docker-coq are centralized in coq-community, but I see nothing blocking for deploying a similar Docker repository for selected packages (which would thus reduce the initial overhead of creating a Docker Hub account etc.)
Christian Doczkal (Dec 04 2020 at 13:29):Yannick Forster said:
Is there any chance to centralise this e.g. as part of
coq-community? If there would be a central repo where I have to submit a PR with a couple of lines (stating which repo should be included, and which branches) once, and then get automated docker images of my projects without maintaining a repo, that would be amazing
I assume you mean automated docker images of the dependencies of your project, right?
Yannick Forster (Dec 04 2020 at 13:33):Ha, I'm not sure what I meant. I'm usually thinking about coq-library-undecidability and metacoq, and I'm involved in both projects. The best way probably would be to enable docker builds for any repo with as less overhead as possible. Anything which circumvents accounts on DoclerHub would already be a good step
Christian Doczkal (Dec 04 2020 at 13:37):Well, graph-theory builds in a few minutes, much faster than coq-fourcolor, the dependency I want to add. So for me it's mostly about not having to compile the dependency. It's a bit of a shame, because coq-fourcolor is in the CI of mathcomp, so it gets built anyway every time math-comp:master changes...
Christian Doczkal (Dec 04 2020 at 13:39):So, in a perfect world, that build would be saved rather than thrown away ...
Yannick Forster (Dec 04 2020 at 13:47):While we're dreaming about a perfect world: It would also be great if there would be a more centralised coq-community CI, which could subsume the mathcomp CI, but also offer forward dependency checking for other projects. Maybe the docker images could come from this CI then. (but in any case, simplifying the current docker workflow would be great, even without fulfilling the dreams here). I asked for a coq-community CI here a while ago: https://coq.zulipchat.com/#narrow/stream/237658-MetaCoq/topic/MetaCoq.20CI.20.2F.20Coq.20Community.20CI/near/211756574
Christian Doczkal (Dec 04 2020 at 13:54):@Yannick Forster I fear both of our wishes will remain in the realm of dreams for a while ...
Erik Martin-Dorel (Dec 04 2020 at 14:02):Hi @Yannick Forster thanks for the link, actually I had missed your earlier ping!
fortunately, part of what you ask for is already implemented in math-comp CI (i.e., to auto-deploy mathcomp/mathcomp-dev images to Docker Hub and build the selected reverse dependencies from these images in one go)
Erik Martin-Dorel (Dec 04 2020 at 14:03):just FTR, here are the links: https://gitlab.com/math-comp/math-comp/-/pipelines/225253135 − https://gitlab.com/math-comp/math-comp/-/jobs/890610024
Christian Doczkal (Dec 04 2020 at 15:07):@Erik Martin-Dorel , if I understand correctly, then mathcomp is built and immediately deployed as a docker image and then the reverse dependencies are checked using the images that have just been created, right? So one could also deploy some of the things that are currently only tested and then thrown away? This would at least take care of developments depending on mathcomp and one (big) reverse dependency, right?
Christian Doczkal (Dec 04 2020 at 15:08):Also, do I understand right, that this pipeline only runs on activity in the math-comp repository, so if there is no activity on math-comp:master for a week, these images can become stale?
Erik Martin-Dorel (Dec 04 2020 at 15:19):Christian Doczkal said:
Erik Martin-Dorel , if I understand correctly, then mathcomp is built and immediately deployed as a docker image and then the reverse dependencies are checked using the images that have just been created, right?
Yes.
So one could also deploy some of the things that are currently only tested and then thrown away?
This could be feasible, albeit not straightforward (it would require a big refactoring of the YAML, as the last stage jobs run in an ephemeral container, cf. the image: … field while the first stage jobs that are then deployed use image: docker-latest and have scripts that need to be encapsulated in docker-build commands, hence more verbosity…)
Erik Martin-Dorel (Dec 04 2020 at 15:21):Christian Doczkal said:
Also, do I understand right, that this pipeline only runs on activity in the math-comp repository, so if there is no activity on
math-comp:masterfor a week, these images can become stale?
Yes, the idea is that mathcomp/mathcomp-dev:* images should only be rebuilt if a PR is merged in mathcomp or coq (for mathcomp/mathcomp-dev:coq-dev)
Erik Martin-Dorel (Dec 04 2020 at 15:23):So indeed the overall infrastructure could evolve further, but one of the questions is, which repo should have the responsibility to deploy an "official" image for the reverse dependencies? as I guess that these dependencies also need to be deployed for stable versions of mathcomp, for example…
Christian Doczkal (Dec 04 2020 at 15:26):Erik Martin-Dorel said:
Yes, the idea is that
mathcomp/mathcomp-dev:*images are only rebuilt if a PR is merged in mathcomp or coq (formathcomp/mathcomp-dev:coq-dev
Okay, this is the idea, but currently the part about rebuilding after merges to coq:master is missing, right? Or how else did this happen: https://github.com/math-comp/math-comp/issues/681
Erik Martin-Dorel (Dec 04 2020 at 15:33):yes, sorry for that… up to now, a scheduled pipeline was in charge to rebuild mathcomp/mathcomp:coq-dev every night and the plan was to replace it with an automatic, immediate trigger; to do this two extensions were needed in docker-keeper to enable this:
coqorg/coq:dev and coqorg/coq:8.13-alpha from merges in coqmathcomp/mathcomp:coq-dev but it is still pending… Clément Pit-Claudel (Dec 04 2020 at 16:26):@Erik Martin-Dorel any chance you could help me setup CI for Alectryon? I don't have an OPAM file for it because it depends on Python as well. Should I create one?
Erik Martin-Dorel (Dec 04 2020 at 16:31):Hi @Clément Pit-Claudel , sure! when would you like to discuss this?
Erik Martin-Dorel (Dec 04 2020 at 16:32):maybe on next Monday?
Clément Pit-Claudel (Dec 04 2020 at 16:57):@Erik Martin-Dorel Sounds good, maybe on monday?
Erik Martin-Dorel (Dec 04 2020 at 23:34):Hi @Clément Pit-Claudel, yes: would you be available after 17:00 UTC+1 on 2020-12-07 ?
(if yes I'll send you a link)
Théo Zimmermann (Dec 05 2020 at 12:37):Christian Doczkal said:
So, in a perfect world, that build would be saved rather than thrown away ...
Note that this is one of the objectives of the Nix setup that we have discussed a lot this week with Cyril and Vincent (see the corresponding thread).
Last updated: Jun 10 2023 at 23:01 UTC