Github CI and incremental builds · coq-community devs & users

Stream: coq-community devs & users

Topic: Github CI and incremental builds

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.

Emilio Jesús Gallego Arias (Mar 23 2022 at 15:08):

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

Emilio Jesús Gallego Arias (Mar 23 2022 at 15:08):

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

Karl Palmskog (Mar 23 2022 at 15:09):

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

use a general purpose CI caching system like the one on GitHub (https://github.com/actions/cache)
build your own Docker containers using Erik Martin-Dorel's Docker images/scripts, and have those containers include your deps (https://github.com/coq-community/docker-coq)
use Nix and Cachix via the Coq Nix Toolbox: https://github.com/coq-community/coq-nix-toolbox

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/

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

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)

Karl Palmskog (Mar 23 2022 at 20:20):

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

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?

if not, then caching the fiat-crypto build as suggested above could help
if yes, then you may need a better incremental build system setup, something such as dune + dune cache.

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.

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

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

Bas Spitters (Mar 25 2022 at 09:18):

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

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

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

Karl Palmskog (Mar 26 2022 at 20:42):

Last updated: Jun 03 2023 at 18:01 UTC