Stream: Coq workshop 2020

Topic: [S5] A Gentle Introduction to Container-based CI for Coq...


view this post on Zulip 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".

view this post on Zulip Emilio Jesús Gallego Arias (Jul 05 2020 at 14:24):

Erik's talk has just started!

view this post on Zulip 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]

view this post on Zulip 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?

view this post on Zulip Enrico Tassi (Jul 05 2020 at 14:42):

OK, thanks!

view this post on Zulip Yves Bertot (Jul 05 2020 at 14:42):

Should we understand that coq-community/templates is the right pointer?

view this post on Zulip Yves Bertot (Jul 05 2020 at 14:43):

What is the easiest documentation?

view this post on Zulip 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...

view this post on Zulip Théo Zimmermann (Jul 05 2020 at 14:46):

Slides will be put on the website soon ;-)

view this post on Zulip 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

view this post on Zulip 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 the docker 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/

view this post on Zulip 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)

view this post on Zulip 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:

view this post on Zulip Erik Martin-Dorel (Jul 05 2020 at 15:11):

Paolo G. Giarrusso said:

Are your slides online?
I thought the slides mentioned docker-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

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Jul 05 2020 at 15:19):

(Let me know if these questions are too specific!).

view this post on Zulip Erik Martin-Dorel (Jul 05 2020 at 15:27):

Paolo G. Giarrusso said:

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?

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)

view this post on Zulip 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 :)

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Jul 05 2020 at 15:34):

that's a possibility, sure

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Jul 05 2020 at 15:37):

Might be time to rewrite this script in some saner language (OCaml, Python?) :laughing:

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Jul 05 2020 at 16:08):

Théo Zimmermann said:

Another possibility would be for the generate.sh script to generate meta.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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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):

If 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)

view this post on Zulip 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))

view this post on Zulip Anton Trunov (Jul 05 2020 at 16:47):

Théo Zimmermann said:

Another possibility would be for the generate.sh script to generate meta.yml as well if it doesn't exist.

and we need a meta-meta.yml file as the input to the generator script ;)

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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