Update the Nix setup to rely on the Coq Nix Toolbox.

[Zimmi48]

Use the dynamic workflow generation.

(Testing coq-community/templates#87.)

• Remove the former Nix CI setup.

[palmskog]

One general comment: this setup is completely opaque to anyone who doesn't know Nix and Cachix. With the previous setup, I could at least extrapolate what an option meant, but there is just no hope with stuff like nix-bundles, nix-default, all the different *.nix files, etc.

[Zimmi48]

nix-default might not be a very well-chosen name given that it indicates which version of the toolbox to use. It was anyway an artifact of testing an outdated branch and can be removed now. And I'd like to make the Cachix configuration unnecessary for coq-community projects wince it will virtually always be the same. But I didn't succeed yet (see coq-community/templates#87 (comment)).

"Bundle" isn't a Nix term but a toolbox-specific term. We tried to document it in the toolbox repository and in the templates PR. Basically, it describes a set of compatible package versions.

But your comment isn't just about the meta.yml changes but also about the auto-generated files, right? I don't think there's any hope in making these files easier to understand as there's this natural tendency when you add more and more features that auto-generated files will become more and more complex. Eventually, we should just mask out these changes in PRs with a .gitattributes setup (as discussed in coq-community/templates#71). That being said .nix/fallback-config.nix does contain some documentation.

[palmskog]

I understand that with increased generality comes more files and options, but at the point where 3-4 options and 4+ files are needed for Nix CI, I think we should recommend smaller projects to go with Docker only. At least I think I will do that with my own private small projects.

[Zimmi48]

Well, until now the Nix setup was very limited and didn't stand the comparison with the Docker-Coq setup. It's becoming interesting only now. In particular, if you have dependencies that are not pre-built in one of the Docker images or if you want to easily test reverse dependencies. AAC-Tactics is not the best example to demonstrate that.

[Zimmi48]

Here is a new version of the PR, based on a lightweight toolbox-based setup. I've included a .travis.yml file to test it (done at https://travis-ci.com/github/Zimmi48/aac-tactics/jobs/529539984) that I will remove in the next force-push.

We need coq/coq#14723 to get Coq master commits to be properly pushed to the coq Cachix once more, but in the meantime they are still pushed by the GitHub Action to the coq-community Cachix, so if Coq hasn't been updated between two runs, the runs are still sped up.

We will also need NixOS/nixpkgs#116690 to go back to using the coq-on-cachix repo to always get a prebuilt Coq.

[Zimmi48]

First run took 13 minutes on GitHub Actions and 10 minutes on Travis CI (including Coq compilation). However, I cannot test the speed-up due to caching because this PR is open from a fork. I will reopen from a local branch to get access to the secret variable CACHIX_AUTH_TOKEN.