Stream: coq-community devs & users

Topic: Custom docker images


view this post on Zulip Paolo Giarrusso (Mar 01 2022 at 09:49):

Is there a convenient way to setup per-project docker images, with the deps you need? My current setup for that is a bit clunky, even if at least they're built via GitHub Actions (https://github.com/Blaisorblade/docker-dot-iris). Right now I even duplicate the dependencies (I used to get them from a submodule with my project, but submodules are too clunky).

view this post on Zulip Karl Palmskog (Mar 01 2022 at 09:50):

I think Erik's infrastructure is probably the best choice for this: https://gitlab.com/erikmd/docker-keeper/-/wikis/home

But maybe @Erik Martin-Dorel could comment on this particular mode of use.

view this post on Zulip Paolo Giarrusso (Mar 01 2022 at 09:52):

I agree it's the most developer Docker infrastructure for Coq usage, but I am not sure I've seen hints about this mode of usage

view this post on Zulip Paolo Giarrusso (Mar 01 2022 at 09:53):

It seems most people just install dependencies (outside Coq) in each CI run, which is fine if those are fast (or if you're patient?).

view this post on Zulip Paolo Giarrusso (Mar 01 2022 at 09:54):

A good reason for that is I don't have a convenient story for upgrading dependencies, beyond "I manually create a new image and change configs in a couple of repos"

view this post on Zulip Karl Palmskog (Mar 01 2022 at 09:54):

yes, the basic Docker images + opam goes quite a long way unless you have long-running deps

view this post on Zulip Paolo Giarrusso (Mar 01 2022 at 09:55):

I only need Iris, but I think it takes about as much as my code or more...

view this post on Zulip Karl Palmskog (Mar 01 2022 at 09:55):

my feeling is that Nix + Coq-Nix-toolbox could provide a sweet spot for projects with some custom long-running deps: https://github.com/coq-community/coq-nix-toolbox

view this post on Zulip Karl Palmskog (Mar 01 2022 at 09:56):

if you only want to add Iris, I think Docker-keeper should be the way to go

view this post on Zulip Paolo Giarrusso (Mar 01 2022 at 09:56):

OTOH let's face it, everything in my repo tends to over-engineered for fun/learning experience

view this post on Zulip Karl Palmskog (Mar 01 2022 at 09:57):

I think adding Iris to Docker-Coq is basically (in theory) just one small commit for Erik, although I don't know how easy his setup is to replicate

view this post on Zulip Paolo Giarrusso (Mar 01 2022 at 10:40):

no, I think that setup is just not designed for what I'd like; while Nix requires packaging my dependencies in Nix. The ideal input is just my opam file. In practice, I'm happy to push any kind of metaphorical button when I change it. And to copy-paste any amount of fixed code to my repo (either the main one or a second one).

view this post on Zulip Paolo Giarrusso (Mar 01 2022 at 10:40):

But judging from the mathcomp image, this is just not how things are setup:

https://gitlab.com/math-comp/docker-mathcomp/-/blob/master/images.yml
https://gitlab.com/math-comp/docker-mathcomp/-/blob/master/mathcomp/single/Dockerfile
https://gitlab.com/math-comp/docker-mathcomp/-/blob/master/mathcomp/dual/Dockerfile

view this post on Zulip Karl Palmskog (Mar 01 2022 at 10:42):

the Coq-Nix-Toolbox makes packaging "standard" Coq projects nearly trivial. See for example Huffman package here added/generated by Cyril in a minute: https://github.com/coq-community/huffman/blob/master/.nix/coq-overlays/huffman/default.nix

view this post on Zulip Karl Palmskog (Mar 01 2022 at 10:43):

but isn't Iris packaged upstream anyway?

view this post on Zulip Paolo Giarrusso (Mar 01 2022 at 10:44):

Yes, every commit is packaged in opam, and I can patch those if needed

view this post on Zulip Karl Palmskog (Mar 01 2022 at 10:44):

https://github.com/NixOS/nixpkgs/blob/master/pkgs/development/coq-modules/iris/default.nix

view this post on Zulip Paolo Giarrusso (Mar 01 2022 at 10:45):

I've never actually had to patch Iris, but in 2 years I haven't ever run on standard upstream packages more or less of anything :sweat_smile: .

view this post on Zulip Théo Zimmermann (Mar 01 2022 at 10:46):

Since Iris is already available in nixpkgs (as pointed by Karl), you can just use this definition (if you go Coq Nix Toolbox) to run the dev version (or any revision really) of Iris.

view this post on Zulip Karl Palmskog (Mar 01 2022 at 10:47):

my opinion is essentially that Docker-Coq+more-packages is cleaner if done correctly in style of Docker Keeper, but Nix gets you cached builds at package level with less work

view this post on Zulip Paolo Giarrusso (Mar 01 2022 at 10:48):

@Théo Zimmermann I see that Iris releases are packaged there, but I don't know anybody using Iris releases

view this post on Zulip Karl Palmskog (Mar 01 2022 at 10:48):

I think that derivation also defines "Iris-dev" or whatever you call it

view this post on Zulip Paolo Giarrusso (Mar 01 2022 at 10:48):

I'm sure that _if I knew Nix_ I could tweak that to package some other version, but I don't.

view this post on Zulip Théo Zimmermann (Mar 01 2022 at 10:49):

@Paolo Giarrusso You're missing my point: you do not have to use Iris releases when using Nix. The fact that there is a nixpkgs derivation is enough and you can override it with any version (very easily).

view this post on Zulip Théo Zimmermann (Mar 01 2022 at 10:49):

You don't even have to learn Nix in fact, you just have to follow the instructions in the Coq Nix Toolbox README.

view this post on Zulip Paolo Giarrusso (Mar 01 2022 at 10:50):

I have tried using Nix, and put more effort into it than opam, but I've honestly given up.

view this post on Zulip Paolo Giarrusso (Mar 01 2022 at 10:51):

Goalpost warning: I'm also thinking of (work) needs, which are a bit different. But even for dot-iris, I've had to enable flambda myself in the past years (dunno if that's fixed now).

view this post on Zulip Théo Zimmermann (Mar 01 2022 at 10:52):

OK, if you need to deviate from the default OCaml version in nixpkgs, then it might actually require more work than following a dumb README.

view this post on Zulip Théo Zimmermann (Mar 01 2022 at 10:52):

Paolo Giarrusso said:

I have tried using Nix, and put more effort into it than opam, but I've honestly given up.

Anyway, that's not relevant if you have tried before / independently of the Coq Nix Toolbox.

view this post on Zulip Paolo Giarrusso (Mar 01 2022 at 10:55):

  1. I don't think these docs are _actually_ sufficient on their own:

--arg override '{p1 = v1; ...; pn = vn;}': a very condensed inline way to select specific versions of coq or any package from coqPackages or ocamlPackages. E.g. --arg override '{coq = "8.12"; ...; mathcomp = "1.12.0";}' to override the current default bundle with the given versions.

as this mentions neither the name to use nor the right format of versions.

view this post on Zulip Paolo Giarrusso (Mar 01 2022 at 10:55):

  1. Thanks for suggesting Nix, my experience was bad enough that personally I am not going to use it, and I don't think I'm alone in this regard.

view this post on Zulip Karl Palmskog (Mar 01 2022 at 10:56):

I think you have to look at projects that actually use the Nix toolbox, like the following:

view this post on Zulip Karl Palmskog (Mar 01 2022 at 10:57):

with Nix ruled out I'd still go with Docker keeper, or failing that just create your own Docker-Coq-like image, like we did here: https://github.com/runtimeverification/vlsm/blob/master/Dockerfile

view this post on Zulip Paolo Giarrusso (Mar 01 2022 at 11:00):

I've indeed created my Docker image, and will likely keep doing that — that's reasonable enough. docker-keeper is accessible but doesn't seem to help with what I want — if other people were interested, maybe we could have a productive conversation on that :-).

view this post on Zulip Paolo Giarrusso (Mar 01 2022 at 11:00):

in particular, a good solution might avoid or reduce the need for Coq Platform images :-)

view this post on Zulip Paolo Giarrusso (Mar 01 2022 at 11:01):

I should probably have said that upthread and linked explicitly https://coq.zulipchat.com/#narrow/stream/250632-Coq-Platform.20devs.20.26.20users/topic/Docker.20images.20for.20the.20Coq.20Platform :sweat_smile:

view this post on Zulip Karl Palmskog (Mar 01 2022 at 11:06):

Docker images for the Coq Platform are needed for other applications than CI, such as for delivering artifacts for reviewing. Also, if Docker image generation is set up in a modular way, people could actually generate images by changing scripts related to the Platform, and not the Docker part

view this post on Zulip Erik Martin-Dorel (Mar 10 2022 at 23:16):

Hi, sorry I just skimmed this topic (will read it more in-depth later) but to reply to @Paolo Giarrusso:

I've indeed created my Docker image, and will likely keep doing that — that's reasonable enough. docker-keeper is accessible but doesn't seem to help with what I want — if other people were interested, maybe we could have a productive conversation on that :-).

I'd be definitely interested to be part of one such conversation :+1:

maybe the current documentation of docker-keeper does not summarize this well, but to recap quickly, docker-keeper is just a big wrapper (1.1 kLOC Py3) automated, and customizable, easy to add in any GitHub repo, without the need to be in a separated repo, but which can also be separated, that:


Last updated: Feb 04 2023 at 02:03 UTC