c4patino/nixpkgs
1
0
Fork 0
mirror of https://github.com/NixOS/nixpkgs.git synced 2026-07-06 17:13:24 -05:00
Code Issues Projects Releases Packages Wiki Activity

[Backport release-26.05] rocqPackages.mathcomp-analysis: now depends on real-closed (#532689)

Browse source
This commit is contained in:
Vincent Laporte 2026-06-17 15:47:36 +00:00 • committed by GitHub
commit 1dfc16dff2
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
7 changed files with 136 additions and 63 deletions
Download patch file Download diff file Expand all files Collapse all files

1
pkgs/development/coq-modules/coqeal/default.nix
View file

@ -58,6 +58,7 @@ let
release."1.0.3".sha256 = "0hc63ny7phzbihy8l7wxjvn3haxx8jfnhi91iw8hkq8n29i23v24";
propagatedBuildInputs = [
mathcomp.ssreflect
mathcomp.algebra
bignums
multinomials

1
pkgs/development/coq-modules/mathcomp-abel/default.nix
View file

@ -43,6 +43,7 @@ mkCoqDerivation {
release."1.0.0".sha256 = "190jd8hb8anqsvr9ysr514pm5sh8qhw4030ddykvwxx9d9q6rbp3";
propagatedBuildInputs = [
mathcomp.ssreflect
mathcomp.field
mathcomp-real-closed
];

2
pkgs/development/coq-modules/mathcomp-analysis/default.nix
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 [

148
pkgs/development/coq-modules/mathcomp-real-closed/default.nix
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

2
pkgs/development/rocq-modules/mathcomp-analysis/default.nix
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 =

50
pkgs/development/rocq-modules/mathcomp-real-closed/default.nix Normal file
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;
};
}

1
pkgs/top-level/rocq-packages.nix
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 { };