coqPackages.*: fix formatting

This commit is contained in:
Pierre Roux
2025-06-19 12:29:43 +02:00
committed by Vincent Laporte
parent 46968b2c89
commit 0ddb075c4d
47 changed files with 578 additions and 1615 deletions
@@ -13,20 +13,13 @@
inherit version;
defaultVersion =
with lib.versions;
lib.switch coq.coq-version [
{
case = range "9.0" "9.0";
out = "9.0.0+rocq${coq.coq-version}";
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";
}
{
case = range "8.13" "8.20";
out = "9.0.0+coq${coq.coq-version}";
}
{
case = range "8.6" "8.17";
out = "${coq.coq-version}.0";
}
] null;
)) null;
release."9.0.0+rocq9.0".sha256 = "sha256-ctnwpyNVhryEUA5YEsAImrcJsNMhtBgDSOz+z5Z4R78=";
release."9.0.0+coq8.20".sha256 = "sha256-pkvyDaMXRalc6Uu1eBTuiqTpRauRrzu946c6TavyTKY=";
@@ -14,52 +14,20 @@ let
if elpi-version != null then
elpi-version
else
(lib.switch coq.coq-version [
{
case = "8.11";
out = "1.11.4";
}
{
case = "8.12";
out = "1.12.0";
}
{
case = "8.13";
out = "1.13.7";
}
{
case = "8.14";
out = "1.13.7";
}
{
case = "8.15";
out = "1.15.0";
}
{
case = "8.16";
out = "1.17.0";
}
{
case = "8.17";
out = "1.17.0";
}
{
case = "8.18";
out = "1.18.1";
}
{
case = "8.19";
out = "1.18.1";
}
{
case = "8.20";
out = "2.0.7";
}
{
case = "9.0";
out = "2.0.7";
}
] { });
(
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";
}
)) { }
);
elpi = coq.ocamlPackages.elpi.override { version = default-elpi-version; };
propagatedBuildInputs_wo_elpi = [
coq.ocamlPackages.findlib
@@ -69,52 +37,22 @@ let
repo = "coq-elpi";
owner = "LPCIC";
inherit version;
defaultVersion = lib.switch coq.coq-version [
{
case = "9.0";
out = "2.5.2";
}
{
case = "8.20";
out = "2.5.2";
}
{
case = "8.19";
out = "2.0.1";
}
{
case = "8.18";
out = "2.0.0";
}
{
case = "8.17";
out = "1.18.0";
}
{
case = "8.16";
out = "1.15.6";
}
{
case = "8.15";
out = "1.14.0";
}
{
case = "8.14";
out = "1.11.2";
}
{
case = "8.13";
out = "1.11.1";
}
{
case = "8.12";
out = "1.8.3_8.12";
}
{
case = "8.11";
out = "1.6.3_8.11";
}
] null;
defaultVersion =
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;
release."2.5.2".sha256 = "sha256-lLzjPrbVB3rrqox528YiheUb0u89R84Xmrgkn0oplOs=";
release."2.5.0".sha256 = "sha256-Z5xjO83X/ZoTQlWnVupGXPH3HuJefr57Kv128I0dltg=";
release."2.4.0".sha256 = "sha256-W2+vVGExLLux8e0nSZESSoMVvrLxhL6dmXkb+JuKiqc=";
+20 -75
View File
@@ -18,81 +18,26 @@ let
inherit version;
defaultVersion =
with lib.versions;
lib.switch
[ coq.version mathcomp.version ]
[
{
cases = [
(range "8.20" "9.0")
(isGe "2.3.0")
];
out = "2.1.0";
}
{
cases = [
(range "8.16" "8.20")
(isGe "2.1.0")
];
out = "2.0.3";
}
{
cases = [
(range "8.16" "8.20")
(isGe "2.0.0")
];
out = "2.0.1";
}
{
cases = [
(range "8.16" "8.17")
(isGe "2.0.0")
];
out = "2.0.0";
}
{
cases = [
(range "8.15" "8.18")
(range "1.15.0" "1.18.0")
];
out = "1.1.3";
}
{
cases = [
(range "8.13" "8.17")
(range "1.13.0" "1.18.0")
];
out = "1.1.1";
}
{
cases = [
(range "8.10" "8.15")
(range "1.12.0" "1.18.0")
];
out = "1.1.0";
}
{
cases = [
(isGe "8.10")
(range "1.11.0" "1.12.0")
];
out = "1.0.5";
}
{
cases = [
(isGe "8.7")
"1.11.0"
];
out = "1.0.4";
}
{
cases = [
(isGe "8.7")
"1.10.0"
];
out = "1.0.3";
}
]
null;
let
cmc = c: mc: [
c
mc
];
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;
release."2.1.0".sha256 = "sha256-UoDxy2BKraDyRsO42GXRo26O74OF51biZQGkIMWLf8Y=";
release."2.0.3".sha256 = "sha256-5lDq7IWlEW0EkNzYPu+dA6KOvRgy53W/alikpDr/Kd0=";
@@ -15,36 +15,17 @@ mkCoqDerivation {
inherit version;
defaultVersion =
with lib.versions;
lib.switch coq.coq-version [
{
case = range "8.12" "9.0";
out = "3.4.3";
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";
}
{
case = range "8.12" "8.20";
out = "3.4.2";
}
{
case = range "8.12" "8.18";
out = "3.4.0";
}
{
case = range "8.12" "8.17";
out = "3.3.0";
}
{
case = range "8.8" "8.16";
out = "3.2.0";
}
{
case = range "8.8" "8.13";
out = "3.1.0";
}
{
case = range "8.5" "8.9";
out = "3.0.2";
}
] null;
)) null;
release."3.4.3".sha256 = "sha256-bzzAIENU2OYTtmdBU9Xw8zyBvz9vqTiqjWSm7RnXXRA=";
release."3.4.2".sha256 = "sha256-aBTF8ZKu67Rb3ryCqFyejUXf/65KgG8i5je/ZMFSrj4=";
release."3.4.1".sha256 = "sha256-REhvIBl3EaL8CQqI34Gn7Xjf9NhPI3nrUAO26pSLbm0=";
@@ -14,39 +14,20 @@ mkCoqDerivation {
inherit version;
defaultVersion =
with lib.versions;
lib.switch
[ coq.coq-version ssreflect.version ]
[
{
cases = [
(range "8.17" "9.0")
(range "2.0.0" "2.4.0")
];
out = "0.2.2";
}
{
cases = [
(range "8.17" "9.0")
(range "2.0.0" "2.3.0")
];
out = "0.2.1";
}
{
cases = [
(range "8.17" "8.20")
(range "2.0.0" "2.2.0")
];
out = "0.2.0";
}
{
cases = [
(range "8.11" "8.20")
(isLe "2.0.0")
];
out = "0.1.1";
}
]
null;
let
cmc = c: mc: [
c
mc
];
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;
releaseRev = v: "v${v}";
@@ -15,64 +15,24 @@ mkCoqDerivation {
owner = "Karmaki";
repo = "coq-dpdgraph";
inherit version;
defaultVersion = lib.switch coq.coq-version [
{
case = "8.20";
out = "1.0+8.20";
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";
}
{
case = "8.19";
out = "1.0+8.19";
}
{
case = "8.18";
out = "1.0+8.18";
}
{
case = "8.17";
out = "1.0+8.17";
}
{
case = "8.16";
out = "1.0+8.16";
}
{
case = "8.15";
out = "1.0+8.15";
}
{
case = "8.14";
out = "1.0+8.14";
}
{
case = "8.13";
out = "1.0+8.13";
}
{
case = "8.12";
out = "0.6.8";
}
{
case = "8.11";
out = "0.6.7";
}
{
case = "8.10";
out = "0.6.6";
}
{
case = "8.9";
out = "0.6.5";
}
{
case = "8.8";
out = "0.6.3";
}
{
case = "8.7";
out = "0.6.2";
}
] null;
)) null;
release."1.0+8.20".sha256 = "sha256-szfH/OksCH3SCbcFjwEvLwHE5avmHp1vYiJM6KAXFqs=";
release."1.0+8.19".sha256 = "sha256-L1vjEydYiwDFTXES3sgfdaO/D50AbTJKBXUKUCgbpto=";
@@ -12,72 +12,26 @@
repo = "Coq-Equations";
opam-name = "rocq-equations";
inherit version;
defaultVersion = lib.switch coq.coq-version [
{
case = "9.0";
out = "1.3.1+9.0";
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";
}
{
case = "8.20";
out = "1.3.1+8.20";
}
{
case = "8.19";
out = "1.3+8.19";
}
{
case = "8.18";
out = "1.3+8.18";
}
{
case = "8.17";
out = "1.3+8.17";
}
{
case = "8.16";
out = "1.3+8.16";
}
{
case = "8.15";
out = "1.3+8.15";
}
{
case = "8.14";
out = "1.3+8.14";
}
{
case = "8.13";
out = "1.3+8.13";
}
{
case = "8.12";
out = "1.2.4+coq8.12";
}
{
case = "8.11";
out = "1.2.4+coq8.11";
}
{
case = "8.10";
out = "1.2.1+coq8.10-2";
}
{
case = "8.9";
out = "1.2.1+coq8.9";
}
{
case = "8.8";
out = "1.2+coq8.8";
}
{
case = "8.7";
out = "1.0+coq8.7";
}
{
case = "8.6";
out = "1.0+coq8.6";
}
] null;
)) null;
release."1.0+coq8.6".version = "1.0";
release."1.0+coq8.6".rev = "v1.0";
@@ -14,46 +14,21 @@
inherit version;
defaultVersion =
with lib.versions;
lib.switch
[ coq.coq-version mathcomp-boot.version ]
[
{
cases = [
(range "8.17" "9.0")
(range "2.0.0" "2.4.0")
];
out = "0.5.0";
}
{
cases = [
(range "8.17" "8.20")
(range "2.0.0" "2.3.0")
];
out = "0.4.0";
}
{
cases = [
(range "8.11" "8.20")
(range "1.12.0" "1.19.0")
];
out = "0.3.1";
}
{
cases = [
(range "8.11" "8.14")
(isLe "1.12.0")
];
out = "0.3.0";
}
{
cases = [
(range "8.10" "8.12")
(isLe "1.12.0")
];
out = "0.2.2";
}
]
null;
let
cmc = c: mc: [
c
mc
];
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;
releaseRev = v: "v${v}";
+10 -29
View File
@@ -15,36 +15,17 @@ mkCoqDerivation {
inherit version;
defaultVersion =
with lib.versions;
lib.switch coq.coq-version [
{
case = range "8.15" "9.0";
out = "4.2.1";
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";
}
{
case = range "8.14" "8.20";
out = "4.2.0";
}
{
case = range "8.14" "8.18";
out = "4.1.3";
}
{
case = range "8.14" "8.17";
out = "4.1.1";
}
{
case = range "8.14" "8.16";
out = "4.1.0";
}
{
case = range "8.7" "8.15";
out = "3.4.3";
}
{
case = range "8.5" "8.8";
out = "2.6.1";
}
] null;
)) 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=";
@@ -23,46 +23,21 @@ mkCoqDerivation {
inherit version;
defaultVersion =
with lib.versions;
lib.switch
[ coq.version mathcomp.version ]
[
{
cases = [
(isGe "8.16")
(isGe "2.0")
];
out = "1.4.1";
}
{
cases = [
(isGe "8.16")
"2.0.0"
];
out = "1.3.0";
}
{
cases = [
(isGe "8.11")
(range "1.12" "1.19")
];
out = "1.2.5";
}
{
cases = [
(isGe "8.11")
(range "1.11" "1.14")
];
out = "1.2.4";
}
{
cases = [
(isLe "8.13")
(lib.pred.inter (isGe "1.11.0") (isLt "1.13"))
];
out = "1.2.3";
}
]
null;
let
cmc = c: mc: [
c
mc
];
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;
propagatedBuildInputs = [
mathcomp.boot
+14 -33
View File
@@ -23,39 +23,20 @@ mkCoqDerivation {
inherit version;
defaultVersion =
with lib.versions;
lib.switch
[ coq.version mathcomp.version ]
[
{
cases = [
(range "8.16" "9.0")
(range "2.0" "2.4")
];
out = "2.3";
}
{
cases = [
(range "8.16" "9.0")
(range "2.0" "2.3")
];
out = "2.2";
}
{
cases = [
(range "8.10" "8.18")
(range "1.12.0" "1.18.0")
];
out = "1.17";
}
{
cases = [
(range "8.10" "8.12")
"1.11.0"
];
out = "1.11";
}
]
null;
let
cmc = c: mc: [
c
mc
];
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;
propagatedBuildInputs = [
mathcomp.boot
@@ -25,53 +25,22 @@ mkCoqDerivation {
inherit version;
defaultVersion =
with lib.versions;
lib.switch
[ coq.coq-version mathcomp.version ]
[
{
cases = [
(range "8.18" "9.0")
(range "2.0.0" "2.4.0")
];
out = "0.9.6";
}
{
cases = [
(range "8.16" "8.19")
(range "2.0.0" "2.3.0")
];
out = "0.9.4";
}
{
cases = [
(range "8.16" "8.18")
(range "2.0.0" "2.1.0")
];
out = "0.9.3";
}
{
cases = [
(range "8.14" "8.18")
(range "1.13.0" "1.18.0")
];
out = "0.9.2";
}
{
cases = [
(range "8.14" "8.16")
(range "1.13.0" "1.14.0")
];
out = "0.9.1";
}
{
cases = [
(range "8.12" "8.13")
(range "1.12.0" "1.14.0")
];
out = "0.9";
}
]
null;
let
cmc = c: mc: [
c
mc
];
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;
propagatedBuildInputs = [
mathcomp.algebra
@@ -15,44 +15,19 @@ let
inherit version;
defaultVersion =
with lib.versions;
lib.switch coq.coq-version [
{
case = range "8.20" "9.0";
out = "1.9.1";
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";
}
{
case = range "8.19" "8.20";
out = "1.8.0";
}
{
case = range "8.18" "8.20";
out = "1.7.1";
}
{
case = range "8.16" "8.18";
out = "1.6.0";
}
{
case = range "8.15" "8.18";
out = "1.5.0";
}
{
case = range "8.15" "8.17";
out = "1.4.0";
}
{
case = range "8.13" "8.14";
out = "1.2.0";
}
{
case = range "8.12" "8.13";
out = "1.1.0";
}
{
case = isEq "8.11";
out = "0.10.0";
}
] null;
)) 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=";
@@ -15,14 +15,13 @@ mkCoqDerivation {
defaultVersion =
let
inherit (lib.versions) range;
inherit (lib.versions) isLe range;
in
lib.switch coq.coq-version [
{
case = range "8.14" "8.19";
out = "0.2.1";
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;
)) null;
release = {
"0.2.1".sha256 = "sha256-CIcaXEojNdajXNoMBjGlQRc1sOJSKgUlditNxbNSPgk=";
};
@@ -20,16 +20,12 @@
inherit version;
defaultVersion =
with lib.versions;
lib.switch coq.coq-version [
{
case = range "8.13" "8.16";
out = "0.9";
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";
}
{
case = range "8.11" "8.12";
out = "0.4";
}
] null;
)) null;
useDune = true;
@@ -19,44 +19,19 @@ mkCoqDerivation rec {
inherit version;
defaultVersion =
with lib.versions;
lib.switch coq.coq-version [
{
case = range "8.13" "8.20";
out = "4.11.1";
lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
lib.mapAttrsToList (out: case: { inherit case out; }) {
"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";
}
{
case = range "8.12" "8.19";
out = "4.10.0";
}
{
case = range "8.12" "8.18";
out = "4.9.0";
}
{
case = range "8.12" "8.17";
out = "4.8.0";
}
{
case = range "8.12" "8.16";
out = "4.6.0";
}
{
case = range "8.8" "8.16";
out = "4.5.2";
}
{
case = range "8.8" "8.12";
out = "4.0.0";
}
{
case = range "8.7" "8.11";
out = "3.4.2";
}
{
case = range "8.5" "8.6";
out = "3.3.0";
}
] null;
)) null;
release."4.11.1".sha256 = "sha256-QWZvU468rOhK796xCCEawW6rhCRTPnE0iLll9ynKflo=";
release."4.11.0".sha256 = "sha256-vPwa4zSjyvxHLGDoNaBnHV2pb77dnQFbC50BL80fcvE=";
release."4.10.0".sha256 = "sha256-MZJVoKGLXjDabdv9BuUSK1L9z1cubzC9cqVuWevKIXQ=";
+10 -29
View File
@@ -13,36 +13,17 @@ mkCoqDerivation {
inherit version;
defaultVersion =
with lib.versions;
lib.switch coq.coq-version [
{
case = range "8.19" "9.0";
out = "4.3.0";
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";
}
{
case = range "8.18" "8.19";
out = "4.2.0";
}
{
case = range "8.16" "8.18";
out = "4.1.0";
}
{
case = range "8.13" "8.17";
out = "4.0.0";
}
{
case = range "8.12" "8.14";
out = "3.5.0";
}
{
case = range "8.11" "8.13";
out = "3.4.0";
}
{
case = range "8.9" "8.10";
out = "3.3.0";
}
] null;
)) 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=";
+11 -33
View File
@@ -23,40 +23,18 @@
inherit version;
defaultVersion =
with lib.versions;
lib.switch coq.coq-version [
{
case = isEq "8.20";
out = "8.20.0";
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";
}
{
case = isEq "8.19";
out = "8.19.0";
}
{
case = isEq "8.18";
out = "8.18.0";
}
{
case = isEq "8.17";
out = "8.17.0";
}
{
case = isEq "8.16";
out = "8.16.0";
}
{
case = isEq "8.15";
out = "8.15.0";
}
{
case = isEq "8.14";
out = "8.14.0";
}
{
case = isEq "8.13";
out = "8.13+no";
}
] null;
)) null;
mlPlugin = true;
nativeBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]);
@@ -15,14 +15,13 @@ mkCoqDerivation {
defaultVersion =
let
inherit (lib.versions) range;
inherit (lib.versions) isLe range;
in
lib.switch coq.coq-version [
{
case = range "8.12" "8.19";
out = "0.1.1";
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;
)) null;
release = {
"0.1.1".sha256 = "sha256-IFwIj8dxW4jm2gvuUJ8LKZFSJeljp0bsn8fezxY6t2o=";
};
+12 -19
View File
@@ -15,25 +15,18 @@ mkCoqDerivation {
inherit version;
defaultVersion =
with lib.versions;
lib.switch
[ coq.version mathcomp.version ]
[
{
cases = [
(range "8.19" "9.0")
(range "2.2" "2.4")
];
out = "2025.02.0";
}
{
cases = [
(isEq "8.18")
(isEq "2.2")
];
out = "2024.07.2";
}
]
null;
let
cmc = c: mc: [
c
mc
];
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;
releaseRev = v: "v${v}";
release."2025.02.0".sha256 = "sha256-Jlf0+VPuYWXdWyKHKHSp7h/HuCCp4VkcrgDAmh7pi5s=";
+6 -10
View File
@@ -15,18 +15,14 @@
defaultVersion =
let
inherit (lib.versions) range;
inherit (lib.versions) isLe range;
in
lib.switch coq.coq-version [
{
case = range "8.14" "9.0";
out = "0.2.0";
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";
}
{
case = range "8.14" "8.20";
out = "0.1.3";
}
] null;
)) null;
release = {
"0.2.0".sha256 = "sha256-qDRTgWLUvu4x3/d3BDcqo2I4W5ZmLyRiwuY/Tm/FuKA=";
"0.1.3".sha256 = "sha256-lElAzW4IuX+BB6ngDjlyKn0MytLRfbhQanB+Lct/WR0=";
@@ -18,32 +18,20 @@ mkCoqDerivation {
inherit version;
defaultVersion =
lib.switch
[ coq.version mathcomp.version ]
[
{
cases = [
(lib.versions.range "8.10" "8.16")
(lib.versions.range "1.12.0" "1.15.0")
];
out = "1.2.1";
}
{
cases = [
(lib.versions.range "8.10" "8.15")
(lib.versions.range "1.12.0" "1.14.0")
];
out = "1.2.0";
}
{
cases = [
(lib.versions.range "8.10" "8.14")
(lib.versions.range "1.11.0" "1.12.0")
];
out = "1.1.2";
}
]
null;
with lib.versions;
let
cmc = c: mc: [
c
mc
];
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;
release."1.2.1".sha256 = "sha256-M1q6WIPBsayHde2hwlTxylH169hcTs3OuFsEkM0e3yc=";
release."1.2.0".sha256 = "1picd4m85ipj22j3b84cv8ab3330radzrhd6kp0gpxq14dhv02c2";
@@ -20,46 +20,21 @@ mkCoqDerivation {
defaultVersion =
with lib.versions;
lib.switch
[ coq.coq-version mathcomp-algebra.version ]
[
{
cases = [
(range "8.20" "9.0")
(isGe "2.4")
];
out = "1.2.5";
}
{
cases = [
(range "8.16" "9.0")
(isGe "2.0")
];
out = "1.2.4";
}
{
cases = [
(range "8.16" "8.18")
(isGe "2.0")
];
out = "1.2.2";
}
{
cases = [
(range "8.16" "8.19")
(isGe "1.15")
];
out = "1.1.1";
}
{
cases = [
(range "8.13" "8.16")
(isGe "1.12")
];
out = "1.0.0";
}
]
null;
let
cmc = c: mc: [
c
mc
];
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;
release."1.0.0".sha256 = "sha256-kszARPBizWbxSQ/Iqpf2vLbxYc6AjpUCLnSNlPcNfls=";
release."1.1.1".sha256 = "sha256-5wItMeeTRoJlRBH3zBNc2VUZn6pkDde60YAvXTx+J3U=";
@@ -44,119 +44,32 @@ let
release."0.2.3".sha256 = "0p9mr8g1qma6h10qf7014dv98ln90dfkwn76ynagpww7qap8s966";
defaultVersion =
with lib.versions;
let
inherit (lib.versions) range;
cmc = c: mc: [
c
mc
];
in
lib.switch
[ coq.version mathcomp.version ]
[
{
cases = [
(range "8.20" "9.0")
(range "2.1.0" "2.4.0")
];
out = "1.11.0";
}
{
cases = [
(range "8.19" "8.20")
(range "2.1.0" "2.3.0")
];
out = "1.9.0";
}
{
cases = [
(range "8.17" "8.20")
(range "2.0.0" "2.2.0")
];
out = "1.1.0";
}
{
cases = [
(range "8.17" "8.19")
(range "1.17.0" "1.19.0")
];
out = "0.7.0";
}
{
cases = [
(range "8.17" "8.18")
(range "1.15.0" "1.18.0")
];
out = "0.6.7";
}
{
cases = [
(range "8.17" "8.18")
(range "1.15.0" "1.18.0")
];
out = "0.6.6";
}
{
cases = [
(range "8.14" "8.18")
(range "1.15.0" "1.17.0")
];
out = "0.6.5";
}
{
cases = [
(range "8.14" "8.18")
(range "1.13.0" "1.16.0")
];
out = "0.6.1";
}
{
cases = [
(range "8.14" "8.18")
(range "1.13" "1.15")
];
out = "0.5.2";
}
{
cases = [
(range "8.13" "8.15")
(range "1.13" "1.14")
];
out = "0.5.1";
}
{
cases = [
(range "8.13" "8.15")
(range "1.12" "1.14")
];
out = "0.3.13";
}
{
cases = [
(range "8.11" "8.14")
(range "1.12" "1.13")
];
out = "0.3.10";
}
{
cases = [
(range "8.10" "8.12")
"1.11.0"
];
out = "0.3.3";
}
{
cases = [
(range "8.10" "8.11")
"1.11.0"
];
out = "0.3.1";
}
{
cases = [
(range "8.8" "8.11")
(range "1.8" "1.10")
];
out = "0.2.3";
}
]
null;
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;
# list of analysis packages sorted by dependency order
packages = {
@@ -18,18 +18,17 @@ mkCoqDerivation {
inherit version;
defaultVersion =
with lib.versions;
lib.switch
[ coq.version mathcomp.version ]
[
{
cases = [
(range "8.13" "8.16")
(range "1.12.0" "1.17.0")
];
out = "1.0.2";
}
]
null;
let
cmc = c: mc: [
c
mc
];
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;
release."1.0.2".sha256 = "sha256-llxyMKYvWUA7fyroG1S/jtpioAoArmarR1edi3cikcY=";
@@ -23,16 +23,12 @@ mkCoqDerivation {
inherit version;
defaultVersion =
with lib.versions;
lib.switch coq.version [
{
case = range "8.10" "9.0";
out = "1.0.2";
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";
}
{
case = range "8.5" "8.14";
out = "1.0.0";
}
] null;
)) null;
propagatedBuildInputs = [ mathcomp-boot ];
@@ -17,88 +17,27 @@ mkCoqDerivation {
inherit version;
defaultVersion =
with lib.versions;
lib.switch
[ coq.version mathcomp-boot.version ]
[
{
cases = [
(range "8.20" "9.0")
(range "2.3" "2.4")
];
out = "2.2.0";
}
{
cases = [
(range "8.16" "9.0")
(range "2.0" "2.3")
];
out = "2.1.0";
}
{
cases = [
(range "8.16" "8.18")
(range "2.0" "2.1")
];
out = "2.0.0";
}
{
cases = [
(range "8.13" "8.20")
(range "1.12" "1.19")
];
out = "1.5.2";
}
{
cases = [
(isGe "8.10")
(range "1.11" "1.17")
];
out = "1.5.1";
}
{
cases = [
(range "8.7" "8.11")
"1.11.0"
];
out = "1.5.0";
}
{
cases = [
(isEq "8.11")
(range "1.8" "1.10")
];
out = "1.4.0+coq-8.11";
}
{
cases = [
(range "8.7" "8.11.0")
(range "1.8" "1.10")
];
out = "1.4.0";
}
{
cases = [
(range "8.7" "8.11.0")
(range "1.8" "1.10")
];
out = "1.3.4";
}
{
cases = [
(range "8.7" "8.9")
"1.7.0"
];
out = "1.1.0";
}
{
cases = [
(range "8.6" "8.7")
(range "1.6.1" "1.7")
];
out = "1.0.0";
}
]
null;
let
cmc = c: mc: [
c
mc
];
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;
release = {
"2.2.0".sha256 = "sha256-oDQEZOutrJxmN8FvzovUIhqw0mwc8Ej7thrieJrW8BY=";
"2.1.0".sha256 = "sha256-gh0cnhdVDyo+D5zdtxLc10kGKQLQ3ITzHnMC45mCtpY=";
@@ -20,81 +20,26 @@
defaultVersion =
with lib.versions;
lib.switch
[ coq.version mathcomp-analysis.version ]
[
{
cases = [
(range "8.20" "8.20")
(isGe "1.10")
];
out = "0.9.3";
}
{
cases = [
(range "8.19" "8.20")
(isGe "1.9")
];
out = "0.9.1";
}
{
cases = [
(range "8.19" "8.20")
(isGe "1.7")
];
out = "0.7.7";
}
{
cases = [
(range "8.19" "8.20")
(isGe "1.7")
];
out = "0.7.5";
}
{
cases = [
(range "8.18" "8.20")
(isGe "1.5")
];
out = "0.7.3";
}
{
cases = [
(range "8.18" "8.19")
(isGe "1.2")
];
out = "0.7.2";
}
{
cases = [
(range "8.17" "8.19")
(isGe "1.0")
];
out = "0.7.1";
}
{
cases = [
(isGe "8.17")
(range "0.6.6" "0.7.0")
];
out = "0.6.1";
}
{
cases = [
(range "8.17" "8.18")
(range "0.6.0" "0.6.7")
];
out = "0.5.2";
}
{
cases = [
(range "8.15" "8.16")
(range "0.5.4" "0.6.5")
];
out = "0.5.1";
}
]
null;
let
cmc = c: mc: [
c
mc
];
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;
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=";
@@ -19,39 +19,20 @@ mkCoqDerivation {
inherit version;
defaultVersion =
with lib.versions;
lib.switch
[ coq.version mathcomp-ssreflect.version ]
[
{
cases = [
(range "8.16" "9.0")
(range "2.0.0" "2.4.0")
];
out = "1.0.3";
}
{
cases = [
(range "8.16" "9.0")
(range "2.0.0" "2.3.0")
];
out = "1.0.2";
}
{
cases = [
(range "8.12" "8.18")
(range "1.12.0" "1.17.0")
];
out = "1.0.1";
}
{
cases = [
(range "8.10" "8.16")
(range "1.12.0" "1.17.0")
];
out = "1.0.0";
}
]
null;
let
cmc = c: mc: [
c
mc
];
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;
release."1.0.3".sha256 = "sha256-5lpOCDyH6NFzGLvnXHHAnR7Qv5oXsUyC8TLBFrIiBag=";
release."1.0.2".sha256 = "sha256-U20xgA+e9KTRdvILD1cxN6ia+dlA8uBTIbc4QlKz9ss=";
release."1.0.1".sha256 = "sha256-utNjFCAqC5xOuhdyKhfMZkRYJD0xv9Gt6U3ZdQ56mek=";
@@ -57,25 +57,18 @@ mkCoqDerivation {
inherit version;
defaultVersion =
with lib.versions;
lib.switch
[ coq.version mathcomp.version ]
[
{
cases = [
(range "8.16" "9.0")
(isGe "2.0")
];
out = "3.2";
}
{
cases = [
(range "8.12" "8.20")
(range "1.12" "1.19")
];
out = "2.4";
}
]
null;
let
cmc = c: mc: [
c
mc
];
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;
propagatedBuildInputs = [
mathcomp.algebra
@@ -21,32 +21,19 @@ mkCoqDerivation {
defaultVersion =
with lib.versions;
lib.switch
[ coq.coq-version mathcomp-algebra.version ]
[
{
cases = [
(range "8.16" "9.0")
(isGe "2.0.0")
];
out = "1.5.0+2.0+8.16";
}
{
cases = [
(range "8.13" "8.20")
(range "1.12" "1.19.0")
];
out = "1.3.0+1.12+8.13";
}
{
cases = [
(range "8.13" "8.16")
(range "1.12" "1.17.0")
];
out = "1.1.0+1.12+8.13";
}
]
null;
let
cmc = c: mc: [
c
mc
];
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;
release."1.0.0+1.12+8.13".sha256 = "1j533vx6lacr89bj1bf15l1a0s7rvrx4l00wyjv99aczkfbz6h6k";
release."1.1.0+1.12+8.13".sha256 = "1plf4v6q5j7wvmd5gsqlpiy0vwlw6hy5daq2x42gqny23w9mi2pr";
@@ -31,86 +31,31 @@ let
withDoc = single && (args.withDoc or false);
defaultVersion =
let
inherit (lib.versions) range;
inherit (lib.versions) isLe range;
in
lib.switch coq.coq-version [
{
case = range "8.20" "9.0";
out = "2.4.0";
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";
}
{
case = range "8.19" "9.0";
out = "2.3.0";
}
{
case = range "8.17" "8.20";
out = "2.2.0";
}
{
case = range "8.17" "8.18";
out = "2.1.0";
}
{
case = range "8.17" "8.18";
out = "2.0.0";
}
{
case = range "8.19" "8.20";
out = "1.19.0";
}
{
case = range "8.17" "8.18";
out = "1.18.0";
}
{
case = range "8.15" "8.18";
out = "1.17.0";
}
{
case = range "8.13" "8.18";
out = "1.16.0";
}
{
case = range "8.14" "8.16";
out = "1.15.0";
}
{
case = range "8.11" "8.15";
out = "1.14.0";
}
{
case = range "8.11" "8.15";
out = "1.13.0";
}
{
case = range "8.10" "8.13";
out = "1.12.0";
}
{
case = range "8.7" "8.12";
out = "1.11.0";
}
{
case = range "8.7" "8.11";
out = "1.10.0";
}
{
case = range "8.7" "8.11";
out = "1.9.0";
}
{
case = range "8.7" "8.9";
out = "1.8.0";
}
{
case = range "8.6" "8.9";
out = "1.7.0";
}
{
case = range "8.5" "8.7";
out = "1.6.4";
}
] null;
)) null;
release = {
"2.4.0".sha256 = "sha256-A1XgLLwZRvKS8QyceCkSQa7ue6TYyf5fMft5gSx9NOs=";
"2.3.0".sha256 = "sha256-wa6OBig8rhAT4iwupSylyCAMhO69rADa0MQIX5zzL+Q=";
@@ -10,50 +10,22 @@
let
repo = "metacoq";
owner = "MetaCoq";
defaultVersion = lib.switch coq.coq-version [
{
case = "8.11";
out = "1.0-beta2-8.11";
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";
# 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";
}
{
case = "8.12";
out = "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)
# { case = "8.13"; out = "1.0-beta2-8.13"; }
{
case = "8.14";
out = "1.1-8.14";
}
{
case = "8.15";
out = "1.1-8.15";
}
{
case = "8.16";
out = "1.1-8.16";
}
{
case = "8.17";
out = "1.3.1-8.17";
}
{
case = "8.18";
out = "1.3.1-8.18";
}
{
case = "8.19";
out = "1.3.3-8.19";
}
{
case = "8.20";
out = "1.3.4-8.20";
}
{
case = "9.0";
out = "1.3.4-9.0";
}
] null;
)) null;
release = {
"1.0-beta2-8.11".sha256 = "sha256-I9YNk5Di6Udvq5/xpLSNflfjRyRH8fMnRzbo3uhpXNs=";
"1.0-beta2-8.12".sha256 = "sha256-I8gpmU9rUQJh0qfp5KOgDNscVvCybm5zX4TINxO1TVA=";
@@ -10,12 +10,11 @@
let
repo = "metarocq";
owner = "MetaRocq";
defaultVersion = lib.switch coq.coq-version [
{
case = "9.0";
out = "1.4-9.0";
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;
)) null;
release = {
"1.4-9.0".sha256 = "sha256-5QecDAMkvgfDPZ7/jDfnOgcE+Eb1LTAozP7nz6nkuxg=";
};
@@ -21,102 +21,29 @@ mkCoqDerivation {
inherit version;
defaultVersion =
with lib.versions;
lib.switch
[ coq.version mathcomp.version ]
[
{
cases = [
(range "8.18" "9.0")
(range "2.1.0" "2.4.0")
];
out = "2.4.0";
}
{
cases = [
(range "8.17" "9.0")
(range "2.1.0" "2.3.0")
];
out = "2.3.0";
}
{
cases = [
(range "8.17" "8.20")
(isGe "2.1.0")
];
out = "2.2.0";
}
{
cases = [
(range "8.16" "8.18")
"2.1.0"
];
out = "2.1.0";
}
{
cases = [
(range "8.16" "8.18")
"2.0.0"
];
out = "2.0.0";
}
{
cases = [
(isGe "8.15")
(range "1.15.0" "1.19.0")
];
out = "1.6.0";
}
{
cases = [
(isGe "8.10")
(range "1.13.0" "1.17.0")
];
out = "1.5.6";
}
{
cases = [
(range "8.10" "8.16")
(range "1.12.0" "1.15.0")
];
out = "1.5.5";
}
{
cases = [
(range "8.10" "8.12")
"1.12.0"
];
out = "1.5.3";
}
{
cases = [
(range "8.7" "8.12")
"1.11.0"
];
out = "1.5.2";
}
{
cases = [
(range "8.7" "8.11")
(range "1.8" "1.10")
];
out = "1.5.0";
}
{
cases = [
(range "8.7" "8.10")
(range "1.8" "1.10")
];
out = "1.4";
}
{
cases = [
"8.6"
(range "1.6" "1.7")
];
out = "1.1";
}
]
null;
let
cmc = c: mc: [
c
mc
];
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;
release = {
"2.4.0".sha256 = "sha256-7zfIddRH+Sl4nhEPtS/lMZwRUZI45AVFpcC/UC8Z0Yo=";
"2.3.0".sha256 = "sha256-usIcxHOAuN+f/j3WjVbPrjz8Hl9ac8R6kYeAKi3CEts=";
@@ -19,28 +19,15 @@ mkCoqDerivation {
inherit version;
defaultVersion =
with lib.versions;
lib.switch mathcomp.character.version [
{
case = (range "2.2.0" "2.4.0");
out = "2.2.0";
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");
}
{
case = (range "2.1.0" "2.3.0");
out = "2.1.0";
}
{
case = (range "1.13.0" "1.15.0");
out = "1.14.0";
}
{
case = (range "1.12.0" "1.14.0");
out = "1.13.0";
}
{
case = (range "1.10.0" "1.12.0");
out = "1.12.0";
}
] null;
)) null;
propagatedBuildInputs = [
mathcomp.character
@@ -21,39 +21,20 @@ mkCoqDerivation {
inherit version;
defaultVersion =
with lib.versions;
lib.switch
[ coq.coq-version mathcomp.version ]
[
{
cases = [
(range "8.16" "9.0")
(range "2.0.0" "2.4.0")
];
out = "1.2.2";
}
{
cases = [
(range "8.16" "9.0")
(range "2.0.0" "2.3.0")
];
out = "1.2.1";
}
{
cases = [
(range "8.16" "8.18")
(range "2.0.0" "2.1.0")
];
out = "1.2.0";
}
{
cases = [
(range "8.10" "8.20")
(isLt "2.0.0")
];
out = "1.1.3";
}
]
null;
let
cmc = c: mc: [
c
mc
];
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;
propagatedBuildInputs = [
mathcomp.ssreflect
@@ -28,52 +28,21 @@ mkCoqDerivation {
inherit version;
defaultVersion =
with lib.versions;
lib.switch coq.coq-version [
{
case = isEq "8.20";
out = "1.7.11";
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";
}
{
case = range "8.18" "8.19";
out = "1.7.10";
}
{
case = isEq "8.17";
out = "1.7.9";
}
{
case = isEq "8.16";
out = "1.7.8";
}
{
case = isEq "8.15";
out = "1.7.7";
}
{
case = isEq "8.14";
out = "1.7.6";
}
{
case = isEq "8.13";
out = "1.7.5";
}
{
case = isEq "8.12";
out = "1.7.4";
}
{
case = isEq "8.11";
out = "1.7.3";
}
{
case = isEq "8.10";
out = "1.7.2";
}
{
case = isEq "8.9";
out = "1.7.1";
}
] null;
)) null;
mlPlugin = true;
@@ -14,20 +14,13 @@
inherit version;
defaultVersion =
with lib.versions;
lib.switch coq.coq-version [
{
case = range "8.17" "9.0";
out = "1.10.0";
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";
}
{
case = range "8.11" "8.19";
out = "1.8.0";
}
{
case = range "8.7" "8.13";
out = "1.3.0";
}
] null;
)) null;
release."1.10.0".sha256 = "sha256-67cBhLvRMWLWBL7NXK1zZTQC4PtSKu9qtesU4SqKkOw=";
release."1.8.0".sha256 = "sha256-3ADNeXrBIpYRlfUW+LkLHUWV1w1HFrVc/TZISMuwvRY=";
release."1.7.0".sha256 = "sha256:1a1q9x2abx71hqvjdai3n12jxzd49mhf3nqqh3ya2ssl2lj609ci";
@@ -19,46 +19,27 @@
inherit version;
defaultVersion =
with lib.versions;
lib.switch
[ coq.coq-version mathcomp-boot.version ]
[
{
cases = [
(range "8.18" "9.0")
(range "2.3.0" "2.4.0")
];
out = "0.2.4";
}
{
cases = [
(range "8.18" "8.20")
(range "2.3.0" "2.3.0")
];
out = "0.2.3";
}
{
cases = [
(range "8.18" "8.20")
(range "2.1.0" "2.2.0")
];
out = "0.2.2";
}
let
cmc = c: mc: [
c
mc
];
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");
# This is the original dependency:
# { cases = ["8.17" "1.18.0"]; out = "0.1.0"; }
# "0.1.0" = ["8.17" "1.18.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.)
{
cases = [
"8.17"
"1.17.0"
];
out = "0.1.0";
}
]
null;
"0.1.0" = cmc "8.17" "1.17.0";
}
)) null;
releaseRev = v: "v${v}";
@@ -10,12 +10,11 @@ let
repo = "stalmarck";
defaultVersion =
with lib.versions;
lib.switch coq.coq-version [
{
case = isEq "8.20";
out = "8.20.0";
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;
)) null;
release = {
"8.20.0".sha256 = "sha256-jITxQT1jLyZvWCGPnmK8i3IrwsZwMPOV0aBe9r22TIQ=";
};
@@ -15,17 +15,12 @@
inherit version;
defaultVersion =
with lib.versions;
lib.switch coq.version [
{
case = isEq "9.0";
out = "9.0.0";
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
}
# the one below is artificial as stdlib was included in Coq before
{
case = isLt "9.0";
out = "9.0.0";
}
] null;
)) null;
releaseRev = v: "V${v}";
release."9.0.0".sha256 = "sha256-2l7ak5Q/NbiNvUzIVXOniEneDXouBMNSSVFbD1Pf8cQ=";
+10 -29
View File
@@ -13,36 +13,17 @@ mkCoqDerivation {
owner = "iris";
defaultVersion =
with lib.versions;
lib.switch coq.coq-version [
{
case = range "8.19" "9.0";
out = "1.11.0";
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";
}
{
case = range "8.18" "8.19";
out = "1.10.0";
}
{
case = range "8.16" "8.18";
out = "1.9.0";
}
{
case = range "8.13" "8.17";
out = "1.8.0";
}
{
case = range "8.12" "8.14";
out = "1.6.0";
}
{
case = range "8.11" "8.13";
out = "1.5.0";
}
{
case = range "8.8" "8.10";
out = "1.4.0";
}
] null;
)) null;
release."1.11.0".sha256 = "sha256-yqnkaA5gUdZBJZ3JnvPYh11vKQRl0BAnior1yGowG7k=";
release."1.10.0".sha256 = "sha256-bfynevIKxAltvt76lsqVxBmifFkzEhyX8lRgTKxr21I=";
release."1.9.0".sha256 = "sha256-OXeB+XhdyzWMp5Karsz8obp0rTeMKrtG7fu/tmc9aeI=";
@@ -12,12 +12,11 @@ mkRocqDerivation {
inherit version;
defaultVersion =
with lib.versions;
lib.switch rocq-core.rocq-version [
{
case = range "9.0" "9.0";
out = "9.0.0+rocq${rocq-core.rocq-version}";
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;
)) 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}";
@@ -13,12 +13,11 @@ let
inherit version;
defaultVersion =
with lib.versions;
lib.switch rocq-core.rocq-version [
{
case = range "9.0" "9.0";
out = "1.9.1";
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;
)) null;
release."1.9.1".sha256 = "sha256-AiS0ezMyfIYlXnuNsVLz1GlKQZzJX+ilkrKkbo0GrF0=";
releaseRev = v: "v${v}";
@@ -12,12 +12,11 @@ let
if elpi-version != null then
elpi-version
else
(lib.switch rocq-core.rocq-version [
{
case = "9.0";
out = "2.0.7";
(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";
}
] { });
)) { });
elpi = rocq-core.ocamlPackages.elpi.override { version = default-elpi-version; };
propagatedBuildInputs_wo_elpi = [
rocq-core.ocamlPackages.findlib
@@ -28,12 +27,14 @@ let
repo = "coq-elpi";
owner = "LPCIC";
inherit version;
defaultVersion = lib.switch rocq-core.rocq-version [
{
case = "9.0";
out = "2.5.2";
}
] null;
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;
release."2.5.2".sha256 = "sha256-lLzjPrbVB3rrqox528YiheUb0u89R84Xmrgkn0oplOs=";
releaseRev = v: "v${v}";
@@ -14,17 +14,11 @@ mkRocqDerivation {
inherit version;
defaultVersion =
with lib.versions;
lib.switch rocq-core.version [
{
case = isEq "9.0";
out = "9.0.0";
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";
}
# the one below is artificial as stdlib was included in Coq before
{
case = isLt "9.0";
out = "9.0.0";
}
] null;
)) null;
releaseRev = v: "V${v}";
release."9.0.0".sha256 = "sha256-2l7ak5Q/NbiNvUzIVXOniEneDXouBMNSSVFbD1Pf8cQ=";