Stream: coq-community devs & users

Topic: Github CI and incremental builds


view this post on Zulip Bas Spitters (Mar 23 2022 at 15:03):

Is there experience/ good practices for incremental builds and CI. Concretely, we have a project that depends on fiat-crypto.
We'd like to test our project regularly against fiat (perhaps each commit?). However, Fiat-crypto takes a long time to compile.
Can incremental builds be used in this process. This must be a common problem.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 23 2022 at 15:08):

@Bas Spitters there are solutions to this indeed, but YMMV.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 23 2022 at 15:08):

Give a few mins and I'll extend my answer, busy now

view this post on Zulip Karl Palmskog (Mar 23 2022 at 15:09):

@Bas Spitters there have been long discussions about CI caching before. You main options are essentially:

view this post on Zulip Théo Zimmermann (Mar 23 2022 at 15:14):

Just FTR Erik's infrastructure for building custom Docker image is: https://gitlab.com/erikmd/docker-keeper/

view this post on Zulip Karl Palmskog (Mar 23 2022 at 16:08):

@Théo Zimmermann I guess the question many will ask themselves with the NIx+Cachix option is: how does one go about to set up a personal Cachix cache (namespace)?

view this post on Zulip Théo Zimmermann (Mar 23 2022 at 19:26):

It's actually super easy. But are you suggesting we should document the steps in the Coq Nix Toolbox README? (makes sense to me)

view this post on Zulip Karl Palmskog (Mar 23 2022 at 20:20):

would be very helpful, yes, if we want this to be useful outside of coq-community

view this post on Zulip Emilio Jesús Gallego Arias (Mar 24 2022 at 15:58):

@Bas Spitters , not sure what you mean by "incremental" build. Are you rebuilding different versions of fiat-crypto at each commit of your project?

view this post on Zulip Bas Spitters (Mar 25 2022 at 09:09):

We're currently using a simple coq-makefile together with fiat as a git submodule.
Ideally, I'd like to get notified if a commit to fiat breaks our development.
I guess this is a common use case.

view this post on Zulip Karl Palmskog (Mar 25 2022 at 09:12):

@Bas Spitters the best solution would be if you are part of the reverse CI dependencies of fiat-crypto. We have had a lot of success in coq-community setting up reverse dependency CI, and it's an active research topic of Théo's

view this post on Zulip Karl Palmskog (Mar 25 2022 at 09:13):

specifically, fiat-crypto would run your project as part of their CI for each of their PRs, and there ideally would be some notification mechanism when things break

view this post on Zulip Bas Spitters (Mar 25 2022 at 09:18):

Yes, that sounds like exactly what we'd like. Please tell me more :-)

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

@Bas Spitters the best illustration might be in the CI run of the Hydras & Co. project: https://github.com/coq-community/hydra-battles/actions/runs/2016528135

You can see that we test the Goedel project, which is a reverse dependency of (a package in) Hydras & Co. Section 4.2 here gives a high-level overview: https://hal.archives-ouvertes.fr/hal-03404668v2/document#page=10

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

however, reverse dependency testing will require coordination with fiat-crypto maintainers. Probably the best way is if they (may boil down to Jason Gross) use the Coq Nix Toolbox: https://github.com/coq-community/coq-nix-toolbox

view this post on Zulip Karl Palmskog (Mar 26 2022 at 20:42):

see also this recent discussion about custom Docker images


Last updated: Feb 05 2023 at 13:02 UTC