From 0ddb075c4db5d065e42867f45247b3a0091c486e Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 19 Jun 2025 12:29:43 +0200 Subject: [PATCH] coqPackages.*: fix formatting --- .../coq-modules/bignums/default.nix | 19 +-- .../coq-modules/coq-elpi/default.nix | 122 ++++------------ .../coq-modules/coqeal/default.nix | 95 +++--------- .../coq-modules/coquelicot/default.nix | 39 ++--- .../coq-modules/deriving/default.nix | 47 ++---- .../coq-modules/dpdgraph/default.nix | 74 +++------- .../coq-modules/equations/default.nix | 84 +++-------- .../coq-modules/extructures/default.nix | 55 ++----- .../development/coq-modules/flocq/default.nix | 39 ++--- .../coq-modules/fourcolor/default.nix | 55 ++----- pkgs/development/coq-modules/gaia/default.nix | 47 ++---- .../coq-modules/graph-theory/default.nix | 63 +++----- .../coq-modules/hierarchy-builder/default.nix | 49 ++----- pkgs/development/coq-modules/http/default.nix | 11 +- .../coq-modules/hydra-battles/default.nix | 14 +- .../coq-modules/interval/default.nix | 49 ++----- pkgs/development/coq-modules/iris/default.nix | 39 ++--- .../coq-modules/itauto/default.nix | 44 ++---- .../coq-modules/itree-io/default.nix | 11 +- .../coq-modules/jasmin/default.nix | 31 ++-- pkgs/development/coq-modules/json/default.nix | 16 +-- .../coq-modules/mathcomp-abel/default.nix | 40 ++---- .../mathcomp-algebra-tactics/default.nix | 55 ++----- .../coq-modules/mathcomp-analysis/default.nix | 135 ++++-------------- .../coq-modules/mathcomp-apery/default.nix | 23 ++- .../mathcomp-bigenough/default.nix | 14 +- .../coq-modules/mathcomp-finmap/default.nix | 103 +++---------- .../coq-modules/mathcomp-infotheo/default.nix | 95 +++--------- .../coq-modules/mathcomp-tarjan/default.nix | 47 ++---- .../coq-modules/mathcomp-word/default.nix | 31 ++-- .../coq-modules/mathcomp-zify/default.nix | 39 ++--- .../coq-modules/mathcomp/default.nix | 101 +++---------- .../coq-modules/metacoq/default.nix | 58 ++------ .../coq-modules/metarocq/default.nix | 9 +- .../coq-modules/multinomials/default.nix | 119 +++------------ .../coq-modules/odd-order/default.nix | 29 ++-- .../coq-modules/reglang/default.nix | 47 ++---- .../coq-modules/relation-algebra/default.nix | 59 ++------ .../coq-modules/simple-io/default.nix | 19 +-- .../coq-modules/ssprove/default.nix | 49 ++----- .../coq-modules/stalmarck/default.nix | 9 +- .../coq-modules/stdlib/default.nix | 15 +- .../development/coq-modules/stdpp/default.nix | 39 ++--- .../rocq-modules/bignums/default.nix | 9 +- .../hierarchy-builder/default.nix | 9 +- .../rocq-modules/rocq-elpi/default.nix | 23 +-- .../rocq-modules/stdlib/default.nix | 14 +- 47 files changed, 578 insertions(+), 1615 deletions(-) diff --git a/pkgs/development/coq-modules/bignums/default.nix b/pkgs/development/coq-modules/bignums/default.nix index 242b05d4664f..6d38525921cf 100644 --- a/pkgs/development/coq-modules/bignums/default.nix +++ b/pkgs/development/coq-modules/bignums/default.nix @@ -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="; diff --git a/pkgs/development/coq-modules/coq-elpi/default.nix b/pkgs/development/coq-modules/coq-elpi/default.nix index 332dc6344106..baa817b33138 100644 --- a/pkgs/development/coq-modules/coq-elpi/default.nix +++ b/pkgs/development/coq-modules/coq-elpi/default.nix @@ -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="; diff --git a/pkgs/development/coq-modules/coqeal/default.nix b/pkgs/development/coq-modules/coqeal/default.nix index 603d2be00601..7b0d58845adb 100644 --- a/pkgs/development/coq-modules/coqeal/default.nix +++ b/pkgs/development/coq-modules/coqeal/default.nix @@ -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="; diff --git a/pkgs/development/coq-modules/coquelicot/default.nix b/pkgs/development/coq-modules/coquelicot/default.nix index 8832ddcec24c..274f41d111ad 100644 --- a/pkgs/development/coq-modules/coquelicot/default.nix +++ b/pkgs/development/coq-modules/coquelicot/default.nix @@ -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="; diff --git a/pkgs/development/coq-modules/deriving/default.nix b/pkgs/development/coq-modules/deriving/default.nix index 9f20bdc3b335..0dffe5e50e41 100644 --- a/pkgs/development/coq-modules/deriving/default.nix +++ b/pkgs/development/coq-modules/deriving/default.nix @@ -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}"; diff --git a/pkgs/development/coq-modules/dpdgraph/default.nix b/pkgs/development/coq-modules/dpdgraph/default.nix index 76e82bfbe106..d48290887f22 100644 --- a/pkgs/development/coq-modules/dpdgraph/default.nix +++ b/pkgs/development/coq-modules/dpdgraph/default.nix @@ -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="; diff --git a/pkgs/development/coq-modules/equations/default.nix b/pkgs/development/coq-modules/equations/default.nix index ab4f827eef0b..0ab9f55039ed 100644 --- a/pkgs/development/coq-modules/equations/default.nix +++ b/pkgs/development/coq-modules/equations/default.nix @@ -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"; diff --git a/pkgs/development/coq-modules/extructures/default.nix b/pkgs/development/coq-modules/extructures/default.nix index e57da9deb4f7..0635ea5f05e2 100644 --- a/pkgs/development/coq-modules/extructures/default.nix +++ b/pkgs/development/coq-modules/extructures/default.nix @@ -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}"; diff --git a/pkgs/development/coq-modules/flocq/default.nix b/pkgs/development/coq-modules/flocq/default.nix index 091b5275d7a4..9f83232d6504 100644 --- a/pkgs/development/coq-modules/flocq/default.nix +++ b/pkgs/development/coq-modules/flocq/default.nix @@ -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="; diff --git a/pkgs/development/coq-modules/fourcolor/default.nix b/pkgs/development/coq-modules/fourcolor/default.nix index 5effd74fc033..10f11f7f236b 100644 --- a/pkgs/development/coq-modules/fourcolor/default.nix +++ b/pkgs/development/coq-modules/fourcolor/default.nix @@ -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 diff --git a/pkgs/development/coq-modules/gaia/default.nix b/pkgs/development/coq-modules/gaia/default.nix index 9dc1865dcea3..3157176a6e4b 100644 --- a/pkgs/development/coq-modules/gaia/default.nix +++ b/pkgs/development/coq-modules/gaia/default.nix @@ -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 diff --git a/pkgs/development/coq-modules/graph-theory/default.nix b/pkgs/development/coq-modules/graph-theory/default.nix index b07e5dff78e3..ab4eb73fc7e9 100644 --- a/pkgs/development/coq-modules/graph-theory/default.nix +++ b/pkgs/development/coq-modules/graph-theory/default.nix @@ -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 diff --git a/pkgs/development/coq-modules/hierarchy-builder/default.nix b/pkgs/development/coq-modules/hierarchy-builder/default.nix index 07064760975e..fc57e1b44834 100644 --- a/pkgs/development/coq-modules/hierarchy-builder/default.nix +++ b/pkgs/development/coq-modules/hierarchy-builder/default.nix @@ -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="; diff --git a/pkgs/development/coq-modules/http/default.nix b/pkgs/development/coq-modules/http/default.nix index 5eb5fa79e2ef..926f2b743712 100644 --- a/pkgs/development/coq-modules/http/default.nix +++ b/pkgs/development/coq-modules/http/default.nix @@ -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="; }; diff --git a/pkgs/development/coq-modules/hydra-battles/default.nix b/pkgs/development/coq-modules/hydra-battles/default.nix index 74f57cc77d62..648a6d3229fc 100644 --- a/pkgs/development/coq-modules/hydra-battles/default.nix +++ b/pkgs/development/coq-modules/hydra-battles/default.nix @@ -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; diff --git a/pkgs/development/coq-modules/interval/default.nix b/pkgs/development/coq-modules/interval/default.nix index eacc9e91774d..9ed1576170a0 100644 --- a/pkgs/development/coq-modules/interval/default.nix +++ b/pkgs/development/coq-modules/interval/default.nix @@ -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="; diff --git a/pkgs/development/coq-modules/iris/default.nix b/pkgs/development/coq-modules/iris/default.nix index 8eb6340957d3..7bfdd94d3c27 100644 --- a/pkgs/development/coq-modules/iris/default.nix +++ b/pkgs/development/coq-modules/iris/default.nix @@ -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="; diff --git a/pkgs/development/coq-modules/itauto/default.nix b/pkgs/development/coq-modules/itauto/default.nix index 6c1a592dc3e7..e7183563d8d4 100644 --- a/pkgs/development/coq-modules/itauto/default.nix +++ b/pkgs/development/coq-modules/itauto/default.nix @@ -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 ]); diff --git a/pkgs/development/coq-modules/itree-io/default.nix b/pkgs/development/coq-modules/itree-io/default.nix index d932513bbea5..c3df0dbf49a1 100644 --- a/pkgs/development/coq-modules/itree-io/default.nix +++ b/pkgs/development/coq-modules/itree-io/default.nix @@ -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="; }; diff --git a/pkgs/development/coq-modules/jasmin/default.nix b/pkgs/development/coq-modules/jasmin/default.nix index 73ee3dd6d317..c53ab153f3e9 100644 --- a/pkgs/development/coq-modules/jasmin/default.nix +++ b/pkgs/development/coq-modules/jasmin/default.nix @@ -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="; diff --git a/pkgs/development/coq-modules/json/default.nix b/pkgs/development/coq-modules/json/default.nix index 52fd5871f9d1..b48b8de4ec89 100644 --- a/pkgs/development/coq-modules/json/default.nix +++ b/pkgs/development/coq-modules/json/default.nix @@ -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="; diff --git a/pkgs/development/coq-modules/mathcomp-abel/default.nix b/pkgs/development/coq-modules/mathcomp-abel/default.nix index 8da24e652d92..925cbbdc62a7 100644 --- a/pkgs/development/coq-modules/mathcomp-abel/default.nix +++ b/pkgs/development/coq-modules/mathcomp-abel/default.nix @@ -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"; diff --git a/pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix b/pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix index 89e53c0e0f64..fc4cca84b4d0 100644 --- a/pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix +++ b/pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix @@ -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="; diff --git a/pkgs/development/coq-modules/mathcomp-analysis/default.nix b/pkgs/development/coq-modules/mathcomp-analysis/default.nix index 02103c2eb986..b24c6fa18849 100644 --- a/pkgs/development/coq-modules/mathcomp-analysis/default.nix +++ b/pkgs/development/coq-modules/mathcomp-analysis/default.nix @@ -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 = { diff --git a/pkgs/development/coq-modules/mathcomp-apery/default.nix b/pkgs/development/coq-modules/mathcomp-apery/default.nix index 390aae694fb6..697d0e970e6a 100644 --- a/pkgs/development/coq-modules/mathcomp-apery/default.nix +++ b/pkgs/development/coq-modules/mathcomp-apery/default.nix @@ -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="; diff --git a/pkgs/development/coq-modules/mathcomp-bigenough/default.nix b/pkgs/development/coq-modules/mathcomp-bigenough/default.nix index 45399fa5ce63..357fd97d93cf 100644 --- a/pkgs/development/coq-modules/mathcomp-bigenough/default.nix +++ b/pkgs/development/coq-modules/mathcomp-bigenough/default.nix @@ -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 ]; diff --git a/pkgs/development/coq-modules/mathcomp-finmap/default.nix b/pkgs/development/coq-modules/mathcomp-finmap/default.nix index 0d761eac6bcf..97dd95556200 100644 --- a/pkgs/development/coq-modules/mathcomp-finmap/default.nix +++ b/pkgs/development/coq-modules/mathcomp-finmap/default.nix @@ -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="; diff --git a/pkgs/development/coq-modules/mathcomp-infotheo/default.nix b/pkgs/development/coq-modules/mathcomp-infotheo/default.nix index c1f8d149c605..25d3827a89e3 100644 --- a/pkgs/development/coq-modules/mathcomp-infotheo/default.nix +++ b/pkgs/development/coq-modules/mathcomp-infotheo/default.nix @@ -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="; diff --git a/pkgs/development/coq-modules/mathcomp-tarjan/default.nix b/pkgs/development/coq-modules/mathcomp-tarjan/default.nix index 4f8549c00f89..a8d233af7d3b 100644 --- a/pkgs/development/coq-modules/mathcomp-tarjan/default.nix +++ b/pkgs/development/coq-modules/mathcomp-tarjan/default.nix @@ -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="; diff --git a/pkgs/development/coq-modules/mathcomp-word/default.nix b/pkgs/development/coq-modules/mathcomp-word/default.nix index 6175ae80538e..c43d7a34f2f6 100644 --- a/pkgs/development/coq-modules/mathcomp-word/default.nix +++ b/pkgs/development/coq-modules/mathcomp-word/default.nix @@ -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 diff --git a/pkgs/development/coq-modules/mathcomp-zify/default.nix b/pkgs/development/coq-modules/mathcomp-zify/default.nix index 3a6dd0c1b97d..2c91a5056496 100644 --- a/pkgs/development/coq-modules/mathcomp-zify/default.nix +++ b/pkgs/development/coq-modules/mathcomp-zify/default.nix @@ -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"; diff --git a/pkgs/development/coq-modules/mathcomp/default.nix b/pkgs/development/coq-modules/mathcomp/default.nix index 963fd6e2b6d2..0311a33a406c 100644 --- a/pkgs/development/coq-modules/mathcomp/default.nix +++ b/pkgs/development/coq-modules/mathcomp/default.nix @@ -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="; diff --git a/pkgs/development/coq-modules/metacoq/default.nix b/pkgs/development/coq-modules/metacoq/default.nix index 99c79f4e5fba..2856547930ad 100644 --- a/pkgs/development/coq-modules/metacoq/default.nix +++ b/pkgs/development/coq-modules/metacoq/default.nix @@ -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="; diff --git a/pkgs/development/coq-modules/metarocq/default.nix b/pkgs/development/coq-modules/metarocq/default.nix index 6eea8465cc67..a90df150f409 100644 --- a/pkgs/development/coq-modules/metarocq/default.nix +++ b/pkgs/development/coq-modules/metarocq/default.nix @@ -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="; }; diff --git a/pkgs/development/coq-modules/multinomials/default.nix b/pkgs/development/coq-modules/multinomials/default.nix index 93dcf55a6ab2..6cb2adc7aba6 100644 --- a/pkgs/development/coq-modules/multinomials/default.nix +++ b/pkgs/development/coq-modules/multinomials/default.nix @@ -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="; diff --git a/pkgs/development/coq-modules/odd-order/default.nix b/pkgs/development/coq-modules/odd-order/default.nix index 504b05508760..9c0b721141fc 100644 --- a/pkgs/development/coq-modules/odd-order/default.nix +++ b/pkgs/development/coq-modules/odd-order/default.nix @@ -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 diff --git a/pkgs/development/coq-modules/reglang/default.nix b/pkgs/development/coq-modules/reglang/default.nix index cb00b6f48991..d3d1bfc15ff9 100644 --- a/pkgs/development/coq-modules/reglang/default.nix +++ b/pkgs/development/coq-modules/reglang/default.nix @@ -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 diff --git a/pkgs/development/coq-modules/relation-algebra/default.nix b/pkgs/development/coq-modules/relation-algebra/default.nix index 40ffbb30c7d9..d512613fad9b 100644 --- a/pkgs/development/coq-modules/relation-algebra/default.nix +++ b/pkgs/development/coq-modules/relation-algebra/default.nix @@ -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; diff --git a/pkgs/development/coq-modules/simple-io/default.nix b/pkgs/development/coq-modules/simple-io/default.nix index bb4443433e12..d2a3ae0a26df 100644 --- a/pkgs/development/coq-modules/simple-io/default.nix +++ b/pkgs/development/coq-modules/simple-io/default.nix @@ -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"; diff --git a/pkgs/development/coq-modules/ssprove/default.nix b/pkgs/development/coq-modules/ssprove/default.nix index b1a26558a0bd..b91ef56a36b7 100644 --- a/pkgs/development/coq-modules/ssprove/default.nix +++ b/pkgs/development/coq-modules/ssprove/default.nix @@ -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}"; diff --git a/pkgs/development/coq-modules/stalmarck/default.nix b/pkgs/development/coq-modules/stalmarck/default.nix index 10693a88ed0f..2da766715881 100644 --- a/pkgs/development/coq-modules/stalmarck/default.nix +++ b/pkgs/development/coq-modules/stalmarck/default.nix @@ -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="; }; diff --git a/pkgs/development/coq-modules/stdlib/default.nix b/pkgs/development/coq-modules/stdlib/default.nix index af6a262fccdc..90933aa24d75 100644 --- a/pkgs/development/coq-modules/stdlib/default.nix +++ b/pkgs/development/coq-modules/stdlib/default.nix @@ -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="; diff --git a/pkgs/development/coq-modules/stdpp/default.nix b/pkgs/development/coq-modules/stdpp/default.nix index da020725d9ff..41eaacb7fde9 100644 --- a/pkgs/development/coq-modules/stdpp/default.nix +++ b/pkgs/development/coq-modules/stdpp/default.nix @@ -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="; diff --git a/pkgs/development/rocq-modules/bignums/default.nix b/pkgs/development/rocq-modules/bignums/default.nix index b1cecb47a37c..3eced2572c69 100644 --- a/pkgs/development/rocq-modules/bignums/default.nix +++ b/pkgs/development/rocq-modules/bignums/default.nix @@ -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}"; diff --git a/pkgs/development/rocq-modules/hierarchy-builder/default.nix b/pkgs/development/rocq-modules/hierarchy-builder/default.nix index 7987c1c6373a..30be49a216e1 100644 --- a/pkgs/development/rocq-modules/hierarchy-builder/default.nix +++ b/pkgs/development/rocq-modules/hierarchy-builder/default.nix @@ -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}"; diff --git a/pkgs/development/rocq-modules/rocq-elpi/default.nix b/pkgs/development/rocq-modules/rocq-elpi/default.nix index 38415e85db37..8d27cf2e0dfc 100644 --- a/pkgs/development/rocq-modules/rocq-elpi/default.nix +++ b/pkgs/development/rocq-modules/rocq-elpi/default.nix @@ -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}"; diff --git a/pkgs/development/rocq-modules/stdlib/default.nix b/pkgs/development/rocq-modules/stdlib/default.nix index 487350b738fd..17fe604d1df4 100644 --- a/pkgs/development/rocq-modules/stdlib/default.nix +++ b/pkgs/development/rocq-modules/stdlib/default.nix @@ -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=";