gador/nixpkgs
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

rocqPackages.mathcomp-analysis: now depends on real-closed (#532543)

Browse Source
This commit is contained in:
Vincent Laporte
2026-06-17 14:35:15 +00:00
committed by GitHub
parent 6d581676f0 36d1ce50a7
commit f8a250e19b
7 changed files with 139 additions and 66 deletions
Download Patch File Download Diff File Expand all files Collapse all files
pkgs/development/coq-modules/coqeal/default.nix
+1
View File
@@ -58,6 +58,7 @@ let
release."1.0.3".sha256 = "0hc63ny7phzbihy8l7wxjvn3haxx8jfnhi91iw8hkq8n29i23v24";
propagatedBuildInputs = [
mathcomp.ssreflect
mathcomp.algebra
bignums
multinomials
pkgs/development/coq-modules/mathcomp-abel/default.nix
+1
View File
@@ -43,6 +43,7 @@ mkCoqDerivation {
release."1.0.0".sha256 = "190jd8hb8anqsvr9ysr514pm5sh8qhw4030ddykvwxx9d9q6rbp3";
propagatedBuildInputs = [
mathcomp.ssreflect
mathcomp.field
mathcomp-real-closed
];
pkgs/development/coq-modules/mathcomp-analysis/default.nix
-2
View File
@@ -4,7 +4,6 @@
mathcomp,
mathcomp-finmap,
mathcomp-bigenough,
mathcomp-real-closed,
hierarchy-builder,
stdlib,
single ? false,
@@ -105,7 +104,6 @@ let
analysis-deps = [
mathcomp.field
mathcomp-bigenough
mathcomp-real-closed
];
intra-deps = lib.optionals (package != "single") (map mathcomp_ packages.${package});
pkgpath = lib.switch package [
pkgs/development/coq-modules/mathcomp-real-closed/default.nix
+84 -64
View File
@@ -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
pkgs/development/rocq-modules/mathcomp-analysis/default.nix
+2
View File
@@ -4,6 +4,7 @@
mathcomp,
mathcomp-finmap,
mathcomp-bigenough,
mathcomp-real-closed,
stdlib,
single ? false,
rocq-core,
@@ -58,6 +59,7 @@ let
analysis-deps = [
mathcomp.field
mathcomp-bigenough
mathcomp-real-closed
];
intra-deps = lib.optionals (package != "single") (map mathcomp_ packages.${package});
pkgpath =
pkgs/development/rocq-modules/mathcomp-real-closed/default.nix
+50
View File
@@ -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;
};
}
pkgs/top-level/rocq-packages.nix
+1
View File
@@ -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 { };