search

coq-community / templates

Templates for configuration files and scripts useful for maintaining Coq projects [maintainers=@palmskog,@Zimmi48]
The Unlicense
13 stars 8 forks source link

Lightweight Nix toolbox CI. #99

Closed Zimmi48 closed 3 years ago

Zimmi48 commented 3 years ago

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 commented 3 years ago

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 commented 3 years ago

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 https://github.com/coq-community/chapar/pull/24#issuecomment-894670401.

Zimmi48 commented 3 years ago

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

Zimmi48 commented 3 years ago

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 commented 3 years ago

We can cc @siraben for a Nix eye.

palmskog commented 3 years ago

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.

Zimmi48 commented 3 years ago

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.