mathcomp: 1 -> 2

[proux01]

Diff is not very readable so here is a sumup of the change in packages that are available with default mathcomp

8.16
- coq-bits
- coqeal
- deriving
- extructures
- gaia
- gaia-hydras
- mathcomp-analysis
- mathcomp-apery
- mathcomp-classical
- mathcomp-infotheo
- multinomials

=> let's keep MC1 the default on Coq 8.16

8.17
+ mathcomp-tarjan

8.18
+ mathcomp-tarjan
+ ssprove

8.19
+ coqeal
+ gaia
+ graph-theory
+ mathcomp-tarjan
+ ssprove

8.20
+ coqeal
+ gaia
+ mathcomp-algebra-tactics
+ mathcomp-analysis
+ mathcomp-classical
+ mathcomp-real-closed
+ mathcomp-tarjan

[CohenCyril]

@proux01 Given the losses for 8.16, I would advocate keeping mathcomp 1 as default there. As for 8.17 it's on par, but out of sentimentality I would be inclined to keep mathcomp 1 so that gaia still compiles there. From 8.18 on I am in favor of switching to mathcomp 2.

[CohenCyril]

Thanks for making the experiments.

[proux01]

Makes a lot of sense. About gaia, it appears that we just never updated the Nix package with the newer release on MathComp 2, then let's switch to MC2 starting at Coq 8.17 since it's a net gain from there.

[CohenCyril]

Makes a lot of sense. About gaia, it appears that we just never updated the Nix package with the newer release on MathComp 2, then let's switch to MC2 starting at Coq 8.17 since it's a net gain from there.

Ah perfect! Well done

[proux01]

So CI seems happy and confirms that we don't remove any package