talexander/nixpkgs
1
0
Fork 0
Code Issues Pull Requests Releases Activity

coqPackages.*: better formatting fix

Browse Source
This commit is contained in:
Pierre Roux 2025-06-29 16:35:20 +02:00 committed by Vincent Laporte
parent 0a87494ff3
commit 19e4869241
47 changed files with 681 additions and 581 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
pkgs/development/coq-modules/bignums/default.nix
View File

@ -12,14 +12,15 @@
owner = "coq";
inherit version;
defaultVersion =
let
case = case: out: { inherit case out; };
in
with lib.versions;
lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: case: { inherit case out; }) {
"9.0.0+rocq${coq.coq-version}" = range "9.0" "9.0";
"9.0.0+coq${coq.coq-version}" = range "8.13" "8.20";
"${coq.coq-version}.0" = range "8.6" "8.17";
}
)) null;
lib.switch coq.coq-version [
(case (range "9.0" "9.0") "9.0.0+rocq${coq.coq-version}")
(case (range "8.13" "8.20") "9.0.0+coq${coq.coq-version}")
(case (range "8.6" "8.17") "${coq.coq-version}.0")
] null;
release."9.0.0+rocq9.0".sha256 = "sha256-ctnwpyNVhryEUA5YEsAImrcJsNMhtBgDSOz+z5Z4R78=";
release."9.0.0+coq8.20".sha256 = "sha256-pkvyDaMXRalc6Uu1eBTuiqTpRauRrzu946c6TavyTKY=";

52
pkgs/development/coq-modules/coq-elpi/default.nix
View File

@ -15,18 +15,19 @@ let
elpi-version
else
(
let
case = case: out: { inherit case out; };
in
with lib.versions;
lib.switch coq.coq-version (lib.lists.sort (x: y: lib.versions.isLe x.out y.out) (
lib.mapAttrsToList (out: case: { inherit case out; }) {
"1.11.4" = "8.11";
"1.12.0" = "8.12";
"1.13.7" = range "8.13" "8.14";
"1.15.0" = "8.15";
"1.17.0" = range "8.16" "8.17";
"1.18.1" = range "8.18" "8.19";
"2.0.7" = range "8.20" "9.0";
}
)) { }
lib.switch coq.coq-version [
(case "8.11" "1.11.4")
(case "8.12" "1.12.0")
(case (range "8.13" "8.14") "1.13.7")
(case "8.15" "1.15.0")
(case (range "8.16" "8.17") "1.17.0")
(case (range "8.18" "8.19") "1.18.1")
(case (range "8.20" "9.0") "2.0.7")
] { }
);
elpi = coq.ocamlPackages.elpi.override { version = default-elpi-version; };
propagatedBuildInputs_wo_elpi = [
@ -38,21 +39,22 @@ let
owner = "LPCIC";
inherit version;
defaultVersion =
let
case = case: out: { inherit case out; };
in
with lib.versions;
lib.switch coq.coq-version (lib.lists.sort (x: y: lib.versions.isLe x.out y.out) (
lib.mapAttrsToList (out: case: { inherit case out; }) {
"2.5.2" = range "8.20" "9.0";
"2.0.1" = "8.19";
"2.0.0" = "8.18";
"1.18.0" = "8.17";
"1.15.6" = "8.16";
"1.14.0" = "8.15";
"1.11.2" = "8.14";
"1.11.1" = "8.13";
"1.8.3_8.12" = "8.12";
"1.6.3_8.11" = "8.11";
}
)) null;
lib.switch coq.coq-version [
(case (range "8.20" "9.0") "2.5.2")
(case "8.19" "2.0.1")
(case "8.18" "2.0.0")
(case "8.17" "1.18.0")
(case "8.16" "1.15.6")
(case "8.15" "1.14.0")
(case "8.14" "1.11.2")
(case "8.13" "1.11.1")
(case "8.12" "1.8.3_8.12")
(case "8.11" "1.6.3_8.11")
] null;
release."2.5.2".sha256 = "sha256-lLzjPrbVB3rrqox528YiheUb0u89R84Xmrgkn0oplOs=";
release."2.5.0".sha256 = "sha256-Z5xjO83X/ZoTQlWnVupGXPH3HuJefr57Kv128I0dltg=";
release."2.4.0".sha256 = "sha256-W2+vVGExLLux8e0nSZESSoMVvrLxhL6dmXkb+JuKiqc=";

42
pkgs/development/coq-modules/coqeal/default.nix
View File

@ -17,27 +17,31 @@ let
inherit version;
defaultVersion =
with lib.versions;
let
cmc = c: mc: [
c
mc
];
case = coq: mc: out: {
case = [
coq
mc
];
inherit out;
};
in
lib.switch [ coq.coq-version mathcomp.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: cases: { inherit cases out; }) {
"2.1.0" = cmc (range "8.20" "9.0") (isGe "2.3.0");
"2.0.3" = cmc (range "8.16" "8.20") (isGe "2.1.0");
"2.0.1" = cmc (range "8.16" "8.20") (isGe "2.0.0");
"2.0.0" = cmc (range "8.16" "8.17") (isGe "2.0.0");
"1.1.3" = cmc (range "8.15" "8.18") (range "1.15.0" "1.18.0");
"1.1.1" = cmc (range "8.13" "8.17") (range "1.13.0" "1.18.0");
"1.1.0" = cmc (range "8.10" "8.15") (range "1.12.0" "1.18.0");
"1.0.5" = cmc (isGe "8.10") (range "1.11.0" "1.12.0");
"1.0.4" = cmc (isGe "8.7") "1.11.0";
"1.0.3" = cmc (isGe "8.7") "1.10.0";
}
)) null;
with lib.versions;
lib.switch
[ coq.coq-version mathcomp.version ]
[
(case (range "8.20" "9.0") (isGe "2.3.0") "2.1.0")
(case (range "8.16" "8.20") (isGe "2.1.0") "2.0.3")
(case (range "8.16" "8.20") (isGe "2.0.0") "2.0.1")
(case (range "8.16" "8.17") (isGe "2.0.0") "2.0.0")
(case (range "8.15" "8.18") (range "1.15.0" "1.18.0") "1.1.3")
(case (range "8.13" "8.17") (range "1.13.0" "1.18.0") "1.1.1")
(case (range "8.10" "8.15") (range "1.12.0" "1.18.0") "1.1.0")
(case (isGe "8.10") (range "1.11.0" "1.12.0") "1.0.5")
(case (isGe "8.7") "1.11.0" "1.0.4")
(case (isGe "8.7") "1.10.0" "1.0.3")
]
null;
release."2.1.0".sha256 = "sha256-UoDxy2BKraDyRsO42GXRo26O74OF51biZQGkIMWLf8Y=";
release."2.0.3".sha256 = "sha256-5lDq7IWlEW0EkNzYPu+dA6KOvRgy53W/alikpDr/Kd0=";

23
pkgs/development/coq-modules/coquelicot/default.nix
View File

@ -14,18 +14,19 @@ mkCoqDerivation {
domain = "gitlab.inria.fr";
inherit version;
defaultVersion =
let
case = case: out: { inherit case out; };
in
with lib.versions;
lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: case: { inherit case out; }) {
"3.4.3" = range "8.12" "9.0";
"3.4.2" = range "8.12" "8.20";
"3.4.0" = range "8.12" "8.18";
"3.3.0" = range "8.12" "8.17";
"3.2.0" = range "8.8" "8.16";
"3.1.0" = range "8.8" "8.13";
"3.0.2" = range "8.5" "8.9";
}
)) null;
lib.switch coq.coq-version [
(case (range "8.12" "9.0") "3.4.3")
(case (range "8.12" "8.20") "3.4.2")
(case (range "8.12" "8.18") "3.4.0")
(case (range "8.12" "8.17") "3.3.0")
(case (range "8.8" "8.16") "3.2.0")
(case (range "8.8" "8.13") "3.1.0")
(case (range "8.5" "8.9") "3.0.2")
] null;
release."3.4.3".sha256 = "sha256-bzzAIENU2OYTtmdBU9Xw8zyBvz9vqTiqjWSm7RnXXRA=";
release."3.4.2".sha256 = "sha256-aBTF8ZKu67Rb3ryCqFyejUXf/65KgG8i5je/ZMFSrj4=";
release."3.4.1".sha256 = "sha256-REhvIBl3EaL8CQqI34Gn7Xjf9NhPI3nrUAO26pSLbm0=";

30
pkgs/development/coq-modules/deriving/default.nix
View File

@ -13,21 +13,25 @@ mkCoqDerivation {
inherit version;
defaultVersion =
with lib.versions;
let
cmc = c: mc: [
c
mc
];
case = coq: mc: out: {
case = [
coq
mc
];
inherit out;
};
in
lib.switch [ coq.coq-version ssreflect.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: cases: { inherit cases out; }) {
"0.2.2" = cmc (range "8.17" "9.0") (range "2.0.0" "2.4.0");
"0.2.1" = cmc (range "8.17" "9.0") (range "2.0.0" "2.3.0");
"0.2.0" = cmc (range "8.17" "8.20") (range "2.0.0" "2.2.0");
"0.1.1" = cmc (range "8.11" "8.20") (isLe "2.0.0");
}
)) null;
with lib.versions;
lib.switch
[ coq.coq-version ssreflect.version ]
[
(case (range "8.17" "9.0") (range "2.0.0" "2.4.0") "0.2.2")
(case (range "8.17" "9.0") (range "2.0.0" "2.3.0") "0.2.1")
(case (range "8.17" "8.20") (range "2.0.0" "2.2.0") "0.2.0")
(case (range "8.11" "8.20") (isLe "2.0.0") "0.1.1")
]
null;
releaseRev = v: "v${v}";

38
pkgs/development/coq-modules/dpdgraph/default.nix
View File

@ -15,24 +15,26 @@ mkCoqDerivation {
owner = "Karmaki";
repo = "coq-dpdgraph";
inherit version;
defaultVersion = lib.switch coq.coq-version (lib.lists.sort (x: y: lib.versions.isLe x.out y.out) (
lib.mapAttrsToList (out: case: { inherit case out; }) {
"1.0+8.20" = "8.20";
"1.0+8.19" = "8.19";
"1.0+8.18" = "8.18";
"1.0+8.17" = "8.17";
"1.0+8.16" = "8.16";
"1.0+8.15" = "8.15";
"1.0+8.14" = "8.14";
"1.0+8.13" = "8.13";
"0.6.8" = "8.12";
"0.6.7" = "8.11";
"0.6.6" = "8.10";
"0.6.5" = "8.9";
"0.6.3" = "8.8";
"0.6.2" = "8.7";
}
)) null;
defaultVersion =
let
case = case: out: { inherit case out; };
in
lib.switch coq.coq-version [
(case "8.20" "1.0+8.20")
(case "8.19" "1.0+8.19")
(case "8.18" "1.0+8.18")
(case "8.17" "1.0+8.17")
(case "8.16" "1.0+8.16")
(case "8.15" "1.0+8.15")
(case "8.14" "1.0+8.14")
(case "8.13" "1.0+8.13")
(case "8.12" "0.6.8")
(case "8.11" "0.6.7")
(case "8.10" "0.6.6")
(case "8.9" "0.6.5")
(case "8.8" "0.6.3")
(case "8.7" "0.6.2")
] null;
release."1.0+8.20".sha256 = "sha256-szfH/OksCH3SCbcFjwEvLwHE5avmHp1vYiJM6KAXFqs=";
release."1.0+8.19".sha256 = "sha256-L1vjEydYiwDFTXES3sgfdaO/D50AbTJKBXUKUCgbpto=";

42
pkgs/development/coq-modules/equations/default.nix
View File

@ -12,26 +12,28 @@
repo = "Coq-Equations";
opam-name = "rocq-equations";
inherit version;
defaultVersion = lib.switch coq.coq-version (lib.lists.sort (x: y: lib.versions.isLe x.out y.out) (
lib.mapAttrsToList (out: case: { inherit case out; }) {
"1.3.1+9.0" = "9.0";
"1.3.1+8.20" = "8.20";
"1.3+8.19" = "8.19";
"1.3+8.18" = "8.18";
"1.3+8.17" = "8.17";
"1.3+8.16" = "8.16";
"1.3+8.15" = "8.15";
"1.3+8.14" = "8.14";
"1.3+8.13" = "8.13";
"1.2.4+coq8.12" = "8.12";
"1.2.4+coq8.11" = "8.11";
"1.2.1+coq8.10-2" = "8.10";
"1.2.1+coq8.9" = "8.9";
"1.2+coq8.8" = "8.8";
"1.0+coq8.7" = "8.7";
"1.0+coq8.6" = "8.6";
}
)) null;
defaultVersion =
let
case = case: out: { inherit case out; };
in
lib.switch coq.coq-version [
(case "9.0" "1.3.1+9.0")
(case "8.20" "1.3.1+8.20")
(case "8.19" "1.3+8.19")
(case "8.18" "1.3+8.18")
(case "8.17" "1.3+8.17")
(case "8.16" "1.3+8.16")
(case "8.15" "1.3+8.15")
(case "8.14" "1.3+8.14")
(case "8.13" "1.3+8.13")
(case "8.12" "1.2.4+coq8.12")
(case "8.11" "1.2.4+coq8.11")
(case "8.10" "1.2.1+coq8.10-2")
(case "8.9" "1.2.1+coq8.9")
(case "8.8" "1.2+coq8.8")
(case "8.7" "1.0+coq8.7")
(case "8.6" "1.0+coq8.6")
] null;
release."1.0+coq8.6".version = "1.0";
release."1.0+coq8.6".rev = "v1.0";

32
pkgs/development/coq-modules/extructures/default.nix
View File

@ -13,22 +13,26 @@
inherit version;
defaultVersion =
with lib.versions;
let
cmc = c: mc: [
c
mc
];
case = coq: mc: out: {
case = [
coq
mc
];
inherit out;
};
in
lib.switch [ coq.coq-version mathcomp-boot.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: cases: { inherit cases out; }) {
"0.5.0" = cmc (range "8.17" "9.0") (range "2.0.0" "2.4.0");
"0.4.0" = cmc (range "8.17" "8.20") (range "2.0.0" "2.3.0");
"0.3.1" = cmc (range "8.11" "8.20") (range "1.12.0" "1.19.0");
"0.3.0" = cmc (range "8.11" "8.14") (isLe "1.12.0");
"0.2.2" = cmc (range "8.10" "8.12") (isLe "1.12.0");
}
)) null;
with lib.versions;
lib.switch
[ coq.coq-version mathcomp-boot.version ]
[
(case (range "8.17" "9.0") (range "2.0.0" "2.4.0") "0.5.0")
(case (range "8.17" "8.20") (range "2.0.0" "2.3.0") "0.4.0")
(case (range "8.11" "8.20") (range "1.12.0" "1.19.0") "0.3.1")
(case (range "8.11" "8.14") (isLe "1.12.0") "0.3.0")
(case (range "8.10" "8.12") (isLe "1.12.0") "0.2.2")
]
null;
releaseRev = v: "v${v}";

23
pkgs/development/coq-modules/flocq/default.nix
View File

@ -14,18 +14,19 @@ mkCoqDerivation {
domain = "gitlab.inria.fr";
inherit version;
defaultVersion =
let
case = case: out: { inherit case out; };
in
with lib.versions;
lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: case: { inherit case out; }) {
"4.2.1" = range "8.15" "9.0";
"4.2.0" = range "8.14" "8.20";
"4.1.3" = range "8.14" "8.18";
"4.1.1" = range "8.14" "8.17";
"4.1.0" = range "8.14" "8.16";
"3.4.3" = range "8.7" "8.15";
"2.6.1" = range "8.5" "8.8";
}
)) null;
lib.switch coq.coq-version [
(case (range "8.15" "9.0") "4.2.1")
(case (range "8.14" "8.20") "4.2.0")
(case (range "8.14" "8.18") "4.1.3")
(case (range "8.14" "8.17") "4.1.1")
(case (range "8.14" "8.16") "4.1.0")
(case (range "8.7" "8.15") "3.4.3")
(case (range "8.5" "8.8") "2.6.1")
] null;
release."4.2.1".sha256 = "sha256-W5hcAm0GGmNsvre79/iGNcoBwFzStC4G177hZ3ds/4E=";
release."4.2.0".sha256 = "sha256-uTeo4GCs6wTLN3sLKsj0xLlt1fUDYfozXtq6iooLUgM=";
release."4.1.4".sha256 = "sha256-Use6Mlx79yef1CkCPyGoOItsD69B9KR+mQArCtmre4s=";

32
pkgs/development/coq-modules/fourcolor/default.nix
View File

@ -22,22 +22,26 @@ mkCoqDerivation {
inherit version;
defaultVersion =
with lib.versions;
let
cmc = c: mc: [
c
mc
];
case = coq: mc: out: {
case = [
coq
mc
];
inherit out;
};
in
lib.switch [ coq.coq-version mathcomp.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: cases: { inherit cases out; }) {
"1.4.1" = cmc (isGe "8.16") (isGe "2.0");
"1.3.0" = cmc (isGe "8.16") "2.0.0";
"1.2.5" = cmc (isGe "8.11") (range "1.12" "1.19");
"1.2.4" = cmc (isGe "8.11") (range "1.11" "1.14");
"1.2.3" = cmc (isLe "8.13") (lib.pred.inter (isGe "1.11.0") (isLt "1.13"));
}
)) null;
with lib.versions;
lib.switch
[ coq.coq-version mathcomp.version ]
[
(case (isGe "8.16") (isGe "2.0") "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")
(case (isLe "8.13") (lib.pred.inter (isGe "1.11.0") (isLt "1.13")) "1.2.3")
]
null;
propagatedBuildInputs = [
mathcomp.boot

30
pkgs/development/coq-modules/gaia/default.nix
View File

@ -22,21 +22,25 @@ mkCoqDerivation {
inherit version;
defaultVersion =
with lib.versions;
let
cmc = c: mc: [
c
mc
];
case = coq: mc: out: {
case = [
coq
mc
];
inherit out;
};
in
lib.switch [ coq.coq-version mathcomp.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: cases: { inherit cases out; }) {
"2.3" = cmc (range "8.16" "9.0") (range "2.0" "2.4");
"2.2" = cmc (range "8.16" "9.0") (range "2.0" "2.3");
"1.17" = cmc (range "8.10" "8.18") (range "1.12.0" "1.18.0");
"1.11" = cmc (range "8.10" "8.12") "1.11.0";
}
)) null;
with lib.versions;
lib.switch
[ coq.coq-version mathcomp.version ]
[
(case (range "8.16" "9.0") (range "2.0" "2.4") "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")
(case (range "8.10" "8.12") "1.11.0" "1.11")
]
null;
propagatedBuildInputs = [
mathcomp.boot

34
pkgs/development/coq-modules/graph-theory/default.nix
View File

@ -24,23 +24,27 @@ mkCoqDerivation {
inherit version;
defaultVersion =
with lib.versions;
let
cmc = c: mc: [
c
mc
];
case = coq: mc: out: {
case = [
coq
mc
];
inherit out;
};
in
lib.switch [ coq.coq-version mathcomp.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: cases: { inherit cases out; }) {
"0.9.6" = cmc (range "8.18" "9.0") (range "2.0.0" "2.4.0");
"0.9.4" = cmc (range "8.16" "8.19") (range "2.0.0" "2.3.0");
"0.9.3" = cmc (range "8.16" "8.18") (range "2.0.0" "2.1.0");
"0.9.2" = cmc (range "8.14" "8.18") (range "1.13.0" "1.18.0");
"0.9.1" = cmc (range "8.14" "8.16") (range "1.13.0" "1.14.0");
"0.9" = cmc (range "8.12" "8.13") (range "1.12.0" "1.14.0");
}
)) null;
with lib.versions;
lib.switch
[ coq.coq-version mathcomp.version ]
[
(case (range "8.18" "9.0") (range "2.0.0" "2.4.0") "0.9.6")
(case (range "8.16" "8.19") (range "2.0.0" "2.3.0") "0.9.4")
(case (range "8.16" "8.18") (range "2.0.0" "2.1.0") "0.9.3")
(case (range "8.14" "8.18") (range "1.13.0" "1.18.0") "0.9.2")
(case (range "8.14" "8.16") (range "1.13.0" "1.14.0") "0.9.1")
(case (range "8.12" "8.13") (range "1.12.0" "1.14.0") "0.9")
]
null;
propagatedBuildInputs = [
mathcomp.algebra

27
pkgs/development/coq-modules/hierarchy-builder/default.nix
View File

@ -14,20 +14,21 @@ let
owner = "math-comp";
inherit version;
defaultVersion =
let
case = case: out: { inherit case out; };
in
with lib.versions;
lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: case: { inherit case out; }) {
"1.9.1" = range "8.20" "9.0";
"1.8.0" = range "8.19" "8.20";
"1.7.1" = range "8.18" "8.20";
"1.6.0" = range "8.16" "8.18";
"1.5.0" = range "8.15" "8.18";
"1.4.0" = range "8.15" "8.17";
"1.2.0" = range "8.13" "8.14";
"1.1.0" = range "8.12" "8.13";
"0.10.0" = isEq "8.11";
}
)) null;
lib.switch coq.coq-version [
(case (range "8.20" "9.0") "1.9.1")
(case (range "8.19" "8.20") "1.8.0")
(case (range "8.18" "8.20") "1.7.1")
(case (range "8.16" "8.18") "1.6.0")
(case (range "8.15" "8.18") "1.5.0")
(case (range "8.15" "8.17") "1.4.0")
(case (range "8.13" "8.14") "1.2.0")
(case (range "8.12" "8.13") "1.1.0")
(case (isEq "8.11") "0.10.0")
] null;
release."1.9.1".sha256 = "sha256-AiS0ezMyfIYlXnuNsVLz1GlKQZzJX+ilkrKkbo0GrF0=";
release."1.8.1".sha256 = "sha256-Z0WAHDyycqgL+Le/zNfEAoLWzFb7WIL+3G3vEBExlb4=";
release."1.8.0".sha256 = "sha256-4s/4ZZKj5tiTtSHGIM8Op/Pak4Vp52WVOpd4l9m19fY=";

11
pkgs/development/coq-modules/http/default.nix
View File

@ -15,13 +15,12 @@ mkCoqDerivation {
defaultVersion =
let
inherit (lib.versions) isLe range;
case = case: out: { inherit case out; };
inherit (lib.versions) range;
in
lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: case: { inherit case out; }) {
"0.2.1" = range "8.14" "8.19";
}
)) null;
lib.switch coq.coq-version [
(case (range "8.14" "8.19") "0.2.1")
] null;
release = {
"0.2.1".sha256 = "sha256-CIcaXEojNdajXNoMBjGlQRc1sOJSKgUlditNxbNSPgk=";
};

13
pkgs/development/coq-modules/hydra-battles/default.nix
View File

@ -19,13 +19,14 @@
inherit version;
defaultVersion =
let
case = case: out: { inherit case out; };
in
with lib.versions;
lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: case: { inherit case out; }) {
"0.9" = range "8.13" "8.16";
"0.4" = range "8.11" "8.12";
}
)) null;
lib.switch coq.coq-version [
(case (range "8.13" "8.16") "0.9")
(case (range "8.11" "8.12") "0.4")
] null;
useDune = true;

29
pkgs/development/coq-modules/interval/default.nix
View File

@ -18,21 +18,22 @@ mkCoqDerivation rec {
domain = "gitlab.inria.fr";
inherit version;
defaultVersion =
let
case = case: out: { inherit case out; };
in
with lib.versions;
lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: case: { inherit case out; }) {
"4.11.2" = range "8.13" "9.0";
"4.11.1" = range "8.13" "8.20";
"4.10.0" = range "8.12" "8.19";
"4.9.0" = range "8.12" "8.18";
"4.8.0" = range "8.12" "8.17";
"4.6.0" = range "8.12" "8.16";
"4.5.2" = range "8.8" "8.16";
"4.0.0" = range "8.8" "8.12";
"3.4.2" = range "8.7" "8.11";
"3.3.0" = range "8.5" "8.6";
}
)) null;
lib.switch coq.coq-version [
(case (range "8.13" "9.0") "4.11.2")
(case (range "8.13" "8.20") "4.11.1")
(case (range "8.12" "8.19") "4.10.0")
(case (range "8.12" "8.18") "4.9.0")
(case (range "8.12" "8.17") "4.8.0")
(case (range "8.12" "8.16") "4.6.0")
(case (range "8.8" "8.16") "4.5.2")
(case (range "8.8" "8.12") "4.0.0")
(case (range "8.7" "8.11") "3.4.2")
(case (range "8.5" "8.6") "3.3.0")
] null;
release."4.11.2".sha256 = "sha256-ouhjHtlxcqt06+Pt+UZAzwp83bVYPh3N+8jnsVvapSU=";
release."4.11.1".sha256 = "sha256-QWZvU468rOhK796xCCEawW6rhCRTPnE0iLll9ynKflo=";
release."4.11.0".sha256 = "sha256-vPwa4zSjyvxHLGDoNaBnHV2pb77dnQFbC50BL80fcvE=";

23
pkgs/development/coq-modules/iris/default.nix
View File

@ -12,18 +12,19 @@ mkCoqDerivation {
owner = "iris";
inherit version;
defaultVersion =
let
case = case: out: { inherit case out; };
in
with lib.versions;
lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: case: { inherit case out; }) {
"4.3.0" = range "8.19" "9.0";
"4.2.0" = range "8.18" "8.19";
"4.1.0" = range "8.16" "8.18";
"4.0.0" = range "8.13" "8.17";
"3.5.0" = range "8.12" "8.14";
"3.4.0" = range "8.11" "8.13";
"3.3.0" = range "8.9" "8.10";
}
)) null;
lib.switch coq.coq-version [
(case (range "8.19" "9.0") "4.3.0")
(case (range "8.18" "8.19") "4.2.0")
(case (range "8.16" "8.18") "4.1.0")
(case (range "8.13" "8.17") "4.0.0")
(case (range "8.12" "8.14") "3.5.0")
(case (range "8.11" "8.13") "3.4.0")
(case (range "8.9" "8.10") "3.3.0")
] null;
release."4.3.0".sha256 = "sha256-3qhjiFI+A3I3fD8rFfJL5Hek77wScfn/FNNbDyGqA1k=";
release."4.2.0".sha256 = "sha256-HuiHIe+5letgr1NN1biZZFq0qlWUbFmoVI7Q91+UIfM=";
release."4.1.0".sha256 = "sha256-nTZUeZOXiH7HsfGbMKDE7vGrNVCkbMaWxdMWUcTUNlo=";

25
pkgs/development/coq-modules/itauto/default.nix
View File

@ -22,19 +22,20 @@
release."8.13+no".sha256 = "sha256-gXoxtLcHPoyjJkt7WqvzfCMCQlh6kL2KtCGe3N6RC/A=";
inherit version;
defaultVersion =
let
case = case: out: { inherit case out; };
in
with lib.versions;
lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: case: { inherit case out; }) {
"8.20.0" = isEq "8.20";
"8.19.0" = isEq "8.19";
"8.18.0" = isEq "8.18";
"8.17.0" = isEq "8.17";
"8.16.0" = isEq "8.16";
"8.15.0" = isEq "8.15";
"8.14.0" = isEq "8.14";
"8.13+no" = isEq "8.13";
}
)) null;
lib.switch coq.coq-version [
(case (isEq "8.20") "8.20.0")
(case (isEq "8.19") "8.19.0")
(case (isEq "8.18") "8.18.0")
(case (isEq "8.17") "8.17.0")
(case (isEq "8.16") "8.16.0")
(case (isEq "8.15") "8.15.0")
(case (isEq "8.14") "8.14.0")
(case (isEq "8.13") "8.13+no")
] null;
mlPlugin = true;
nativeBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]);

11
pkgs/development/coq-modules/itree-io/default.nix
View File

@ -15,13 +15,12 @@ mkCoqDerivation {
defaultVersion =
let
inherit (lib.versions) isLe range;
case = case: out: { inherit case out; };
inherit (lib.versions) range;
in
lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: case: { inherit case out; }) {
"0.1.1" = range "8.12" "8.19";
}
)) null;
lib.switch coq.coq-version [
(case (range "8.12" "8.19") "0.1.1")
] null;
release = {
"0.1.1".sha256 = "sha256-IFwIj8dxW4jm2gvuUJ8LKZFSJeljp0bsn8fezxY6t2o=";
};

26
pkgs/development/coq-modules/jasmin/default.nix
View File

@ -14,19 +14,23 @@ mkCoqDerivation {
inherit version;
defaultVersion =
with lib.versions;
let
cmc = c: mc: [
c
mc
];
case = coq: mc: out: {
case = [
coq
mc
];
inherit out;
};
in
lib.switch [ coq.coq-version mathcomp.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: cases: { inherit cases out; }) {
"2025.02.0" = cmc (range "8.19" "9.0") (range "2.2" "2.4");
"2024.07.2" = cmc (isEq "8.18") (isEq "2.2");
}
)) null;
with lib.versions;
lib.switch
[ coq.coq-version mathcomp.version ]
[
(case (range "8.19" "9.0") (range "2.2" "2.4") "2025.02.0")
(case (isEq "8.18") (isEq "2.2") "2024.07.2")
]
null;
releaseRev = v: "v${v}";
release."2025.02.0".sha256 = "sha256-Jlf0+VPuYWXdWyKHKHSp7h/HuCCp4VkcrgDAmh7pi5s=";

13
pkgs/development/coq-modules/json/default.nix
View File

@ -15,14 +15,13 @@
defaultVersion =
let
inherit (lib.versions) isLe range;
case = case: out: { inherit case out; };
inherit (lib.versions) range;
in
lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: case: { inherit case out; }) {
"0.2.0" = range "8.14" "9.0";
"0.1.3" = range "8.14" "8.20";
}
)) null;
lib.switch coq.coq-version [
(case (range "8.14" "9.0") "0.2.0")
(case (range "8.14" "8.20") "0.1.3")
] null;
release = {
"0.2.0".sha256 = "sha256-qDRTgWLUvu4x3/d3BDcqo2I4W5ZmLyRiwuY/Tm/FuKA=";
"0.1.3".sha256 = "sha256-lElAzW4IuX+BB6ngDjlyKn0MytLRfbhQanB+Lct/WR0=";

28
pkgs/development/coq-modules/mathcomp-abel/default.nix
View File

@ -18,20 +18,24 @@ mkCoqDerivation {
inherit version;
defaultVersion =
with lib.versions;
let
cmc = c: mc: [
c
mc
];
case = coq: mc: out: {
case = [
coq
mc
];
inherit out;
};
in
lib.switch [ coq.coq-version mathcomp.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: cases: { inherit cases out; }) {
"1.2.1" = cmc (range "8.10" "8.16") (range "1.12.0" "1.15.0");
"1.2.0" = cmc (range "8.10" "8.15") (range "1.12.0" "1.14.0");
"1.1.2" = cmc (range "8.10" "8.14") (range "1.11.0" "1.12.0");
}
)) null;
with lib.versions;
lib.switch
[ coq.coq-version mathcomp.version ]
[
(case (range "8.10" "8.16") (range "1.12.0" "1.15.0") "1.2.1")
(case (range "8.10" "8.15") (range "1.12.0" "1.14.0") "1.2.0")
(case (range "8.10" "8.14") (range "1.11.0" "1.12.0") "1.1.2")
]
null;
release."1.2.1".sha256 = "sha256-M1q6WIPBsayHde2hwlTxylH169hcTs3OuFsEkM0e3yc=";
release."1.2.0".sha256 = "1picd4m85ipj22j3b84cv8ab3330radzrhd6kp0gpxq14dhv02c2";

32
pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix
View File

@ -19,22 +19,26 @@ mkCoqDerivation {
inherit version;
defaultVersion =
with lib.versions;
let
cmc = c: mc: [
c
mc
];
case = coq: mc: out: {
case = [
coq
mc
];
inherit out;
};
in
lib.switch [ coq.coq-version mathcomp-algebra.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: cases: { inherit cases out; }) {
"1.2.5" = cmc (range "8.20" "9.0") (isGe "2.4");
"1.2.4" = cmc (range "8.16" "9.0") (isGe "2.0");
"1.2.2" = cmc (range "8.16" "8.18") (isGe "2.0");
"1.1.1" = cmc (range "8.16" "8.19") (isGe "1.15");
"1.0.0" = cmc (range "8.13" "8.16") (isGe "1.12");
}
)) null;
with lib.versions;
lib.switch
[ coq.coq-version mathcomp-algebra.version ]
[
(case (range "8.20" "9.0") (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")
]
null;
release."1.0.0".sha256 = "sha256-kszARPBizWbxSQ/Iqpf2vLbxYc6AjpUCLnSNlPcNfls=";
release."1.1.1".sha256 = "sha256-5wItMeeTRoJlRBH3zBNc2VUZn6pkDde60YAvXTx+J3U=";

52
pkgs/development/coq-modules/mathcomp-analysis/default.nix
View File

@ -44,32 +44,36 @@ let
release."0.2.3".sha256 = "0p9mr8g1qma6h10qf7014dv98ln90dfkwn76ynagpww7qap8s966";
defaultVersion =
with lib.versions;
let
cmc = c: mc: [
c
mc
];
case = coq: mc: out: {
case = [
coq
mc
];
inherit out;
};
in
lib.switch [ coq.coq-version mathcomp.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: cases: { inherit cases out; }) {
"1.11.0" = cmc (range "8.20" "9.0") (range "2.1.0" "2.4.0");
"1.9.0" = cmc (range "8.19" "8.20") (range "2.1.0" "2.3.0");
"1.1.0" = cmc (range "8.17" "8.20") (range "2.0.0" "2.2.0");
"0.7.0" = cmc (range "8.17" "8.19") (range "1.17.0" "1.19.0");
"0.6.7" = cmc (range "8.17" "8.18") (range "1.15.0" "1.18.0");
"0.6.6" = cmc (range "8.17" "8.18") (range "1.15.0" "1.18.0");
"0.6.5" = cmc (range "8.14" "8.18") (range "1.15.0" "1.17.0");
"0.6.1" = cmc (range "8.14" "8.18") (range "1.13.0" "1.16.0");
"0.5.2" = cmc (range "8.14" "8.18") (range "1.13" "1.15");
"0.5.1" = cmc (range "8.13" "8.15") (range "1.13" "1.14");
"0.3.13" = cmc (range "8.13" "8.15") (range "1.12" "1.14");
"0.3.10" = cmc (range "8.11" "8.14") (range "1.12" "1.13");
"0.3.3" = cmc (range "8.10" "8.12") "1.11.0";
"0.3.1" = cmc (range "8.10" "8.11") "1.11.0";
"0.2.3" = cmc (range "8.8" "8.11") (range "1.8" "1.10");
}
)) null;
with lib.versions;
lib.switch
[ coq.coq-version mathcomp.version ]
[
(case (range "8.20" "9.0") (range "2.1.0" "2.4.0") "1.11.0")
(case (range "8.19" "8.20") (range "2.1.0" "2.3.0") "1.9.0")
(case (range "8.17" "8.20") (range "2.0.0" "2.2.0") "1.1.0")
(case (range "8.17" "8.19") (range "1.17.0" "1.19.0") "0.7.0")
(case (range "8.17" "8.18") (range "1.15.0" "1.18.0") "0.6.7")
(case (range "8.17" "8.18") (range "1.15.0" "1.18.0") "0.6.6")
(case (range "8.14" "8.18") (range "1.15.0" "1.17.0") "0.6.5")
(case (range "8.14" "8.18") (range "1.13.0" "1.16.0") "0.6.1")
(case (range "8.14" "8.18") (range "1.13" "1.15") "0.5.2")
(case (range "8.13" "8.15") (range "1.13" "1.14") "0.5.1")
(case (range "8.13" "8.15") (range "1.12" "1.14") "0.3.13")
(case (range "8.11" "8.14") (range "1.12" "1.13") "0.3.10")
(case (range "8.10" "8.12") "1.11.0" "0.3.3")
(case (range "8.10" "8.11") "1.11.0" "0.3.1")
(case (range "8.8" "8.11") (range "1.8" "1.10") "0.2.3")
]
null;
# list of analysis packages sorted by dependency order
packages = {

24
pkgs/development/coq-modules/mathcomp-apery/default.nix
View File

@ -17,18 +17,22 @@ mkCoqDerivation {
inherit version;
defaultVersion =
with lib.versions;
let
cmc = c: mc: [
c
mc
];
case = coq: mc: out: {
case = [
coq
mc
];
inherit out;
};
in
lib.switch [ coq.coq-version mathcomp.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: cases: { inherit cases out; }) {
"1.0.2" = cmc (range "8.13" "8.16") (range "1.12.0" "1.17.0");
}
)) null;
with lib.versions;
lib.switch
[ coq.coq-version mathcomp.version ]
[
(case (range "8.13" "8.16") (range "1.12.0" "1.17.0") "1.0.2")
]
null;
release."1.0.2".sha256 = "sha256-llxyMKYvWUA7fyroG1S/jtpioAoArmarR1edi3cikcY=";

13
pkgs/development/coq-modules/mathcomp-bigenough/default.nix
View File

@ -22,13 +22,14 @@ mkCoqDerivation {
};
inherit version;
defaultVersion =
let
case = case: out: { inherit case out; };
in
with lib.versions;
lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: case: { inherit case out; }) {
"1.0.2" = range "8.10" "9.0";
"1.0.0" = range "8.5" "8.14";
}
)) null;
lib.switch coq.coq-version [
(case (range "8.10" "9.0") "1.0.2")
(case (range "8.5" "8.14") "1.0.0")
] null;
propagatedBuildInputs = [ mathcomp-boot ];

44
pkgs/development/coq-modules/mathcomp-finmap/default.nix
View File

@ -16,28 +16,32 @@ mkCoqDerivation {
owner = "math-comp";
inherit version;
defaultVersion =
with lib.versions;
let
cmc = c: mc: [
c
mc
];
case = coq: mc: out: {
case = [
coq
mc
];
inherit out;
};
in
lib.switch [ coq.coq-version mathcomp-boot.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: cases: { inherit cases out; }) {
"2.2.0" = cmc (range "8.20" "9.0") (range "2.3" "2.4");
"2.1.0" = cmc (range "8.16" "9.0") (range "2.0" "2.3");
"2.0.0" = cmc (range "8.16" "8.18") (range "2.0" "2.1");
"1.5.2" = cmc (range "8.13" "8.20") (range "1.12" "1.19");
"1.5.1" = cmc (isGe "8.10") (range "1.11" "1.17");
"1.5.0" = cmc (range "8.7" "8.11") "1.11.0";
"1.4.0+coq-8.11" = cmc (isEq "8.11") (range "1.8" "1.10");
"1.4.0" = cmc (range "8.7" "8.11.0") (range "1.8" "1.10");
"1.3.4" = cmc (range "8.7" "8.11.0") (range "1.8" "1.10");
"1.1.0" = cmc (range "8.7" "8.9") "1.7.0";
"1.0.0" = cmc (range "8.6" "8.7") (range "1.6.1" "1.7");
}
)) null;
with lib.versions;
lib.switch
[ coq.coq-version mathcomp-boot.version ]
[
(case (range "8.20" "9.0") (range "2.3" "2.4") "2.2.0")
(case (range "8.16" "9.0") (range "2.0" "2.3") "2.1.0")
(case (range "8.16" "8.18") (range "2.0" "2.1") "2.0.0")
(case (range "8.13" "8.20") (range "1.12" "1.19") "1.5.2")
(case (isGe "8.10") (range "1.11" "1.17") "1.5.1")
(case (range "8.7" "8.11") "1.11.0" "1.5.0")
(case (isEq "8.11") (range "1.8" "1.10") "1.4.0+coq-8.11")
(case (range "8.7" "8.11.0") (range "1.8" "1.10") "1.4.0")
(case (range "8.7" "8.11.0") (range "1.8" "1.10") "1.3.4")
(case (range "8.7" "8.9") "1.7.0" "1.1.0")
(case (range "8.6" "8.7") (range "1.6.1" "1.7") "1.0.0")
]
null;
release = {
"2.2.0".sha256 = "sha256-oDQEZOutrJxmN8FvzovUIhqw0mwc8Ej7thrieJrW8BY=";
"2.1.0".sha256 = "sha256-gh0cnhdVDyo+D5zdtxLc10kGKQLQ3ITzHnMC45mCtpY=";

42
pkgs/development/coq-modules/mathcomp-infotheo/default.nix
View File

@ -19,27 +19,31 @@
inherit version;
defaultVersion =
with lib.versions;
let
cmc = c: mc: [
c
mc
];
case = coq: mc: out: {
case = [
coq
mc
];
inherit out;
};
in
lib.switch [ coq.coq-version mathcomp-analysis.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: cases: { inherit cases out; }) {
"0.9.3" = cmc (range "8.20" "8.20") (isGe "1.10");
"0.9.1" = cmc (range "8.19" "8.20") (isGe "1.9");
"0.7.7" = cmc (range "8.19" "8.20") (isGe "1.7");
"0.7.5" = cmc (range "8.19" "8.20") (isGe "1.7");
"0.7.3" = cmc (range "8.18" "8.20") (isGe "1.5");
"0.7.2" = cmc (range "8.18" "8.19") (isGe "1.2");
"0.7.1" = cmc (range "8.17" "8.19") (isGe "1.0");
"0.6.1" = cmc (isGe "8.17") (range "0.6.6" "0.7.0");
"0.5.2" = cmc (range "8.17" "8.18") (range "0.6.0" "0.6.7");
"0.5.1" = cmc (range "8.15" "8.16") (range "0.5.4" "0.6.5");
}
)) null;
with lib.versions;
lib.switch
[ coq.coq-version mathcomp-analysis.version ]
[
(case (range "8.20" "8.20") (isGe "1.10") "0.9.3")
(case (range "8.19" "8.20") (isGe "1.9") "0.9.1")
(case (range "8.19" "8.20") (isGe "1.7") "0.7.7")
(case (range "8.19" "8.20") (isGe "1.7") "0.7.5")
(case (range "8.18" "8.20") (isGe "1.5") "0.7.3")
(case (range "8.18" "8.19") (isGe "1.2") "0.7.2")
(case (range "8.17" "8.19") (isGe "1.0") "0.7.1")
(case (isGe "8.17") (range "0.6.6" "0.7.0") "0.6.1")
(case (range "8.17" "8.18") (range "0.6.0" "0.6.7") "0.5.2")
(case (range "8.15" "8.16") (range "0.5.4" "0.6.5") "0.5.1")
]
null;
release."0.9.3".sha256 = "sha256-8+cnVKNAvZ3MVV3BpS8UmCIxJphsQRBv3swek1eEBjE=";
release."0.9.1".sha256 = "sha256-WI20HxMHr1ZUwOGPIUl+nRI8TxVUa2+F1xcGjRDHO9g=";
release."0.7.7".sha256 = "sha256-kEbpMl7U+I2kvqi1VrjhIVFkZFO6h0tTHEUZRbHYG7E=";

30
pkgs/development/coq-modules/mathcomp-tarjan/default.nix
View File

@ -18,21 +18,25 @@ mkCoqDerivation {
inherit version;
defaultVersion =
with lib.versions;
let
cmc = c: mc: [
c
mc
];
case = coq: mc: out: {
case = [
coq
mc
];
inherit out;
};
in
lib.switch [ coq.coq-version mathcomp-ssreflect.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: cases: { inherit cases out; }) {
"1.0.3" = cmc (range "8.16" "9.0") (range "2.0.0" "2.4.0");
"1.0.2" = cmc (range "8.16" "9.0") (range "2.0.0" "2.3.0");
"1.0.1" = cmc (range "8.12" "8.18") (range "1.12.0" "1.17.0");
"1.0.0" = cmc (range "8.10" "8.16") (range "1.12.0" "1.17.0");
}
)) null;
with lib.versions;
lib.switch
[ coq.coq-version mathcomp-ssreflect.version ]
[
(case (range "8.16" "9.0") (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")
(case (range "8.12" "8.18") (range "1.12.0" "1.17.0") "1.0.1")
(case (range "8.10" "8.16") (range "1.12.0" "1.17.0") "1.0.0")
]
null;
release."1.0.3".sha256 = "sha256-5lpOCDyH6NFzGLvnXHHAnR7Qv5oXsUyC8TLBFrIiBag=";
release."1.0.2".sha256 = "sha256-U20xgA+e9KTRdvILD1cxN6ia+dlA8uBTIbc4QlKz9ss=";
release."1.0.1".sha256 = "sha256-utNjFCAqC5xOuhdyKhfMZkRYJD0xv9Gt6U3ZdQ56mek=";

26
pkgs/development/coq-modules/mathcomp-word/default.nix
View File

@ -56,19 +56,23 @@ mkCoqDerivation {
inherit version;
defaultVersion =
with lib.versions;
let
cmc = c: mc: [
c
mc
];
case = coq: mc: out: {
case = [
coq
mc
];
inherit out;
};
in
lib.switch [ coq.coq-version mathcomp.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: cases: { inherit cases out; }) {
"3.2" = cmc (range "8.16" "9.0") (isGe "2.0");
"2.4" = cmc (range "8.12" "8.20") (range "1.12" "1.19");
}
)) null;
with lib.versions;
lib.switch
[ coq.coq-version mathcomp.version ]
[
(case (range "8.16" "9.0") (isGe "2.0") "3.2")
(case (range "8.12" "8.20") (range "1.12" "1.19") "2.4")
]
null;
propagatedBuildInputs = [
mathcomp.algebra

28
pkgs/development/coq-modules/mathcomp-zify/default.nix
View File

@ -20,20 +20,24 @@ mkCoqDerivation {
inherit version;
defaultVersion =
with lib.versions;
let
cmc = c: mc: [
c
mc
];
case = coq: mc: out: {
case = [
coq
mc
];
inherit out;
};
in
lib.switch [ coq.coq-version mathcomp-algebra.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: cases: { inherit cases out; }) {
"1.5.0+2.0+8.16" = cmc (range "8.16" "9.0") (isGe "2.0.0");
"1.3.0+1.12+8.13" = cmc (range "8.13" "8.20") (range "1.12" "1.19.0");
"1.1.0+1.12+8.13" = cmc (range "8.13" "8.16") (range "1.12" "1.17.0");
}
)) null;
with lib.versions;
lib.switch
[ coq.coq-version mathcomp-algebra.version ]
[
(case (range "8.16" "9.0") (isGe "2.0.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")
]
null;
release."1.0.0+1.12+8.13".sha256 = "1j533vx6lacr89bj1bf15l1a0s7rvrx4l00wyjv99aczkfbz6h6k";
release."1.1.0+1.12+8.13".sha256 = "1plf4v6q5j7wvmd5gsqlpiy0vwlw6hy5daq2x42gqny23w9mi2pr";

47
pkgs/development/coq-modules/mathcomp/default.nix
View File

@ -31,31 +31,30 @@ let
withDoc = single && (args.withDoc or false);
defaultVersion =
let
inherit (lib.versions) isLe range;
case = case: out: { inherit case out; };
inherit (lib.versions) range;
in
lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: case: { inherit case out; }) {
"2.4.0" = range "8.20" "9.0";
"2.3.0" = range "8.19" "9.0";
"2.2.0" = range "8.17" "8.20";
"2.1.0" = range "8.17" "8.18";
"2.0.0" = range "8.17" "8.18";
"1.19.0" = range "8.19" "8.20";
"1.18.0" = range "8.17" "8.18";
"1.17.0" = range "8.15" "8.18";
"1.16.0" = range "8.13" "8.18";
"1.15.0" = range "8.14" "8.16";
"1.14.0" = range "8.11" "8.15";
"1.13.0" = range "8.11" "8.15";
"1.12.0" = range "8.10" "8.13";
"1.11.0" = range "8.7" "8.12";
"1.10.0" = range "8.7" "8.11";
"1.9.0" = range "8.7" "8.11";
"1.8.0" = range "8.7" "8.9";
"1.7.0" = range "8.6" "8.9";
"1.6.4" = range "8.5" "8.7";
}
)) null;
lib.switch coq.coq-version [
(case (range "8.20" "9.0") "2.4.0")
(case (range "8.19" "9.0") "2.3.0")
(case (range "8.17" "8.20") "2.2.0")
(case (range "8.17" "8.18") "2.1.0")
(case (range "8.17" "8.18") "2.0.0")
(case (range "8.19" "8.20") "1.19.0")
(case (range "8.17" "8.18") "1.18.0")
(case (range "8.15" "8.18") "1.17.0")
(case (range "8.13" "8.18") "1.16.0")
(case (range "8.14" "8.16") "1.15.0")
(case (range "8.11" "8.15") "1.14.0")
(case (range "8.11" "8.15") "1.13.0")
(case (range "8.10" "8.13") "1.12.0")
(case (range "8.7" "8.12") "1.11.0")
(case (range "8.7" "8.11") "1.10.0")
(case (range "8.7" "8.11") "1.9.0")
(case (range "8.7" "8.9") "1.8.0")
(case (range "8.6" "8.9") "1.7.0")
(case (range "8.5" "8.7") "1.6.4")
] null;
release = {
"2.4.0".sha256 = "sha256-A1XgLLwZRvKS8QyceCkSQa7ue6TYyf5fMft5gSx9NOs=";
"2.3.0".sha256 = "sha256-wa6OBig8rhAT4iwupSylyCAMhO69rADa0MQIX5zzL+Q=";

32
pkgs/development/coq-modules/metacoq/default.nix
View File

@ -10,22 +10,24 @@
let
repo = "metacoq";
owner = "MetaCoq";
defaultVersion = lib.switch coq.coq-version (lib.lists.sort (x: y: lib.versions.isLe x.out y.out) (
lib.mapAttrsToList (out: case: { inherit case out; }) {
"1.0-beta2-8.11" = "8.11";
"1.0-beta2-8.12" = "8.12";
defaultVersion =
let
case = case: out: { inherit case out; };
in
lib.switch coq.coq-version [
(case "8.11" "1.0-beta2-8.11")
(case "8.12" "1.0-beta2-8.12")
# Do not provide 8.13 because it does not compile with equations 1.3 provided by default (only 1.2.3)
# "1.0-beta2-8.13" = "8.13";
"1.1-8.14" = "8.14";
"1.1-8.15" = "8.15";
"1.1-8.16" = "8.16";
"1.3.1-8.17" = "8.17";
"1.3.1-8.18" = "8.18";
"1.3.3-8.19" = "8.19";
"1.3.4-8.20" = "8.20";
"1.3.4-9.0" = "9.0";
}
)) null;
# (case "8.13" "1.0-beta2-8.13")
(case "8.14" "1.1-8.14")
(case "8.15" "1.1-8.15")
(case "8.16" "1.1-8.16")
(case "8.17" "1.3.1-8.17")
(case "8.18" "1.3.1-8.18")
(case "8.19" "1.3.3-8.19")
(case "8.20" "1.3.4-8.20")
(case "9.0" "1.3.4-9.0")
] null;
release = {
"1.0-beta2-8.11".sha256 = "sha256-I9YNk5Di6Udvq5/xpLSNflfjRyRH8fMnRzbo3uhpXNs=";
"1.0-beta2-8.12".sha256 = "sha256-I8gpmU9rUQJh0qfp5KOgDNscVvCybm5zX4TINxO1TVA=";

12
pkgs/development/coq-modules/metarocq/default.nix
View File

@ -10,11 +10,13 @@
let
repo = "metarocq";
owner = "MetaRocq";
defaultVersion = lib.switch coq.coq-version (lib.lists.sort (x: y: lib.versions.isLe x.out y.out) (
lib.mapAttrsToList (out: case: { inherit case out; }) {
"1.4-9.0" = "9.0";
}
)) null;
defaultVersion =
let
case = case: out: { inherit case out; };
in
lib.switch coq.coq-version [
(case ("9.0") "1.4-9.0")
] null;
release = {
"1.4-9.0".sha256 = "sha256-5QecDAMkvgfDPZ7/jDfnOgcE+Eb1LTAozP7nz6nkuxg=";
};

48
pkgs/development/coq-modules/multinomials/default.nix
View File

@ -20,30 +20,34 @@ mkCoqDerivation {
inherit version;
defaultVersion =
with lib.versions;
let
cmc = c: mc: [
c
mc
];
case = coq: mc: out: {
case = [
coq
mc
];
inherit out;
};
in
lib.switch [ coq.coq-version mathcomp.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: cases: { inherit cases out; }) {
"2.4.0" = cmc (range "8.18" "9.0") (range "2.1.0" "2.4.0");
"2.3.0" = cmc (range "8.17" "9.0") (range "2.1.0" "2.3.0");
"2.2.0" = cmc (range "8.17" "8.20") (isGe "2.1.0");
"2.1.0" = cmc (range "8.16" "8.18") "2.1.0";
"2.0.0" = cmc (range "8.16" "8.18") "2.0.0";
"1.6.0" = cmc (isGe "8.15") (range "1.15.0" "1.19.0");
"1.5.6" = cmc (isGe "8.10") (range "1.13.0" "1.17.0");
"1.5.5" = cmc (range "8.10" "8.16") (range "1.12.0" "1.15.0");
"1.5.3" = cmc (range "8.10" "8.12") "1.12.0";
"1.5.2" = cmc (range "8.7" "8.12") "1.11.0";
"1.5.0" = cmc (range "8.7" "8.11") (range "1.8" "1.10");
"1.4" = cmc (range "8.7" "8.10") (range "1.8" "1.10");
"1.1" = cmc "8.6" (range "1.6" "1.7");
}
)) null;
with lib.versions;
lib.switch
[ coq.coq-version mathcomp.version ]
[
(case (range "8.18" "9.0") (range "2.1.0" "2.4.0") "2.4.0")
(case (range "8.17" "9.0") (range "2.1.0" "2.3.0") "2.3.0")
(case (range "8.17" "8.20") (isGe "2.1.0") "2.2.0")
(case (range "8.16" "8.18") "2.1.0" "2.1.0")
(case (range "8.16" "8.18") "2.0.0" "2.0.0")
(case (isGe "8.15") (range "1.15.0" "1.19.0") "1.6.0")
(case (isGe "8.10") (range "1.13.0" "1.17.0") "1.5.6")
(case (range "8.10" "8.16") (range "1.12.0" "1.15.0") "1.5.5")
(case (range "8.10" "8.12") "1.12.0" "1.5.3")
(case (range "8.7" "8.12") "1.11.0" "1.5.2")
(case (range "8.7" "8.11") (range "1.8" "1.10") "1.5.0")
(case (range "8.7" "8.10") (range "1.8" "1.10") "1.4")
(case "8.6" (range "1.6" "1.7") "1.1")
]
null;
release = {
"2.4.0".sha256 = "sha256-7zfIddRH+Sl4nhEPtS/lMZwRUZI45AVFpcC/UC8Z0Yo=";
"2.3.0".sha256 = "sha256-usIcxHOAuN+f/j3WjVbPrjz8Hl9ac8R6kYeAKi3CEts=";

19
pkgs/development/coq-modules/odd-order/default.nix
View File

@ -18,16 +18,17 @@ mkCoqDerivation {
inherit version;
defaultVersion =
let
case = case: out: { inherit case out; };
in
with lib.versions;
lib.switch mathcomp.character.version (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: case: { inherit case out; }) {
"2.2.0" = (range "2.2.0" "2.4.0");
"2.1.0" = (range "2.1.0" "2.3.0");
"1.14.0" = (range "1.13.0" "1.15.0");
"1.13.0" = (range "1.12.0" "1.14.0");
"1.12.0" = (range "1.10.0" "1.12.0");
}
)) null;
lib.switch mathcomp.character.version [
(case ((range "2.2.0" "2.4.0")) "2.2.0")
(case ((range "2.1.0" "2.3.0")) "2.1.0")
(case ((range "1.13.0" "1.15.0")) "1.14.0")
(case ((range "1.12.0" "1.14.0")) "1.13.0")
(case ((range "1.10.0" "1.12.0")) "1.12.0")
] null;
propagatedBuildInputs = [
mathcomp.character

30
pkgs/development/coq-modules/reglang/default.nix
View File

@ -20,21 +20,25 @@ mkCoqDerivation {
inherit version;
defaultVersion =
with lib.versions;
let
cmc = c: mc: [
c
mc
];
case = coq: mc: out: {
case = [
coq
mc
];
inherit out;
};
in
lib.switch [ coq.coq-version mathcomp.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: cases: { inherit cases out; }) {
"1.2.2" = cmc (range "8.16" "9.0") (range "2.0.0" "2.4.0");
"1.2.1" = cmc (range "8.16" "9.0") (range "2.0.0" "2.3.0");
"1.2.0" = cmc (range "8.16" "8.18") (range "2.0.0" "2.1.0");
"1.1.3" = cmc (range "8.10" "8.20") (isLt "2.0.0");
}
)) null;
with lib.versions;
lib.switch
[ coq.coq-version mathcomp.version ]
[
(case (range "8.16" "9.0") (range "2.0.0" "2.4.0") "1.2.2")
(case (range "8.16" "9.0") (range "2.0.0" "2.3.0") "1.2.1")
(case (range "8.16" "8.18") (range "2.0.0" "2.1.0") "1.2.0")
(case (range "8.10" "8.20") (isLt "2.0.0") "1.1.3")
]
null;
propagatedBuildInputs = [
mathcomp.ssreflect

31
pkgs/development/coq-modules/relation-algebra/default.nix
View File

@ -27,22 +27,23 @@ mkCoqDerivation {
inherit version;
defaultVersion =
let
case = case: out: { inherit case out; };
in
with lib.versions;
lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: case: { inherit case out; }) {
"1.7.11" = isEq "8.20";
"1.7.10" = range "8.18" "8.19";
"1.7.9" = isEq "8.17";
"1.7.8" = isEq "8.16";
"1.7.7" = isEq "8.15";
"1.7.6" = isEq "8.14";
"1.7.5" = isEq "8.13";
"1.7.4" = isEq "8.12";
"1.7.3" = isEq "8.11";
"1.7.2" = isEq "8.10";
"1.7.1" = isEq "8.9";
}
)) null;
lib.switch coq.coq-version [
(case (isEq "8.20") "1.7.11")
(case (range "8.18" "8.19") "1.7.10")
(case (isEq "8.17") "1.7.9")
(case (isEq "8.16") "1.7.8")
(case (isEq "8.15") "1.7.7")
(case (isEq "8.14") "1.7.6")
(case (isEq "8.13") "1.7.5")
(case (isEq "8.12") "1.7.4")
(case (isEq "8.11") "1.7.3")
(case (isEq "8.10") "1.7.2")
(case (isEq "8.9") "1.7.1")
] null;
mlPlugin = true;

15
pkgs/development/coq-modules/simple-io/default.nix
View File

@ -13,14 +13,15 @@
repo = "coq-simple-io";
inherit version;
defaultVersion =
let
case = case: out: { inherit case out; };
in
with lib.versions;
lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: case: { inherit case out; }) {
"1.10.0" = range "8.17" "9.0";
"1.8.0" = range "8.11" "8.19";
"1.3.0" = range "8.7" "8.13";
}
)) null;
lib.switch coq.coq-version [
(case (range "8.17" "9.0") "1.10.0")
(case (range "8.11" "8.19") "1.8.0")
(case (range "8.7" "8.13") "1.3.0")
] null;
release."1.10.0".sha256 = "sha256-67cBhLvRMWLWBL7NXK1zZTQC4PtSKu9qtesU4SqKkOw=";
release."1.8.0".sha256 = "sha256-3ADNeXrBIpYRlfUW+LkLHUWV1w1HFrVc/TZISMuwvRY=";
release."1.7.0".sha256 = "sha256:1a1q9x2abx71hqvjdai3n12jxzd49mhf3nqqh3ya2ssl2lj609ci";

32
pkgs/development/coq-modules/ssprove/default.nix
View File

@ -18,28 +18,32 @@
inherit version;
defaultVersion =
with lib.versions;
let
cmc = c: mc: [
c
mc
];
case = coq: mc: out: {
case = [
coq
mc
];
inherit out;
};
in
lib.switch [ coq.coq-version mathcomp-boot.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: cases: { inherit cases out; }) {
"0.2.4" = cmc (range "8.18" "9.0") (range "2.3.0" "2.4.0");
"0.2.3" = cmc (range "8.18" "8.20") (range "2.3.0" "2.3.0");
"0.2.2" = cmc (range "8.18" "8.20") (range "2.1.0" "2.2.0");
with lib.versions;
lib.switch
[ coq.coq-version mathcomp-boot.version ]
[
(case (range "8.18" "9.0") (range "2.3.0" "2.4.0") "0.2.4")
(case (range "8.18" "8.20") (range "2.3.0" "2.3.0") "0.2.3")
(case (range "8.18" "8.20") (range "2.1.0" "2.2.0") "0.2.2")
# This is the original dependency:
# "0.1.0" = ["8.17" "1.18.0"];
# (case "8.17" "1.18.0" "0.1.0")
# But it is not loadable. The math-comp nixpkgs configuration
# will always only output version 1.18.0 for Coq 8.17.
# Hence, the Coq 8.17 and math-comp 1.17.0 must be explicitly set
# to load it.
# (This version is not on the math-comp CI and hence not checked.)
"0.1.0" = cmc "8.17" "1.17.0";
}
)) null;
(case "8.17" "1.17.0" "0.1.0")
]
null;
releaseRev = v: "v${v}";

11
pkgs/development/coq-modules/stalmarck/default.nix
View File

@ -9,12 +9,13 @@
let
repo = "stalmarck";
defaultVersion =
let
case = case: out: { inherit case out; };
in
with lib.versions;
lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: case: { inherit case out; }) {
"8.20.0" = isEq "8.20";
}
)) null;
lib.switch coq.coq-version [
(case (isEq "8.20") "8.20.0")
] null;
release = {
"8.20.0".sha256 = "sha256-jITxQT1jLyZvWCGPnmK8i3IrwsZwMPOV0aBe9r22TIQ=";
};

13
pkgs/development/coq-modules/stdlib/default.nix
View File

@ -14,13 +14,14 @@
inherit version;
defaultVersion =
let
case = case: out: { inherit case out; };
in
with lib.versions;
lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: case: { inherit case out; }) {
"9.0.0" = isLe "9.0";
# the < 9.0 above is artificial as stdlib was included in Coq before
}
)) null;
lib.switch coq.coq-version [
(case (isLe "9.0") "9.0.0")
# the < 9.0 above is artificial as stdlib was included in Coq before
] null;
releaseRev = v: "V${v}";
release."9.0.0".sha256 = "sha256-2l7ak5Q/NbiNvUzIVXOniEneDXouBMNSSVFbD1Pf8cQ=";

23
pkgs/development/coq-modules/stdpp/default.nix
View File

@ -12,18 +12,19 @@ mkCoqDerivation {
domain = "gitlab.mpi-sws.org";
owner = "iris";
defaultVersion =
let
case = case: out: { inherit case out; };
in
with lib.versions;
lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: case: { inherit case out; }) {
"1.11.0" = range "8.19" "9.0";
"1.10.0" = range "8.18" "8.19";
"1.9.0" = range "8.16" "8.18";
"1.8.0" = range "8.13" "8.17";
"1.6.0" = range "8.12" "8.14";
"1.5.0" = range "8.11" "8.13";
"1.4.0" = range "8.8" "8.10";
}
)) null;
lib.switch coq.coq-version [
(case (range "8.19" "9.0") "1.11.0")
(case (range "8.18" "8.19") "1.10.0")
(case (range "8.16" "8.18") "1.9.0")
(case (range "8.13" "8.17") "1.8.0")
(case (range "8.12" "8.14") "1.6.0")
(case (range "8.11" "8.13") "1.5.0")
(case (range "8.8" "8.10") "1.4.0")
] null;
release."1.11.0".sha256 = "sha256-yqnkaA5gUdZBJZ3JnvPYh11vKQRl0BAnior1yGowG7k=";
release."1.10.0".sha256 = "sha256-bfynevIKxAltvt76lsqVxBmifFkzEhyX8lRgTKxr21I=";
release."1.9.0".sha256 = "sha256-OXeB+XhdyzWMp5Karsz8obp0rTeMKrtG7fu/tmc9aeI=";

11
pkgs/development/rocq-modules/bignums/default.nix
View File

@ -11,12 +11,13 @@ mkRocqDerivation {
owner = "coq";
inherit version;
defaultVersion =
let
case = case: out: { inherit case out; };
in
with lib.versions;
lib.switch rocq-core.rocq-version (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: case: { inherit case out; }) {
"9.0.0+rocq${rocq-core.rocq-version}" = range "9.0" "9.0";
}
)) null;
lib.switch rocq-core.rocq-version [
(case (range "9.0" "9.0") "9.0.0+rocq${rocq-core.rocq-version}")
] null;
release."9.0.0+rocq9.0".sha256 = "sha256-ctnwpyNVhryEUA5YEsAImrcJsNMhtBgDSOz+z5Z4R78=";
releaseRev = v: "${if lib.versions.isGe "9.0" v then "v" else "V"}${v}";

11
pkgs/development/rocq-modules/hierarchy-builder/default.nix
View File

@ -12,12 +12,13 @@ let
owner = "math-comp";
inherit version;
defaultVersion =
let
case = case: out: { inherit case out; };
in
with lib.versions;
lib.switch rocq-core.rocq-version (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: case: { inherit case out; }) {
"1.9.1" = range "9.0" "9.0";
}
)) null;
lib.switch rocq-core.rocq-version [
(case (range "9.0" "9.0") "1.9.1")
] null;
release."1.9.1".sha256 = "sha256-AiS0ezMyfIYlXnuNsVLz1GlKQZzJX+ilkrKkbo0GrF0=";
releaseRev = v: "v${v}";

26
pkgs/development/rocq-modules/rocq-elpi/default.nix
View File

@ -12,11 +12,12 @@ let
if elpi-version != null then
elpi-version
else
(lib.switch rocq-core.rocq-version (lib.lists.sort (x: y: lib.versions.isLe x.out y.out) (
lib.mapAttrsToList (out: case: { inherit case out; }) {
"2.0.7" = "9.0";
}
)) { });
let
case = case: out: { inherit case out; };
in
lib.switch rocq-core.rocq-version [
(case ("9.0") "2.0.7")
] { };
elpi = rocq-core.ocamlPackages.elpi.override { version = default-elpi-version; };
propagatedBuildInputs_wo_elpi = [
rocq-core.ocamlPackages.findlib
@ -27,14 +28,13 @@ let
repo = "coq-elpi";
owner = "LPCIC";
inherit version;
defaultVersion = lib.switch rocq-core.rocq-version (lib.lists.sort
(x: y: lib.versions.isLe x.out y.out)
(
lib.mapAttrsToList (out: case: { inherit case out; }) {
"2.5.2" = "9.0";
}
)
) null;
defaultVersion =
let
case = case: out: { inherit case out; };
in
lib.switch rocq-core.rocq-version [
(case ("9.0") "2.5.2")
] null;
release."2.5.2".sha256 = "sha256-lLzjPrbVB3rrqox528YiheUb0u89R84Xmrgkn0oplOs=";
releaseRev = v: "v${v}";

11
pkgs/development/rocq-modules/stdlib/default.nix
View File

@ -13,12 +13,13 @@ mkRocqDerivation {
inherit version;
defaultVersion =
let
case = case: out: { inherit case out; };
in
with lib.versions;
lib.switch rocq-core.version (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: case: { inherit case out; }) {
"9.0.0" = isEq "9.0";
}
)) null;
lib.switch rocq-core.version [
(case (isEq "9.0") "9.0.0")
] null;
releaseRev = v: "V${v}";
release."9.0.0".sha256 = "sha256-2l7ak5Q/NbiNvUzIVXOniEneDXouBMNSSVFbD1Pf8cQ=";