New Nix CI setup.

[Zimmi48]

I'm opening this PR to test the new Nix CI setup I have been working on following discussions with @palmskog on a project with extra Coq dependencies.

[Zimmi48]

So this works quite well. I'm leaving the PR open for the maintainers to decide whether it's interesting having or not. A feature is that v8.14 is tested. Another is that it's quite fast. I could remove 8.13 testing if you don't think it's useful to have. Let me know what you think.

[palmskog]

This looks like a really good idea to me, and I think it should be merged. However, I will first take the liberty to make sure we test both the Dune builds and the coq_makefile builds in CI, by making the opam packages use Dune (this is arguably one of the big benefits of this setup). Then, I will leave the ultimate merging decision to @chdoc.

[chdoc]

I am happy to use this project also as a test case for the nix-based CI. I guess the project is lightweight enough that we can run various CI configurations.

I am a bit confused that the meta.yml file still reads dune: false though. Shouldn't this be set to true?

[palmskog]

@chdoc if we set dune: true, then Dune also shows up as a dependency in README.md and is used in the build instructions. Are you sure this is what you want? I typically circumvent this by setting dune: true when I generate the opam packages, and then switch back to dune: false.

[chdoc]

I don't have strong feelings about this. I think it's good if meta.yml, the generated files, and the opam files in the opam-coq-archive are as much in sync as possible. Less things to screw up when regenerating or making a release. Also, it looks like dune will be a dependency of coq-8.14. So very soon, everybody will be using dune.

[palmskog]

So very soon, everybody will be using dune.

Well, everybody will have Dune installed and available, but this is very far from that Dune is fully replacing coq_makefile. My bet is that (1) Dune long term support for Coq is at least a year away and (2) we are several years away from most people using Dune to build their Coq projects. Hence, I still think supporting both build approaches is the correct choice.

[chdoc]

Sure, I wasn't suggesting that coq_makefile is going to be replaces any time soon. It's going to take a while until all the make trickery that people have created over decades is nicely supported by dune. Also, IDE support (ProofGeneral) was still lacking the last time I checked. But all of this is besides the point. Anyway, let's just merge this as is.