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.
@Bas Spitters there are solutions to this indeed, but YMMV.
Give a few mins and I'll extend my answer, busy now
@Bas Spitters there have been long discussions about CI caching before. You main options are essentially:
Just FTR Erik's infrastructure for building custom Docker image is: https://gitlab.com/erikmd/docker-keeper/
@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)?
It's actually super easy. But are you suggesting we should document the steps in the Coq Nix Toolbox README? (makes sense to me)
would be very helpful, yes, if we want this to be useful outside of coq-community
@Bas Spitters , not sure what you mean by "incremental" build. Are you rebuilding different versions of fiat-crypto at each commit of your project?
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.
@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
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
Yes, that sounds like exactly what we'd like. Please tell me more :-)
@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
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
see also this recent discussion about custom Docker images
Last updated: Feb 05 2023 at 13:02 UTC