Théo Zimmermann (Jun 24 2020 at 11:19): Théo Zimmermann (Jun 24 2020 at 11:19):This is the topic to ask questions on the talk "A Gentle Introduction to Container-based CI for Coq projects".
Emilio Jesús Gallego Arias (Jul 05 2020 at 14:24):Erik's talk has just started!
Emilio Jesús Gallego Arias (Jul 05 2020 at 14:33):Note: You can run docker sudo-less in Debian/Ubuntu by adding your user to the dockergroup [as the docker binary is suid]
Enrico Tassi (Jul 05 2020 at 14:39):Q: If I want to prepare images with Coq + Elpi for projects using them (like Hierarchy Builder or FPC) where should I put them? under coqorg ? And if so, do I need some sort of permissions/account?
Enrico Tassi (Jul 05 2020 at 14:42):OK, thanks!
Yves Bertot (Jul 05 2020 at 14:42):Should we understand that coq-community/templates is the right pointer?
Yves Bertot (Jul 05 2020 at 14:43):What is the easiest documentation?
Paolo Giarrusso (Jul 05 2020 at 14:45):Are your slides online?
I thought the slides mentioned docker-keeper, but I can't find it online...
Théo Zimmermann (Jul 05 2020 at 14:46):Slides will be put on the website soon ;-)
Tej Chajed (Jul 05 2020 at 14:49):@Yves Bertot I've found the CI setup wiki page to be a good starting point, especially clicking through to the example setups for Travis CI or GitHub Actions
Erik Martin-Dorel (Jul 05 2020 at 14:57):Emilio Jesús Gallego Arias said:
Note: You can run docker sudo-less in Debian/Ubuntu by adding your user to the
dockergroup [as thedockerbinary is suid]
@Emilio Jesús Gallego Arias is right that this is a possible workaround, but note that this workaround significantly weakens security, as explained in https://github.com/coq-community/docker-coq/wiki/CLI-usage#convenience-config-for-gnulinux-and-macos and https://docs.docker.com/engine/security/security/#docker-daemon-attack-surface (to summarize, the user that has the right to run a Docker container amounts to being root on the machine (because it can choose to bind-mount a directory to access the host filesystem)).
Hence the suggested other workaround to just add alias docker="sudo docker" in one's ~/.bashrc.
Otherwise, there is another proper solution to be able to run containers without being root, relying on a recently implemented feature of Docker:
https://docs.docker.com/engine/security/rootless/
Erik Martin-Dorel (Jul 05 2020 at 15:01):Enrico Tassi said:
Q: If I want to prepare images with Coq + Elpi for projects using them (like Hierarchy Builder or FPC) where should I put them? under coqorg ? And if so, do I need some sort of permissions/account?
This is mostly orthogonal to the coqorg organization, to deploy your own images you could just create a dedicated Docker Hub organization, e.g. https://hub.docker.com/u/elpi, then you'll just need to fork https://gitlab.com/erikmd/docker-keeper-template and follow the instructions of the README -- feel free to ask related questions by posting here on Zulip or opening a GitLab issue!
(docker-keeper is currently used for docker-base, docker-coq, docker-mathcomp)
Erik Martin-Dorel (Jul 05 2020 at 15:10):Yves Bertot said:
Should we understand that coq-community/templates is the right pointer?
Yes, basically I'd say there are three main pointers related to docker-coq:
Erik Martin-Dorel (Jul 05 2020 at 15:11):Paolo G. Giarrusso said:
Are your slides online?
I thought the slides mentioneddocker-keeper, but I can't find it online...
Indeed, I had only mentioned the docker-keeper-template GitLab URL; but the underlying tool is also on GItLab: https://gitlab.com/erikmd/docker-keeper
Paolo Giarrusso (Jul 05 2020 at 15:17):Ah, I had searched on GitHub... does docker-keeper work across different gitlab instances? The instructions assume gitlab.com, but probably I can just search-n-replace that in URLs?
Paolo Giarrusso (Jul 05 2020 at 15:19):(Let me know if these questions are too specific!).
Erik Martin-Dorel (Jul 05 2020 at 15:27):Paolo G. Giarrusso said:
Ah, I had searched on GitHub... does
docker-keeperwork across different gitlab instances? The instructions assumegitlab.com, but probably I can just search-n-replace that in URLs?
Sure, docker-keeper should be compatible with any GitLab instance,
so indeed you'll just need to replace the occurrences of https://gitlab.com in the README.md template and the images.yml file (notably the base_url value that is automatically prepended by the tool to generate some URLs)
Erik Martin-Dorel (Jul 05 2020 at 15:29):Paolo G. Giarrusso said:
(Let me know if these questions are too specific!).
(No worries, your questions are perfectly on-topic :)
Karl Palmskog (Jul 05 2020 at 15:30):I think the main limitation of our templates right now is the initial burden of setting up meta.yml. Should there perhaps be some generator for this?
Erik Martin-Dorel (Jul 05 2020 at 15:32):I was wondering whether we could just provide a webapp (e.g. deployed statically in GitHub pages) that would contain a form, and generate the meta.yml (or even a zipped archive of meta.yml + the generated files :)
What do you think?
Karl Palmskog (Jul 05 2020 at 15:34):that's a possibility, sure
Erik Martin-Dorel (Jul 05 2020 at 15:35):but this is maybe not the only possibility,
anyway I agree with you that this initial step is currently the main "limitation" of the coq-community templates
Théo Zimmermann (Jul 05 2020 at 15:37):Another possibility would be for the generate.sh script to generate meta.yml as well if it doesn't exist.
Théo Zimmermann (Jul 05 2020 at 15:37):Might be time to rewrite this script in some saner language (OCaml, Python?) :laughing:
Paolo Giarrusso (Jul 05 2020 at 15:39):Somewhat relatedly, for my last Coq project, I started from Docker-Coq, but then I built Docker images with its exact dependencies, to cache those deps and speed up CI. Is that supported somehow by your tooling?
For myself, I have some custom scripts (on https://github.com/Blaisorblade/docker-dot-iris), but I'd happily migrate to something better.
Karl Palmskog (Jul 05 2020 at 15:43):hmm, is it possible to start from docker-base rather than docker-coq for custom images/pipeline?
Paolo Giarrusso (Jul 05 2020 at 16:08):Théo Zimmermann said:
Another possibility would be for the
generate.shscript to generatemeta.ymlas well if it doesn't exist.
I guess ref.yml helps quite a bit; IMHO a next step (as some suggested on the repo) might be to get from an "example" or "template-for-humans" version of meta.yml, as many projects do — that is, a syntactically valid meta.yml, containing as comments both field descriptions and fields with defaults, which can be edited as needed. Maybe with a wizard/generator for the "essential" fields.
Paolo Giarrusso (Jul 05 2020 at 16:12):I've skimmed https://github.com/coq-community/templates/issues/19 and https://github.com/coq-community/templates/pull/30 — I see the link to examples, but I hadn't thought that the examples were meant as starting points for meta.yml.
Paolo Giarrusso (Jul 05 2020 at 16:13):(basically, I'm suggesting https://github.com/coq-community/templates/issues/19#issuecomment-604641229 as a starting point — but I realized it afterwards)
Erik Martin-Dorel (Jul 05 2020 at 16:32):Paolo G. Giarrusso said:
Somewhat relatedly, for my last Coq project, I started from Docker-Coq, but then I built Docker images with its exact dependencies, to cache those deps and speed up CI. Is that supported somehow by your tooling?
For myself, I have some custom scripts (on https://github.com/Blaisorblade/docker-dot-iris), but I'd happily migrate to something better.
Thanks for the pointer.
Indeed, the workflow you mention is exactly the use case targeted by docker-keeper :)
I already mentioned this in my talk, but to summarize the main features you'd have by keeping your Dockerfile and using that tooling (instead of a bash script to run manually):
ARGuments)nightly: true e.g. to rebuild each image based on coqorg/coq:dev e.g. after 2:00 UTCIf you'd like to use that tool, as your current Dockerfile repository is on GitHub (and as docker-keeper is tied with GitLab), you could either keep your GitHub repository, create a GitLab mirror (CI/CD for external repo) https://gitlab.com/Blaisorblade/docker-dot-iris, configure Théo's coqbot to enhance the mirroring capabilities (w.r.t. Pull Requests...), and finally add the docker-keeper subtree within your repository; or you could just create an independent GitLab repository (e.g. by forking the docker-keeper-template)
Erik Martin-Dorel (Jul 05 2020 at 16:36):Karl Palmskog said:
hmm, is it possible to start from docker-base rather than docker-coq for custom images/pipeline?
indeed it's possible, but not really useful for Coq projects I guess (docker-base only contains these opam packages (in addition to these APT packages))
Anton Trunov (Jul 05 2020 at 16:47):Théo Zimmermann said:
Another possibility would be for the
generate.shscript to generatemeta.ymlas well if it doesn't exist.
and we need a meta-meta.yml file as the input to the generator script ;)
Paolo Giarrusso (Jul 05 2020 at 16:51):@Erik Martin-Dorel I thought docker-keeper was about building Docker images which contain _my_ library — though the repository never actually says?
Paolo Giarrusso (Jul 05 2020 at 16:52):sorry, it does say: > This repository provides Docker images of (stable versions of) the user/repo project.
Paolo Giarrusso (Jul 05 2020 at 16:56):but for the CI of user/repo, I guess I don't want the images to contain user/repo itself? And my development is a leaf, so images for my user/repo aren't needed for anybody.
My CI script can uninstall user/repo first, I guess, but I guess that still changes when it makes sense to rebuild the images (it's closer to monthly, or to when opam changes).
Paolo Giarrusso (Jul 05 2020 at 16:57):and I don't see that option under https://gitlab.com/erikmd/docker-keeper-template#how-to-trigger-builds
Paolo Giarrusso (Jul 05 2020 at 16:58):@Anton Trunov meta-meta.yml is already there :-) , just called ref.yml https://github.com/coq-community/templates/blob/master/ref.yml
Paolo Giarrusso (Jul 05 2020 at 17:05):Back to docker-keeper: @Erik Martin-Dorel IIUC (and sorry if I misunderstand) docker-keeper seems thought for the _roots_ of the dependency tree, like math-comp, but less so for the _leaves_ or almost such.
Erik Martin-Dorel (Jul 05 2020 at 17:17):Hi @Paolo G. Giarrusso, actually docker-keeper can be used both for "roots" images (often called base images, e.g. coqorg/base) or for "leaves" images. Actually, any "leaf image" can serve as a base for other images ;-)
In particular, docker-keeper does not force you to have the source code of your library as a submodule! (and I wouldn't recommend using submodules as it implies a quite heavy workflow :),
so you can just as well rely on the coq opam repositories and/or doing an opam git pinning, for example?
https://gitlab.com/coq-community/docker-coq/-/blob/379668c623847c2b58742d4c2888598c30f349d0/coq/dev/Dockerfile#L21
Erik Martin-Dorel (Jul 05 2020 at 17:20):Regarding that line of the README:
This repository provides Docker images of (stable versions of) the [user/repo](https://gitlab.com/user/docker-repo) project.
I agree that this could be confusing (between the GitLab Dockerfile repo URL, and the project reference URL).
So I pushed a new version to amend that sentence, hopefully it is less confusing now.
thanks @Paolo G. Giarrusso for your feedback!
Paolo Giarrusso (Jul 05 2020 at 19:17):Erik Martin-Dorel said:
so you can just as well rely on the coq opam repositories and/or doing an opam git pinning, for example?
:thinking: ooooh, sorry; I had missed the part where I'm supposed to customize the Dockerfile.
Last updated: Dec 07 2023 at 04:02 UTC