Paolo Giarrusso (Mar 01 2022 at 09:49): 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).
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.
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
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?).
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"
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
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...
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
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
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
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
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).
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
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
Karl Palmskog (Mar 01 2022 at 10:43):but isn't Iris packaged upstream anyway?
Paolo Giarrusso (Mar 01 2022 at 10:44):Yes, every commit is packaged in opam, and I can patch those if needed
Karl Palmskog (Mar 01 2022 at 10:44):https://github.com/NixOS/nixpkgs/blob/master/pkgs/development/coq-modules/iris/default.nix
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: .
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.
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
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
Karl Palmskog (Mar 01 2022 at 10:48):I think that derivation also defines "Iris-dev" or whatever you call it
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.
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).
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.
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.
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).
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.
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.
Paolo Giarrusso (Mar 01 2022 at 10:55):--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.
Paolo Giarrusso (Mar 01 2022 at 10:55): 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:
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
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 :-).
Paolo Giarrusso (Mar 01 2022 at 11:00):in particular, a good solution might avoid or reduce the need for Coq Platform images :-)
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:
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
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:
takes as input:
ARG parameter="default value" directives1.2.3 = 1.2 = 1)with several extra features, such as automatic linting of YAML and of Dockerfiles, automatic update notifications for docker-keeper, support of webhook triggers
and one or two features whose implementation is pending (required for the coq platform builds)
Last updated: Apr 19 2024 at 18:01 UTC