From 0f40a48351965b8a8cb218138d6a183b71bb1b1b Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 17 Jun 2026 08:22:18 +0200 Subject: [PATCH] rocqPackage.mathcomp-real-closed: init at 2.0.5 (cherry picked from commit 499d913a1af97416e866d5c4ecdeaad76ed708fc) --- .../coq-modules/coqeal/default.nix | 1 + .../coq-modules/mathcomp-abel/default.nix | 1 + .../mathcomp-real-closed/default.nix | 148 ++++++++++-------- .../mathcomp-real-closed/default.nix | 50 ++++++ pkgs/top-level/rocq-packages.nix | 1 + 5 files changed, 137 insertions(+), 64 deletions(-) create mode 100644 pkgs/development/rocq-modules/mathcomp-real-closed/default.nix diff --git a/pkgs/development/coq-modules/coqeal/default.nix b/pkgs/development/coq-modules/coqeal/default.nix index 3ada8a25b79a..929728ce225b 100644 --- a/pkgs/development/coq-modules/coqeal/default.nix +++ b/pkgs/development/coq-modules/coqeal/default.nix @@ -58,6 +58,7 @@ let release."1.0.3".sha256 = "0hc63ny7phzbihy8l7wxjvn3haxx8jfnhi91iw8hkq8n29i23v24"; propagatedBuildInputs = [ + mathcomp.ssreflect mathcomp.algebra bignums multinomials diff --git a/pkgs/development/coq-modules/mathcomp-abel/default.nix b/pkgs/development/coq-modules/mathcomp-abel/default.nix index bfdf24521c42..dacadca383e8 100644 --- a/pkgs/development/coq-modules/mathcomp-abel/default.nix +++ b/pkgs/development/coq-modules/mathcomp-abel/default.nix @@ -43,6 +43,7 @@ mkCoqDerivation { release."1.0.0".sha256 = "190jd8hb8anqsvr9ysr514pm5sh8qhw4030ddykvwxx9d9q6rbp3"; propagatedBuildInputs = [ + mathcomp.ssreflect mathcomp.field mathcomp-real-closed ]; diff --git a/pkgs/development/coq-modules/mathcomp-real-closed/default.nix b/pkgs/development/coq-modules/mathcomp-real-closed/default.nix index 811946457893..76bbf1161aff 100644 --- a/pkgs/development/coq-modules/mathcomp-real-closed/default.nix +++ b/pkgs/development/coq-modules/mathcomp-real-closed/default.nix @@ -7,69 +7,89 @@ version ? null, }: -mkCoqDerivation { +let + derivation = mkCoqDerivation { - namePrefix = [ - "coq" - "mathcomp" - ]; - pname = "real-closed"; - owner = "math-comp"; - inherit version; - release = { - "2.0.3".sha256 = "sha256-heZ7aZ7TO9YNAESIvbAc1qqzO91xMyLAox8VKueIk/s="; - "2.0.2".sha256 = "sha256-hBo9JMtmXDYBmf5ihKGksQLHv3c0+zDBnd8/aI2V/ao="; - "2.0.1".sha256 = "sha256-tQTI3PCl0q1vWpps28oATlzOI8TpVQh1jhTwVmhaZic="; - "2.0.0".sha256 = "sha256-sZvfiC5+5Lg4nRhfKKqyFzovCj2foAhqaq/w9F2bdU8="; - "1.1.4".sha256 = "sha256-8Hs6XfowbpeRD8RhMRf4ZJe2xf8kE0e8m7bPUzR/IM4="; - "1.1.3".sha256 = "1vwmmnzy8i4f203i2s60dn9i0kr27lsmwlqlyyzdpsghvbr8h5b7"; - "1.1.2".sha256 = "0907x4nf7nnvn764q3x9lx41g74rilvq5cki5ziwgpsdgb98pppn"; - "1.1.1".sha256 = "0ksjscrgq1i79vys4zrmgvzy2y4ylxa8wdsf4kih63apw6v5ws6b"; - "1.0.5".sha256 = "0q8nkxr9fba4naylr5xk7hfxsqzq2pvwlg1j0xxlhlgr3fmlavg2"; - "1.0.4".sha256 = "058v9dj973h9kfhqmvcy9a6xhhxzljr90cf99hdfcdx68fi2ha1b"; - "1.0.3".sha256 = "1xbzkzqgw5p42dx1liy6wy8lzdk39zwd6j14fwvv5735k660z7yb"; - "1.0.1".sha256 = "0j81gkjbza5vg89v4n9z598mfdbql416963rj4b8fzm7dp2r4rxg"; + namePrefix = [ + "coq" + "mathcomp" + ]; + pname = "real-closed"; + owner = "math-comp"; + inherit version; + release = { + "2.0.3".sha256 = "sha256-heZ7aZ7TO9YNAESIvbAc1qqzO91xMyLAox8VKueIk/s="; + "2.0.2".sha256 = "sha256-hBo9JMtmXDYBmf5ihKGksQLHv3c0+zDBnd8/aI2V/ao="; + "2.0.1".sha256 = "sha256-tQTI3PCl0q1vWpps28oATlzOI8TpVQh1jhTwVmhaZic="; + "2.0.0".sha256 = "sha256-sZvfiC5+5Lg4nRhfKKqyFzovCj2foAhqaq/w9F2bdU8="; + "1.1.4".sha256 = "sha256-8Hs6XfowbpeRD8RhMRf4ZJe2xf8kE0e8m7bPUzR/IM4="; + "1.1.3".sha256 = "1vwmmnzy8i4f203i2s60dn9i0kr27lsmwlqlyyzdpsghvbr8h5b7"; + "1.1.2".sha256 = "0907x4nf7nnvn764q3x9lx41g74rilvq5cki5ziwgpsdgb98pppn"; + "1.1.1".sha256 = "0ksjscrgq1i79vys4zrmgvzy2y4ylxa8wdsf4kih63apw6v5ws6b"; + "1.0.5".sha256 = "0q8nkxr9fba4naylr5xk7hfxsqzq2pvwlg1j0xxlhlgr3fmlavg2"; + "1.0.4".sha256 = "058v9dj973h9kfhqmvcy9a6xhhxzljr90cf99hdfcdx68fi2ha1b"; + "1.0.3".sha256 = "1xbzkzqgw5p42dx1liy6wy8lzdk39zwd6j14fwvv5735k660z7yb"; + "1.0.1".sha256 = "0j81gkjbza5vg89v4n9z598mfdbql416963rj4b8fzm7dp2r4rxg"; + }; + + defaultVersion = + let + case = coq: mc: out: { + cases = [ + coq + mc + ]; + inherit out; + }; + in + with lib.versions; + lib.switch + [ coq.version mathcomp.version ] + [ + (case (range "8.18" "9.1") (isGe "2.2.0") "2.0.3") + (case (range "8.17" "9.0") (range "2.1.0" "2.3.0") "2.0.2") + (case (range "8.17" "8.20") (range "2.0.0" "2.2.0") "2.0.1") + (case (range "8.16" "8.19") (range "2.0.0" "2.2.0") "2.0.0") + (case (range "8.13" "8.19") (range "1.13.0" "1.19.0") "1.1.4") + (case (isGe "8.13") (range "1.12.0" "1.18.0") "1.1.3") + (case (isGe "8.10") (range "1.12.0" "1.18.0") "1.1.2") + (case (isGe "8.7") "1.11.0" "1.1.1") + (case (isGe "8.7") (range "1.9.0" "1.10.0") "1.0.4") + (case (isGe "8.7") "1.8.0" "1.0.3") + (case (isGe "8.7") "1.7.0" "1.0.1") + ] + null; + + propagatedBuildInputs = [ + mathcomp.ssreflect + mathcomp.algebra + mathcomp.field + mathcomp.fingroup + mathcomp.solvable + mathcomp-bigenough + ]; + + meta = { + description = "Mathematical Components Library on real closed fields"; + license = lib.licenses.cecill-c; + }; }; - - defaultVersion = - let - case = coq: mc: out: { - cases = [ - coq - mc - ]; - inherit out; - }; - in - with lib.versions; - lib.switch - [ coq.version mathcomp.version ] - [ - (case (range "8.18" "9.1") (isGe "2.2.0") "2.0.3") - (case (range "8.17" "9.0") (range "2.1.0" "2.3.0") "2.0.2") - (case (range "8.17" "8.20") (range "2.0.0" "2.2.0") "2.0.1") - (case (range "8.16" "8.19") (range "2.0.0" "2.2.0") "2.0.0") - (case (range "8.13" "8.19") (range "1.13.0" "1.19.0") "1.1.4") - (case (isGe "8.13") (range "1.12.0" "1.18.0") "1.1.3") - (case (isGe "8.10") (range "1.12.0" "1.18.0") "1.1.2") - (case (isGe "8.7") "1.11.0" "1.1.1") - (case (isGe "8.7") (range "1.9.0" "1.10.0") "1.0.4") - (case (isGe "8.7") "1.8.0" "1.0.3") - (case (isGe "8.7") "1.7.0" "1.0.1") - ] - null; - - propagatedBuildInputs = [ - mathcomp.ssreflect - mathcomp.algebra - mathcomp.field - mathcomp.fingroup - mathcomp.solvable - mathcomp-bigenough - ]; - - meta = { - description = "Mathematical Components Library on real closed fields"; - license = lib.licenses.cecill-c; - }; -} +in +# this is just a wrapper for rocqPackages.mathcomp-real-closed for Rocq >= 9.0 +if + coq.rocqPackages ? mathcomp-real-closed + && !(lib.elem version [ + "2.0.2" + "2.0.3" + ]) +then + coq.rocqPackages.mathcomp-real-closed.override { + inherit version; + inherit + mathcomp + mathcomp-bigenough + ; + inherit (coq.rocqPackages) rocq-core; + } +else + derivation diff --git a/pkgs/development/rocq-modules/mathcomp-real-closed/default.nix b/pkgs/development/rocq-modules/mathcomp-real-closed/default.nix new file mode 100644 index 000000000000..e260b8308d0b --- /dev/null +++ b/pkgs/development/rocq-modules/mathcomp-real-closed/default.nix @@ -0,0 +1,50 @@ +{ + rocq-core, + mkRocqDerivation, + mathcomp, + mathcomp-bigenough, + lib, + version ? null, +}: + +mkRocqDerivation { + + namePrefix = [ + "rocq-core" + "mathcomp" + ]; + pname = "real-closed"; + owner = "math-comp"; + inherit version; + release = { + "2.0.5".sha256 = "sha256-nns1TF3isv8FpWqtXilfMEVKvR50fvS6MXnYVzbCzVs="; + }; + + defaultVersion = + let + case = rocq: mc: out: { + cases = [ + rocq + mc + ]; + inherit out; + }; + in + with lib.versions; + lib.switch + [ rocq-core.version mathcomp.version ] + [ + (case (range "9.0" "9.2") (isGe "2.5.0") "2.0.5") + ] + null; + + propagatedBuildInputs = [ + mathcomp.field + mathcomp-bigenough + ]; + + meta = { + description = "Mathematical Components Library on real closed fields"; + license = lib.licenses.cecill-c; + }; +} diff --git a/pkgs/top-level/rocq-packages.nix b/pkgs/top-level/rocq-packages.nix index 34af9d8c93a5..ce62650f358a 100644 --- a/pkgs/top-level/rocq-packages.nix +++ b/pkgs/top-level/rocq-packages.nix @@ -55,6 +55,7 @@ let mathcomp-classical = self.mathcomp-analysis.classical; mathcomp-experimental-reals = self.mathcomp-analysis.experimental-reals; mathcomp-finmap = callPackage ../development/rocq-modules/mathcomp-finmap { }; + mathcomp-real-closed = callPackage ../development/rocq-modules/mathcomp-real-closed { }; mathcomp-reals = self.mathcomp-analysis.reals; mathcomp-reals-stdlib = self.mathcomp-analysis.reals-stdlib; micromega-plugin = callPackage ../development/rocq-modules/micromega-plugin { };