coq_8_13: init at 8.13+β1

[vbgl]

Motivation for this change

Prepare for the next release: https://github.com/coq/coq/releases/tag/V8.13%2Bbeta1

NB: the addition of mathcomp libraries at version 1.12 is just to fix the build with Coq 8.13: it’s a minimal change to avoid conflicts and work duplication with Cyril’s refactoring (in #105877).

cc maintainers @roconnor @thoughtpolice @Zimmi48

Things done

• Tested using sandboxing (nix.useSandbox on NixOS, or option sandbox in nix.conf on non-NixOS linux)
• Built on platform(s)
  • NixOS
  • macOS
  • other Linux distributions
• Tested via one or more NixOS test(s) if existing and applicable for the change (look inside nixos/tests)
• Tested compilation of all pkgs that depend on this change using nix-shell -p nixpkgs-review --run "nixpkgs-review wip"
• Tested execution of all binary files (usually in ./result/bin/)
• Determined the impact on package closure size (by running nix path-info -S before and after)
• Ensured that relevant documentation is up to date
• Fits CONTRIBUTING.md.

[Zimmi48]

LGTM, thanks for clarifying the minimality of changes to math-comp packages.

[SuperSandro2000]

Can we limit the amount of packages? I don't think we need 10 versions in nixpkgs.

[vbgl]

I agree that ten versions of Coq might be too much. In particular compatibility across versions is much better than what it used to be.

How many of them should we keep? And which ones?

[SuperSandro2000]

Result of nixpkgs-review pr 106427 run on x86_64-linux 1

1 package built:

• coq_8_13

[Zimmi48]

How many of them should we keep? And which ones?

How does this selection work in other languages? I think for OCaml we also keep all the versions in a given range (currently, we have 13, from OCaml 4.00 to OCaml 4.12). Are there examples of language compilers for which some intermediate versions are dropped from nixpkgs?

[vbgl]

A data point: there is this issue, that is still open #54556

[SuperSandro2000]

How many of them should we keep? And which ones?

How does this selection work in other languages? I think for OCaml we also keep all the versions in a given range (currently, we have 13, from OCaml 4.00 to OCaml 4.12). Are there examples of language compilers for which some intermediate versions are dropped from nixpkgs?

General rule is 3 versions. I think terrarform is a recent example I have seen.

Keeping all patch versions is not required. We can keep different major versions and minor versions of there is a use case.

[Zimmi48]

Terraform is probably not the best comparison because it's not a language compiler. In nixpkgs, language compilers tend to have many more versions than 3. I gave the OCaml example (with its 13 versions) because this is the example I know the most, but I'd be interested in other examples. Python for instance has 2.7, 3.6, 3.7, 3.8, 3.9.

It seems like a reasonable strategy to drop very old versions (especially when they become a hassle to maintain) but to keep a whole range between the oldest supported and the latest version. Patch-level releases are indeed probably not useful, but not a problem either if they only add one line with a sha256 to the derivation and nothing else (in particular, they are not exported to the package list).

Another aspect to take into consideration is the release frequency and the level of compatibility between releases. In the case of Coq, major releases are frequent (every 6 months) and introduce incompatibilities (although not as many as before) that tend to require an update of the packages that depend on Coq.

[vbgl]

Let’s merge this so that we can update 8.12 to 8.12.2 and avoid merge conflicts.