Test NixOS/nixpkgs#541797.

[Zimmi48]

Test NixOS/nixpkgs#541797.

[Zimmi48]

I was getting confused with some of the errors that I get in CI, but actually, I just realized now that I should simply ignore all the pull_request_target jobs.

What I'm still having trouble understanding is why I need to keep the coqPackages references in the bundles for Rocq >= 9 (otherwise the CI files do not build, with a very cryptic error).

[Zimmi48]

Actually, it appears that there is an issue with correctly propagating the overridden versions from rocq-core to other packages. At least that's what causes the issue with math-classes in the 8.20 bundle. The derivation reveals that the bignums dependency is wrong: it is /nix/store/xwn8r9nlccns1g4scs26ngh1lhrlk83n-rocq9.1-bignums-9.0.0+rocq9.1.drv instead of a version for Coq 8.20. Note that this doesn't happen when building coqPackages_8_20.math-classes from the tested branch, so it is specifically an issue with the override mechanism.

[proux01]

I'll have a look

[proux01]

So, I rebased the nixpkgs branch and did some cleanup of the toolbox. CI here is green which is good. However, I tested it on mathcomp CI (to test other overrides than just Rocq itself): math-comp/math-comp#1634 There we can observe the following remaining issues:

• some disappearing dependencies in the action scripts (likely a toolbox issues, can be fixed later)
• some unexpected coq (instead of rocq-core) dependencies, for instance mathcomp-finmap shouldn't depend on coq, which I don't understand because the package is similar to mathcomp-bigenough which is fine (that may be an issue in nixpkgs)
• various CI failures (for instance mathcomp-single) that I should investigate further

[proux01]

Doing some more cleanup in the toolbox and a few fixes in nixpkgs, CI is finally happy both here and in math-comp/math-comp#1634
I had to give up support of Coq <= 8.20 in the toolbox but I guess it's fine (I doubt anyone is still using that).
So if you can retrieve my last few fixes from https://github.com/proux01/nixpkgs/tree/merge-bignums-derivations I think this can now be merged.

[Zimmi48]

Thanks! After this change, it might be finally time to rename the Coq Nix Toolbox to the Rocq Nix Toolbox 🎉