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

rocqPackages.mathcomp-algebra: master depends on micromega-plugin

Browse Source
This commit is contained in:
Pierre Roux
2026-05-06 11:57:10 +02:00
parent 2a7a765c10
commit 30b1c85e66
6 changed files with 39 additions and 15 deletions
Download Patch File Download Diff File Expand all files Collapse all files
pkgs/development/coq-modules/graph-theory/default.nix
+4 -2
View File
@@ -52,10 +52,12 @@ mkCoqDerivation {
mathcomp.algebra
mathcomp-finmap
mathcomp.fingroup
mathcomp-algebra-tactics
fourcolor
stdlib
];
]
++ lib.optional (
mathcomp.version != "dev" && lib.versions.isLe "2.5" mathcomp.version
) mathcomp-algebra-tactics;
meta = {
description = "Library of formalized graph theory results in Coq";
pkgs/development/coq-modules/jasmin/default.nix
+4 -2
View File
@@ -38,9 +38,11 @@
release."2024.07.2".sha256 = "sha256-aF8SYY5jRxQ6iEr7t6mRN3BEmIDhJ53PGhuZiJGB+i8=";
propagatedBuildInputs = [
mathcomp-algebra-tactics
mathcomp-word
];
]
++ lib.optional (
mathcomp.version != "dev" && lib.versions.isLe "2.5" mathcomp.version
) mathcomp-algebra-tactics;
makeFlags = [
"-C"
pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix
+7 -7
View File
@@ -32,13 +32,13 @@ mkCoqDerivation {
lib.switch
[ coq.coq-version mathcomp-algebra.version ]
[
(case (range "8.20" "9.1") (isGe "2.4") "1.2.7")
(case (range "8.20" "9.1") (isGe "2.4") "1.2.6")
(case (range "8.20" "9.1") (isGe "2.4") "1.2.5")
(case (range "8.16" "9.0") (isGe "2.0") "1.2.4")
(case (range "8.16" "8.18") (isGe "2.0") "1.2.2")
(case (range "8.16" "8.19") (isGe "1.15") "1.1.1")
(case (range "8.13" "8.16") (isGe "1.12") "1.0.0")
(case (range "8.20" "9.1") (range "2.4" "2.5") "1.2.7")
(case (range "8.20" "9.1") (range "2.4" "2.4") "1.2.6")
(case (range "8.20" "9.1") (range "2.4" "2.4") "1.2.5")
(case (range "8.16" "9.0") (range "2.0" "2.3") "1.2.4")
(case (range "8.16" "8.18") (range "2.0" "2.2") "1.2.2")
(case (range "8.16" "8.19") (range "1.15" "1.19") "1.1.1")
(case (range "8.13" "8.16") (range "1.12" "1.17") "1.0.0")
]
null;
pkgs/development/coq-modules/mathcomp-infotheo/default.nix
+6 -1
View File
@@ -1,6 +1,7 @@
{
coq,
mkCoqDerivation,
mathcomp,
mathcomp-analysis,
mathcomp-analysis-stdlib,
mathcomp-algebra-tactics,
@@ -71,6 +72,10 @@
(o: {
propagatedBuildInputs =
o.propagatedBuildInputs
++ lib.optional (lib.versions.isGe "0.6.1" o.version || o.version == "dev") mathcomp-algebra-tactics
++ lib.optional (
mathcomp.version != "dev"
&& lib.versions.isLe "2.5" mathcomp.version
&& (lib.versions.isGe "0.6.1" o.version || o.version == "dev")
) mathcomp-algebra-tactics
++ lib.optional (lib.versions.isGe "0.7.2" o.version || o.version == "dev") interval;
})
pkgs/development/coq-modules/mathcomp/default.nix
+1 -1
View File
@@ -256,7 +256,7 @@ if coq.rocqPackages ? mathcomp && version != "2.3.0" && version != "2.4.0" then
fetchzip
hierarchy-builder
;
inherit (coq.rocqPackages) rocq-core;
inherit (coq.rocqPackages) rocq-core micromega-plugin;
};
in
mc
pkgs/development/rocq-modules/mathcomp/default.nix
+17 -2
View File
@@ -21,6 +21,7 @@
single ? false,
rocq-core,
hierarchy-builder,
micromega-plugin,
version ? null,
}@args:
@@ -139,8 +140,22 @@ let
extraInstallFlags = [ "-f Makefile.coq" ];
}
);
# patched-derivation1 = derivation.overrideAttrs ...
patched-derivation1 = derivation.overrideAttrs (
o:
lib.optionalAttrs
(
lib.elem package [
"algebra"
"single"
]
&& o.version != null
&& (o.version == "dev" || lib.versions.isGe "2.6.0" o.version)
)
{
propagatedBuildInputs = o.propagatedBuildInputs ++ [ micromega-plugin ];
}
);
in
derivation;
patched-derivation1;
in
mathcomp_ (if single then "single" else "all")