rocqPackages.mathcomp: 2.5.0 -> 2.6.0

This commit is contained in:
Pierre Roux
2026-07-17 14:31:46 +02:00
parent a16c3fde2f
commit 0de6221506
11 changed files with 22 additions and 8 deletions

View File

@@ -20,6 +20,7 @@ mkCoqDerivation {
release."1.4.0".hash = "sha256-8TtNPEbp3uLAH+MjOKiTZHOjPb3vVYlabuqsdWxbg80=";
release."1.4.1".hash = "sha256-0UASpo9CdpvidRv33BDWrevo+NSOhxLQFPCJAWPXf+s=";
release."1.4.2".hash = "sha256-d5J8j8gi6siwCLevM6y8Hf2rTB/HEfh72LLk0Qlzr0c=";
release."1.4.3".hash = "sha256-9GWz7YsgPKoDkUok6nfHHT2GGLaB2oojYizKlt8BZAg=";
inherit version;
defaultVersion =
@@ -36,8 +37,9 @@ mkCoqDerivation {
lib.switch
[ coq.coq-version mathcomp.version ]
[
(case (isGe "8.20") (isGe "2.4") "1.4.2")
(case (isGe "8.16") (isGe "2.0") "1.4.1")
(case (isGe "8.20") (isGe "2.5") "1.4.3")
(case (isGe "8.20") (range "2.4" "2.5") "1.4.2")
(case (isGe "8.16") (range "2.0" "2.4") "1.4.1")
(case (isGe "8.16") "2.0.0" "1.3.0")
(case (isGe "8.11") (range "1.12" "1.19") "1.2.5")
(case (isGe "8.11") (range "1.11" "1.14") "1.2.4")

View File

@@ -18,6 +18,7 @@ mkCoqDerivation {
release."1.17".hash = "sha256-2VzdopXgKS/wC5Rd1/Zlr12J5bSIGINFjG1nrMjDrGE=";
release."2.2".hash = "sha256-y8LlQg9d9rfPFjzS9Xu3BW/H3tPiOC+Eb/zwXJGW9d4=";
release."2.3".hash = "sha256-inWJok0F3SZpVfoyMfpRXHVHn4z2aY8JjCKKhdVTnoc=";
release."2.4".hash = "sha256-7hq2K9KMkWug2zyvB2mcy1pnpTJKg8l8vtBtUt6NcXo=";
releaseRev = (v: "v${v}");
inherit version;
@@ -35,6 +36,7 @@ mkCoqDerivation {
lib.switch
[ coq.coq-version mathcomp.version ]
[
(case (range "8.16" "9.2") (range "2.0" "2.6") "2.4")
(case (range "8.16" "9.1") (range "2.0" "2.5") "2.3")
(case (range "8.16" "9.0") (range "2.0" "2.3") "2.2")
(case (range "8.10" "8.18") (range "1.12.0" "1.18.0") "1.17")

View File

@@ -31,6 +31,7 @@ mkCoqDerivation {
lib.switch
[ coq.coq-version mathcomp-ssreflect.version ]
[
(case (range "8.16" "9.2") (range "2.0.0" "2.6.0") "1.0.5")
(case (range "8.16" "9.1") (range "2.0.0" "2.5.0") "1.0.4")
(case (range "8.16" "9.1") (range "2.0.0" "2.4.0") "1.0.3")
(case (range "8.16" "9.0") (range "2.0.0" "2.3.0") "1.0.2")
@@ -38,6 +39,7 @@ mkCoqDerivation {
(case (range "8.10" "8.16") (range "1.12.0" "1.17.0") "1.0.0")
]
null;
release."1.0.5".hash = "sha256-Ti9gwd9rV+a0MJCAOjrpuZH+F9JI1l6dNAQYmIdGreU=";
release."1.0.4".hash = "sha256-fvE53jJe7/kQUI+lhO6lKdWfsFfRjOk2YGOcHUoJ6BU=";
release."1.0.3".hash = "sha256-5lpOCDyH6NFzGLvnXHHAnR7Qv5oXsUyC8TLBFrIiBag=";
release."1.0.2".hash = "sha256-U20xgA+e9KTRdvILD1cxN6ia+dlA8uBTIbc4QlKz9ss=";

View File

@@ -33,8 +33,8 @@ mkCoqDerivation {
lib.switch
[ coq.coq-version mathcomp-algebra.version ]
[
(case (range "8.18" "9.1") (isGe "2.3.0") "1.6.0+2.3+8.18")
(case (range "8.16" "9.1") (isGe "2.0.0") "1.5.0+2.0+8.16")
(case (range "8.18" "9.1") (range "2.3.0" "2.5.0") "1.6.0+2.3+8.18")
(case (range "8.16" "9.1") (range "2.0.0" "2.5.0") "1.5.0+2.0+8.16")
(case (range "8.13" "8.20") (range "1.12" "1.19.0") "1.3.0+1.12+8.13")
(case (range "8.13" "8.16") (range "1.12" "1.17.0") "1.1.0+1.12+8.13")
]

View File

@@ -10,6 +10,7 @@ mkCoqDerivation {
pname = "odd-order";
owner = "math-comp";
release."2.4.0".hash = "sha256-8U3xFKe/gBSapwNRix3i2+jbyTja5xXGnQwtiTiF+9w=";
release."2.3.0".hash = "sha256-53FG8I9O+tsIlmaa9qy6VYyJNwWfGmhavKhbZ0VqAGc=";
release."2.2.0".hash = "sha256-z0C7+wtY8NpoT8wYqHiy8mB2HPYAeJndzDmf7Bb0mg8=";
release."2.1.0".hash = "sha256-TPlaQbO0yXEpUgy3rlCx/w1MSLECJk5tdU26fAGe48Q=";
@@ -33,6 +34,7 @@ mkCoqDerivation {
lib.switch
[ coq.coq-version mathcomp-character.version ]
[
(case (range "9.1" "9.2") (range "2.5" "2.6") "2.4.0")
(case (range "9.0" "9.1") (range "2.5" "2.5") "2.3.0")
(case (range "8.16" "9.1") (range "2.2.0" "2.4.0") "2.2.0")
(case (range "8.16" "9.0") (range "2.1.0" "2.3.0") "2.1.0")

View File

@@ -30,7 +30,7 @@ mkCoqDerivation {
lib.switch
[ coq.coq-version mathcomp-boot.version ]
[
(case (lib.versions.range "8.20" "9.1") (lib.versions.isGe "2.4") "2.2.0")
(case (lib.versions.range "8.20" "9.1") (lib.versions.range "2.4" "2.5") "2.2.0")
]
null;

View File

@@ -31,7 +31,7 @@ let
lib.switch
[ rocq-core.rocq-version mathcomp.version ]
[
(case (range "9.0" "9.1") (range "2.4.0" "2.5.0") "1.16.0")
(case (range "9.0" "9.2") (range "2.4.0" "2.6.0") "1.16.0")
]
null;

View File

@@ -25,7 +25,7 @@ mkRocqDerivation {
in
with lib.versions;
lib.switch rocq-core.rocq-version [
(case (range "9.0" "9.1") "1.0.4")
(case (range "9.0" "9.2") "1.0.4")
] null;
propagatedBuildInputs = [ mathcomp-boot ];

View File

@@ -29,10 +29,12 @@ mkRocqDerivation {
lib.switch
[ rocq-core.rocq-version mathcomp-boot.version ]
[
(case (range "9.2" "9.2") (range "2.5" "2.6") "2.2.4") # also compiles on Rocq 9.0 and 9.1 (but requires graph-theory update)
(case (range "9.0" "9.1") (range "2.3" "2.5") "2.2.2")
]
null;
release = {
"2.2.4".sha256 = "sha256-sEok7UhXiPdIH8/wzvVhXg1yprCETVmxMzeFRHh6Tug=";
"2.2.2".sha256 = "sha256-G5fSdx4MhOXtQ2H8lpyK5FuIbWAZNc7vRL3hcYmGA2o=";
};

View File

@@ -18,6 +18,7 @@ mkRocqDerivation {
inherit version;
release = {
"2.0.5".sha256 = "sha256-nns1TF3isv8FpWqtXilfMEVKvR50fvS6MXnYVzbCzVs=";
"2.0.6".sha256 = "sha256-c+0nlNTjTf115vjvnpLrgXye5YdjsWlsCBpGZj+hU9E=";
};
defaultVersion =
@@ -34,7 +35,8 @@ mkRocqDerivation {
lib.switch
[ rocq-core.version mathcomp.version ]
[
(case (range "9.0" "9.2") (isGe "2.5.0") "2.0.5")
(case (range "9.0" "9.2") (isGe "2.6.0") "2.0.6")
(case (range "9.0" "9.2") (isEq "2.5.0") "2.0.5")
]
null;

View File

@@ -35,9 +35,11 @@ let
inherit (lib.versions) range;
in
lib.switch rocq-core.rocq-version [
(case (range "9.2" "9.2") "2.6.0") # also compiles on Rocq 9.0 and 9.1
(case (range "9.0" "9.1") "2.5.0")
] null;
release = {
"2.6.0".sha256 = "sha256-SovoQ++213r8ISljts81j9E9G1vxVrFy+hhpsCw1fDY=";
"2.5.0".sha256 = "sha256-M/6IP4WhTQ4j2Bc8nXBXjSjWO08QzNIYI+a2owfOh+8=";
};
releaseRev = v: "mathcomp-${v}";