State of CI testing with Nix

[Zimmi48]

It's been a long time since I said I would write this summary issue (cc @siddharthist who was interested in particular).

Overall, the current state of CI testing with Nix is documented in the wiki. It is one of the two newly established and officially supported ways of testing projects depending on Coq, the other being opam + Docker (see comparison here). Both setups avoid to rebuild Coq at every test or depend on an outdated opam cache.

Both setups should allow in theory to reuse build artifacts to build reverse-dependencies (e.g. corn which depends on math-classes) or the various packages depending on math-comp. In the case of Docker, it is a matter of generating a Dockerfile and pushing the new image to a Docker registry (either dockerhub when building the master branch, or GitLab's registry when building any branch, see discussion at math-comp/math-comp#256).

In the case of Nix, it requires pushing to a cache on Cachix. This should be very easy to setup as soon as this is tested and documented. However, my initial tests did not work. The main difficulty is to make sure that the exact same derivation is built on the CI that is going to push to Cachix as is required in the depending builds. The problem is that the derivation depends in turn on the source derivation. Depending how it is built, it may be sensible to the name of the directory which contains it.

For instance, the default.nix file of Coq takes it source from the current directory, and this is also the case for the proposed template default.nix in this repository. When building with nix build, the source will be copied to the nix store in a repository like /nix/store/l14sddwdd8lrji8qp900jcd12h4w1sgq-name where name is the name of the directory that contained the sources in the filesystem. This is highly unstable. That's why in Coq's .gitlab-ci.yml, we do not run nix build on the sources but we do nix build -E "import (fetchTarball $CI_PROJECT_URL/-/archive/$CI_COMMIT_SHA.tar.gz) {}". The fetchTarball operation will always copy the sources to a location in the Nix store that only depends on the content of the tarball. Then our template default.nix for projects depending on Coq will load the Coq dependency in the same way (using fetchTarball again).

A similar trick will be needed to be able to make the build artifacts that we upload to Cachix reusable, unless another way of fixing this instability is found (cc @vbgl to which I talked about these issues already).

[Zimmi48]

I have had the feeling of hitting a wall while trying to extend the current default.nix template to support using development branches of Coq package dependencies.

The problem

The goal is to extend the current Nix's CI setup to support corn in particular. Corn depends on math-classes and bignums. Both have development branches that are compatible with Coq master, but their latest released version (available through nixpkgs.coqPackages) is not.
The same issue could happen for the build of lemma-overloading if the current version of Coq had to break the latest released version of mathcomp-ssreflect.

The concept of development package that tracks a branch instead of being pinned to a particular revision exists in opam but it doesn't exists in Nix and that's the core issue here.

The solution I tried

The idea was to make it possible to depend on a development branch of a package by accepting a generic coqPackagesInfo argument which contains URLs of source tarballs for the dependencies. This argument is passed in turn to dependencies for their own build. To understand this, it is best to look at these examples:

• https://github.com/Zimmi48/bignums/blob/coqPackagesInfo/default.nix
• https://github.com/Zimmi48/math-classes/blob/coqPackagesInfo/default.nix
• https://github.com/Zimmi48/corn/blob/coqPackagesInfo/default.nix

For instance, one can get a shell to build corn by running nix-shell --arg coqPackagesInfo '{ coq = "https://github.com/coq/coq/tarball/master"; bignums = "https://github.com/Zimmi48/bignums/tarball/coqPackagesInfo"; math-classes = "https://github.com/Zimmi48/math-classes/tarball/coqPackagesInfo"; }'.

The limitation

This supposes that all the dependencies have a default.nix built on the same model.
This won't work for instance for lemma-overloading because math-comp doesn't ship any default.nix.
The solution currently in place in https://github.com/coq-community/math-classes/blob/master/default.nix is using the package definition from nixpkgs. I have imitated this idea at https://github.com/Zimmi48/lemma-overloading/blob/coqPackagesInfo/default.nix. This is however somewhat rigid on the way the package must be built.

EDIT: using the package definition from nixpkgs has the additional drawback of having to override all the dependencies of said package with versions corresponding to development branches.

While figuring out what to do here, I'm only using opam to test for compatibility of corn with Coq master in coq-community/corn#66.

[Zimmi48]

I'd like to have a look at the future of our templates for building with Nix on CI.

CI with Nix was the first solution that was explored in our templates (before docker-coq existed) but since then, I've had little time to devote to it and meanwhile, @erikmd has made CI with Docker better and better.

Right now, we support three CI providers in our templates: Travis, CircleCI and GitHub Actions. Only our Travis support also includes Nix support.

Reading https://discourse.nixos.org/t/fate-of-travis-ci-nix-language-support/7907, it looks like the Nix community is massively moving over to GitHub Actions and Nix community support for Travis is going to end soon. I have no experience yet with GitHub Actions for Nix but @CohenCyril does (and it looks simple enough).

It seems to me that it would be a bit sad to renounce entirely to CI with Nix, especially because, to me, Nix is still the easiest way to easily get the dependencies one needs to build a project (when using it locally, it seems more flexible than Docker for instance and more powerful than opam).

OTOH, it seems that the flexibility brought by opam regarding multiple version testing cannot be matched by Nix (although @CohenCyril is again more active and knowledgeable than myself on the current evolution of Coq packaging in nixpkgs and the support of multiple package versions). The problem I mentioned in my previous post that sometimes you need to test with the dev version of your dependencies, that might be packaged in opam but not in Nix still looks unsolved to me.

Finally, a minor point regarding this issue:

The problem is that the derivation depends in turn on the source derivation. Depending how it is built, it may be sensible to the name of the directory which contains it.

I was told of a solution about one year ago, but I still haven't tested it yet 🤦

[CohenCyril]

Hi! Thanks for pinging me @Zimmi48. I indeed experimented a lot with nix for mathcomp, I am not entirely satisfied with the current result, but I have plans to make it better and extend to all coq packages. With cachix and github actions, it leads to really quick and reproducible CI, and I even intend to provide "copy vo" feature to get started instantaneously e.g. when checking out a branch that already passed CI.

Regarding multiple version testing I found a very light way to do it, i.e. by just naming the repo/branch where to fetch the new sources (cf https://github.com/NixOS/nixpkgs/blob/master/pkgs/development/coq-modules/mathcomp/extra.nix#L345-L366 which I need to generalize, refactor and make available for almost any package), but for now without guards (to assert a given set of versions is going to compile). One might say this is a disadvantage wrt opam, but while preparing a few mathcomp nix packages I realized that some combinations I expected to work did not. Indeed, opam lets you describe constraints, but resolution is performed at installation time, leaving the user to deal with potential conflicts, for good or bad reasons, that the developers might ignore and may want to fix. On the other hand, nix forces the person who makes the packages to handpick versions that go well together (https://github.com/NixOS/nixpkgs/blob/master/pkgs/development/coq-modules/mathcomp/extra.nix#L206-L287 actually putting all of it in the same file was one of the mistakes I am going to fix) and I believe that it is a very good thing to have human intervention at this stage. Then CI has to test only a carefully picked set of packages (e.g. https://github.com/math-comp/math-comp-nix/actions/runs/138819891/workflow) and end-users are provided ready-to-use versions of the various libraries, but may alter some versions if they mean it (e.g. https://github.com/math-comp/analysis/blob/e2bab6f145d62cde3c15472175983733989e6e14/config.nix is overriding default packages)

[Zimmi48]

@palmskog reported that Cachix's caching has been failing on Travis recently and this is despite the fact that I pushed a fix related to a similar issue just two months ago (b880f68). I didn't have time yet to figure out what's going wrong this time, but this hints again that our Nix on Travis support isn't really sustainable. As I mentioned in #73, I'd like to start recommending GitHub Actions as the preferred CI provider but this would be a shame to do so without having a template for Nix testing first. @CohenCyril would you be willing to contribute such a template based on your experience and what you know works fine as of today?

[CohenCyril]

@Zimmi48 I intend to contribute, but with CPP's deadline, it might not be before the end of the month. Is it an emergency?

[Zimmi48]

Thank you.
Not an emergency, of course!

[Zimmi48]

@CohenCyril Friendly reminder of this issue now that the CPP deadline has passed 😉

[CohenCyril]

Thi task is scheduled for next week!

[Zimmi48]

Due to new critically low build minute limits introduced by Travis CI, we are going to switch coq-community projects that relied on Travis to GitHub Actions (see https://coq.zulipchat.com/#narrow/stream/237663-coq-community-devs.20.26.20users/topic/New.20Travis.20limits.2E). This means that projects won't be tested with Nix anymore until there is a GitHub Action template for Nix. For some projects, it was especially useful because the Nix setup tested the build with make while the opam setup tested the build with dune.

@CohenCyril do you have an update on your progress?

[CohenCyril]

I did not manage to do it so far, the time I allocated for this was too short.
I will try again next week, and if I do not succeed, I wouldn't mind a group session on this at the CUDW (or before).

[Zimmi48]

A use case that is not easily solved by Docker-Coq-Action was raised in coq-community/docker-coq-action#51. It is the one of easily installing any given version of Coq with any given version of Haskell or Python. The Nix-based CI template could be a good fit for this use case.

[Zimmi48]

An update of this issue: we have been working a lot with Cyril at improving the Nix support for the Coq ecosystem. There is now a (still unstable until the first release) coq-nix-toolbox and the templates are soon going to be updated to rely on it for Nix-based CI (#87).

We have also subscribed to a larger Cachix storage for the Coq community. To start with, this will benefit Coq, math-comp and coq-community, but we should be able to include other organizations or users that would benefit from this.

Apart from releasing an initial version of the coq-nix-toolbox and merging the corresponding template PR, other to-do items are:

• Updating the documentation, in particular the one at https://github.com/coq/coq/wiki/Nix.
• Using the coq-nix-toolbox infrastructure in the Coq repo instead of the custom one that we have today.

[palmskog]

It looks like Nix CI with Cachix is broken for tarballs once again, I'm getting full 20 min builds every time since about a week, for example: https://github.com/coq-community/aac-tactics/runs/3240237246

I'm guessing this will be fixed by the Nix toolbox? In the meantime, maybe we want to completely avoid Nix CI for all tarball builds.

[Zimmi48]

Yes, sorry that's my fault. I've started the transition of Coq's CI to the toolbox infrastructure. Depending on how much needed this legacy CI setup is, I can either prepare a PR on the Coq side to fix the problem, or we can disable the legacy CI system on the few projects that are left using it.

[palmskog]

@Zimmi48 the main problem right now is that we have no CI option for 8.14 except using Nix.

As I pointed out in coq-community/aac-tactics#77 the Nix toolbox approach is way too complex for me to handle, so when Docker support for 8.14 arrives, I will disable Nix CI in all my projects.

[Zimmi48]

@palmskog the PR that broke the binary cache for your use case (coq/coq#14590) hasn't yet been backported, so 8.14 testing should still work as before.

I also acknowledge your use case and point of view on the toolbox and will think about providing a simpler, toolbox-compatible, Nix CI setup. I'm expecting this should be quite doable.

[palmskog]

But the CI run I linked to (https://github.com/coq-community/aac-tactics/runs/3240237246) was already using 8.14, namely, https://github.com/coq/coq-on-cachix/tarball/v8.14, and I still got the 27 min running time. What do I need to do for 8.14 caching to work?

Sounds good that there could be a simple CI setup for Nix. It looks like we are going to spend several more years of using both coq_makefile and Dune concurrently for many projects, so I think testing them both is essential.

[Zimmi48]

OK, then my interpretation of why it was not working as before wasn't correct. That being said, instead of investigating the reason, I will work at providing a lightweight toolbox-based alternative, that should hopefully also be more robust in the long run.