This is the topic to ask questions on the talk "A Gentle Introduction to Container-based CI for Coq projects".
Erik's talk has just started!
Note: You can run docker sudo-less in Debian/Ubuntu by adding your user to the docker
group [as the docker
binary is suid]
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?
OK, thanks!
Should we understand that coq-community/templates is the right pointer?
What is the easiest documentation?
Are your slides online?
I thought the slides mentioned docker-keeper
, but I can't find it online...
Slides will be put on the website soon ;-)
@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
Emilio Jesús Gallego Arias said:
Note: You can run docker sudo-less in Debian/Ubuntu by adding your user to the
docker
group [as thedocker
binary 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/
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)
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:
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
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?
(Let me know if these questions are too specific!).
Paolo G. Giarrusso said:
Ah, I had searched on GitHub... does
docker-keeper
work 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)
Paolo G. Giarrusso said:
(Let me know if these questions are too specific!).
(No worries, your questions are perfectly on-topic :)
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?
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?
that's a possibility, sure
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
Another possibility would be for the generate.sh
script to generate meta.yml
as well if it doesn't exist.
Might be time to rewrite this script in some saner language (OCaml, Python?) :laughing:
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.
hmm, is it possible to start from docker-base rather than docker-coq for custom images/pipeline?
Théo Zimmermann said:
Another possibility would be for the
generate.sh
script to generatemeta.yml
as 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.
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
.
(basically, I'm suggesting https://github.com/coq-community/templates/issues/19#issuecomment-604641229 as a starting point — but I realized it afterwards)
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):
ARG
uments)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
)
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))
Théo Zimmermann said:
Another possibility would be for the
generate.sh
script to generatemeta.yml
as well if it doesn't exist.
and we need a meta-meta.yml
file as the input to the generator script ;)
@Erik Martin-Dorel I thought docker-keeper
was about building Docker images which contain _my_ library — though the repository never actually says?
sorry, it does say: > This repository provides Docker images of (stable versions of) the user/repo project.
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).
and I don't see that option under https://gitlab.com/erikmd/docker-keeper-template#how-to-trigger-builds
@Anton Trunov meta-meta.yml
is already there :-) , just called ref.yml
https://github.com/coq-community/templates/blob/master/ref.yml
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.
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
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!
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: Jun 01 2023 at 11:01 UTC