Lightweight Nix toolbox CI.

[Zimmi48]

This PR introduces a much lighter Nix CI toolbox-based setup (compared to #87) while improving on the legacy state (see recent discussion in #69 and coq-community/aac-tactics#77) to understand the context.

This setup doesn't require installing the toolbox in the project that uses the Nix CI template. For advanced uses of the Coq Nix Toolbox, we recommend following the standalone installation procedure instead.

One caveat is that, since this removes the template default.nix file, this means that only projects that are already available in nixpkgs (and didn't change their build procedure / dependency list) can use this CI setup. For other projects / situations, the standalone installation procedure of the Coq Nix Toolbox is still a solution.

The first commit corresponds to the state that was tested in coq-community/aac-tactics#80, coq-community/aac-tactics#81, coq-community/chapar#23 and coq-community/pocklington#3. The second commit was tested in coq-community/aac-tactics#82 (and coq-community/aac-tactics#83, coq-community/chapar#24, coq-community/pocklington#4) and coq-community/reglang#29 (a project with extra Coq dependencies).

Could be considered as closing #69 (and superseding #87).

[palmskog]

only projects that are already available in nixpkgs (and didn't change their build procedure / dependency list) can use this CI setup.

I'm not sure I fully understand this requirement. From what I remember, this is the list of projects in nixpks: https://github.com/NixOS/nixpkgs/blob/nixpkgs-unstable/pkgs/top-level/coq-packages.nix

However, Huffman is not in this list, and its CI seems to work just fine with this Nix setup: https://github.com/coq-community/huffman/actions/runs/1106532338

What am I missing?

[Zimmi48]

One caveat is that, since this removes the template default.nix file, this means that only projects that are already available in nixpkgs (and didn't change their build procedure / dependency list) can use this CI setup.

Actually, it also works for a project with no extra dependencies and using the standard build mechanism (coq_makefile with a _CoqProject file) as I just realized in coq-community/chapar#24 (comment).

[Zimmi48]

That's all thanks to the amazing work by @CohenCyril both on the mkCoqDerivation nixpkgs function and the Coq Nix Toolbox 😀

[palmskog]

This all looks good to me (and seems to work well in the projects we tried it in). However, maybe someone Nix-knowledgeable like Cyril should review as well. But fine by me also to merge it now and improve and fix over time.

[Zimmi48]

I don't think we will hear back from Cyril for a while given that he has been unresponsive on coq/coq#14723 so far.

[Zimmi48]

We can cc @siraben for a Nix eye.

[palmskog]

OK, I'll leave it up to you guys to merge this when appropriate. After this is merged, I'll go double check all the coq-community project CI-related PRs and merge them.

[siraben]

I can't comment too much on the Coq Nix toolbox as a whole (not very familiar with it yet), but going off the aac-tactics commit, this looks like an improvement by eliminating default.nix being needed in projects that want to use this for CI and has a reasonable upgrade path to flakes later.

[Zimmi48]

One question that I'm considering at this stage (since it now takes less than 10 minutes to rebuild the Coq package if it isn't in Cachix yet) is whether it is still worth keeping the https://github.com/coq/coq-on-cachix setup or whether we should just drop it.

At this point the templates do not rely on it, because for this we would need the coq/coq-on-cachix:master syntax introduced in NixOS/nixpkgs#116690. And it seems just fine like this.