Stream: coq-community devs & users

Topic: Handling custom dependencies in CI


view this post on Zulip Karl Palmskog (Oct 13 2020 at 20:47):

ah, here is likely the next coq-community CI problem, heuristics for handling lengthy-to-build dependencies that are not MathComp (e.g., where to put the Docker images): https://github.com/palmskog/coq-program-verification-template/issues/1

view this post on Zulip Karl Palmskog (Oct 13 2020 at 20:48):

I can easily see that we might have an exploding number of custom images if everyone uses Docker Keeper and goes wild

view this post on Zulip Théo Zimmermann (Oct 13 2020 at 21:07):

Providing Docker images with CompCert and VST does not seem a bad idea to me. In fact, when the platform is around and we have a Docker image for it, it might solve quite a few problems at once.
But another option if you're afraid of Docker image explosion would actually be to rely on CI with Nix + Cachix as @Cyril Cohen has been experimenting for math-comp.

view this post on Zulip Karl Palmskog (Oct 13 2020 at 21:12):

I'm not yet ready to take the plunge to the Nix side, but if Cyril demonstrates the benefits I might come round to it at some point

view this post on Zulip Christian Doczkal (Oct 14 2020 at 09:12):

Yes, this might become a problem indeed. I am currently working on an extension to graph-theory that relies on coq-fourcolor, another one of those developments that takes "forever" to compile. I guess the explosion of images would be not so bad if there were some images with regularly updated collections of packages. For instance, it might be reasonable for math-comp to turn (parts of) its pipeline into images once a week or so.

view this post on Zulip Théo Zimmermann (Oct 14 2020 at 09:14):

coq-fourcolor takes forever to compile even when you already have an image of math-comp ?

view this post on Zulip Christian Doczkal (Oct 14 2020 at 09:20):

I think coq-fourcolor takes more time to compile than the entirety of mathcomp. It regularly finishes well after odd-order, or any other package in the mathcomp CI pipeline for that matter. On my 8-core Laptop it takes about 10-15min, IIRC.

view this post on Zulip Karl Palmskog (Oct 14 2020 at 15:51):

I think it could become part of the Coq Platform to curate commonly used Docker images (of packages that are in the platform). Basically, we want to find the optimum of: (1) minimal image size and (2) packages most commonly used in CI

view this post on Zulip Christian Doczkal (Oct 14 2020 at 16:21):

I hate to say this, but this is precisely what (binary) package managers have been designed to do. So maybe Nix+Cachix is really the better way to go. :shrug:

view this post on Zulip Paolo Giarrusso (Oct 14 2020 at 18:23):

then you reduce the problem to “how to specify the versions you want”

view this post on Zulip Paolo Giarrusso (Oct 14 2020 at 18:24):

OTOH, when I tried, the hardest part was “enable ocaml 4.07.1+flambda since that’s not the default”, but maybe one should just change the default.

view this post on Zulip Paolo Giarrusso (Oct 14 2020 at 18:25):

“install stdpp for the non-default Coq” seemed also hard, but I managed.

view this post on Zulip Paolo Giarrusso (Oct 14 2020 at 18:27):

(with quite some trial and error and confusion, but I managed in a couple of hours)

view this post on Zulip Paolo Giarrusso (Oct 14 2020 at 18:28):

and to use Cachix (or Docker), you’d probably not have much choice in the versions to use (they’re chosen for you).

view this post on Zulip Paolo Giarrusso (Oct 14 2020 at 18:29):

TLDR: In other contexts, I’d wonder “how hard is it to translate an arbitrary opam file with fixed versions into a Nix derivation” (and it seems too hard), but maybe that doesn’t apply here.

view this post on Zulip Théo Zimmermann (Oct 15 2020 at 07:42):

Paolo Giarrusso said:

OTOH, when I tried, the hardest part was “enable ocaml 4.07.1+flambda since that’s not the default”, but maybe one should just change the default.

A new image with just 4.07.1+flambda is going to be made available and it will eventually become the default.

view this post on Zulip Théo Zimmermann (Oct 15 2020 at 07:42):

Paolo Giarrusso said:

and to use Cachix (or Docker), you’d probably not have much choice in the versions to use (they’re chosen for you).

Correct, although we could also produce cached Nix artifacts for several OCaml versions if there was a demand for it.

view this post on Zulip Théo Zimmermann (Oct 15 2020 at 07:43):

Paolo Giarrusso said:

TLDR: In other contexts, I’d wonder “how hard is it to translate an arbitrary opam file with fixed versions into a Nix derivation” (and it seems too hard), but maybe that doesn’t apply here.

@Cyril Cohen is more advanced than myself on these questions nowadays, so I'm waiting for his input / solutions.


Last updated: Feb 05 2023 at 13:02 UTC