From 0de62215064e6cff1a67422c3fa24723380cf467 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 17 Jul 2026 14:31:46 +0200 Subject: [PATCH] rocqPackages.mathcomp: 2.5.0 -> 2.6.0 --- pkgs/development/coq-modules/fourcolor/default.nix | 6 ++++-- pkgs/development/coq-modules/gaia/default.nix | 2 ++ pkgs/development/coq-modules/mathcomp-tarjan/default.nix | 2 ++ pkgs/development/coq-modules/mathcomp-zify/default.nix | 4 ++-- pkgs/development/coq-modules/odd-order/default.nix | 2 ++ pkgs/development/coq-modules/wasmcert/default.nix | 2 +- pkgs/development/rocq-modules/mathcomp-analysis/default.nix | 2 +- .../development/rocq-modules/mathcomp-bigenough/default.nix | 2 +- pkgs/development/rocq-modules/mathcomp-finmap/default.nix | 2 ++ .../rocq-modules/mathcomp-real-closed/default.nix | 4 +++- pkgs/development/rocq-modules/mathcomp/default.nix | 2 ++ 11 files changed, 22 insertions(+), 8 deletions(-) diff --git a/pkgs/development/coq-modules/fourcolor/default.nix b/pkgs/development/coq-modules/fourcolor/default.nix index 3dfa427a2f7a..8359575a4e32 100644 --- a/pkgs/development/coq-modules/fourcolor/default.nix +++ b/pkgs/development/coq-modules/fourcolor/default.nix @@ -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") diff --git a/pkgs/development/coq-modules/gaia/default.nix b/pkgs/development/coq-modules/gaia/default.nix index 3252dddbbac3..abf16a0336f7 100644 --- a/pkgs/development/coq-modules/gaia/default.nix +++ b/pkgs/development/coq-modules/gaia/default.nix @@ -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") diff --git a/pkgs/development/coq-modules/mathcomp-tarjan/default.nix b/pkgs/development/coq-modules/mathcomp-tarjan/default.nix index ec3162fbd29b..d86510376a25 100644 --- a/pkgs/development/coq-modules/mathcomp-tarjan/default.nix +++ b/pkgs/development/coq-modules/mathcomp-tarjan/default.nix @@ -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="; diff --git a/pkgs/development/coq-modules/mathcomp-zify/default.nix b/pkgs/development/coq-modules/mathcomp-zify/default.nix index 8642a58a073c..06b9ec660bea 100644 --- a/pkgs/development/coq-modules/mathcomp-zify/default.nix +++ b/pkgs/development/coq-modules/mathcomp-zify/default.nix @@ -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") ] diff --git a/pkgs/development/coq-modules/odd-order/default.nix b/pkgs/development/coq-modules/odd-order/default.nix index dab19c066d4b..e69d05d2db6a 100644 --- a/pkgs/development/coq-modules/odd-order/default.nix +++ b/pkgs/development/coq-modules/odd-order/default.nix @@ -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") diff --git a/pkgs/development/coq-modules/wasmcert/default.nix b/pkgs/development/coq-modules/wasmcert/default.nix index 5d0c09374f99..454f6a63bd39 100644 --- a/pkgs/development/coq-modules/wasmcert/default.nix +++ b/pkgs/development/coq-modules/wasmcert/default.nix @@ -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; diff --git a/pkgs/development/rocq-modules/mathcomp-analysis/default.nix b/pkgs/development/rocq-modules/mathcomp-analysis/default.nix index 3941139e8770..96f83c3bb377 100644 --- a/pkgs/development/rocq-modules/mathcomp-analysis/default.nix +++ b/pkgs/development/rocq-modules/mathcomp-analysis/default.nix @@ -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; diff --git a/pkgs/development/rocq-modules/mathcomp-bigenough/default.nix b/pkgs/development/rocq-modules/mathcomp-bigenough/default.nix index 71f3ca0c6be2..2fd7f57d8f3a 100644 --- a/pkgs/development/rocq-modules/mathcomp-bigenough/default.nix +++ b/pkgs/development/rocq-modules/mathcomp-bigenough/default.nix @@ -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 ]; diff --git a/pkgs/development/rocq-modules/mathcomp-finmap/default.nix b/pkgs/development/rocq-modules/mathcomp-finmap/default.nix index 8e5ed395218d..7d71d4767c61 100644 --- a/pkgs/development/rocq-modules/mathcomp-finmap/default.nix +++ b/pkgs/development/rocq-modules/mathcomp-finmap/default.nix @@ -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="; }; diff --git a/pkgs/development/rocq-modules/mathcomp-real-closed/default.nix b/pkgs/development/rocq-modules/mathcomp-real-closed/default.nix index 8a8fa9c78a2c..8f26ad0b6dbe 100644 --- a/pkgs/development/rocq-modules/mathcomp-real-closed/default.nix +++ b/pkgs/development/rocq-modules/mathcomp-real-closed/default.nix @@ -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; diff --git a/pkgs/development/rocq-modules/mathcomp/default.nix b/pkgs/development/rocq-modules/mathcomp/default.nix index 05de2bbd843c..1c25a1bbe76d 100644 --- a/pkgs/development/rocq-modules/mathcomp/default.nix +++ b/pkgs/development/rocq-modules/mathcomp/default.nix @@ -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}";