From d317484de16e4446c2771826c6eb1d853eb0297d Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Sat, 7 May 2022 07:29:17 +0200 Subject: [PATCH 1/9] coqPackages.graph-theory: enable for Coq 8.15 --- pkgs/development/coq-modules/graph-theory/default.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pkgs/development/coq-modules/graph-theory/default.nix b/pkgs/development/coq-modules/graph-theory/default.nix index eedbe6fb5d88..9ba5f03a5620 100644 --- a/pkgs/development/coq-modules/graph-theory/default.nix +++ b/pkgs/development/coq-modules/graph-theory/default.nix @@ -12,7 +12,7 @@ mkCoqDerivation { inherit version; defaultVersion = with versions; switch coq.coq-version [ - { case = range "8.13" "8.14"; out = "0.9"; } + { case = range "8.13" "8.15"; out = "0.9"; } ] null; propagatedBuildInputs = [ mathcomp-algebra mathcomp-finmap mathcomp-fingroup hierarchy-builder ]; From 4847e4382c9ae9691bf1f20d32c4c64c44a7e3b3 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Sat, 7 May 2022 07:29:25 +0200 Subject: [PATCH 2/9] coqPackages.category-theory: enable with Coq 8.15 --- pkgs/development/coq-modules/category-theory/default.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pkgs/development/coq-modules/category-theory/default.nix b/pkgs/development/coq-modules/category-theory/default.nix index ae3f7e809fb6..7cff9ddef4b9 100644 --- a/pkgs/development/coq-modules/category-theory/default.nix +++ b/pkgs/development/coq-modules/category-theory/default.nix @@ -16,7 +16,7 @@ with lib; mkCoqDerivation { inherit version; defaultVersion = with versions; switch coq.coq-version [ - { case = range "8.10" "8.14"; out = "20211213"; } + { case = range "8.10" "8.15"; out = "20211213"; } { case = range "8.8" "8.9"; out = "20190414"; } { case = range "8.6" "8.7"; out = "20180709"; } ] null; From e9d3fe8f289627ed3f224339241d7317675effc2 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Sat, 7 May 2022 07:29:30 +0200 Subject: [PATCH 3/9] coqPackages.goedel: enable with Coq 8.15 --- pkgs/development/coq-modules/goedel/default.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pkgs/development/coq-modules/goedel/default.nix b/pkgs/development/coq-modules/goedel/default.nix index c50f8672e01c..ecd154c82ed5 100644 --- a/pkgs/development/coq-modules/goedel/default.nix +++ b/pkgs/development/coq-modules/goedel/default.nix @@ -12,7 +12,7 @@ mkCoqDerivation { inherit version; defaultVersion = with versions; switch coq.coq-version [ - { case = range "8.11" "8.14"; out = "8.13.0"; } + { case = range "8.11" "8.15"; out = "8.13.0"; } ] null; propagatedBuildInputs = [ hydra-battles pocklington ]; From f393892bb369a73ff655d7336369d43fd45f06ff Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Sat, 7 May 2022 07:29:33 +0200 Subject: [PATCH 4/9] coqPackages.smtcoq: disable for Coq > 8.13 --- pkgs/development/coq-modules/smtcoq/default.nix | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pkgs/development/coq-modules/smtcoq/default.nix b/pkgs/development/coq-modules/smtcoq/default.nix index 416b8d1bb58c..0389b45fb5cd 100644 --- a/pkgs/development/coq-modules/smtcoq/default.nix +++ b/pkgs/development/coq-modules/smtcoq/default.nix @@ -9,8 +9,8 @@ mkCoqDerivation { release."itp22".sha256 = "sha256-CdPfgDfeJy8Q6ZlQeVCSR/x8ZlJ2kSEF6F5UnAespnQ="; inherit version; - defaultVersion = with versions; switch [ coq.version mathcomp.version ] [ - { cases = [ (isGe "8.13") ]; out = "itp22"; } + defaultVersion = with versions; switch coq.version [ + { case = isEq "8.13"; out = "itp22"; } ] null; propagatedBuildInputs = [ trakt cvc4 ] ++ lib.optionals (!stdenv.isDarwin) [ veriT ]; From e34f56ce98a9cfbea6703e65dd96fa7fa09fc91c Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Sat, 7 May 2022 07:29:36 +0200 Subject: [PATCH 5/9] coqPackages.itauto: init at 8.14.0 & 8.15.0 --- pkgs/development/coq-modules/itauto/default.nix | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/pkgs/development/coq-modules/itauto/default.nix b/pkgs/development/coq-modules/itauto/default.nix index af535993362a..4993a76b4f08 100644 --- a/pkgs/development/coq-modules/itauto/default.nix +++ b/pkgs/development/coq-modules/itauto/default.nix @@ -6,9 +6,13 @@ mkCoqDerivation rec { owner = "fbesson"; domain = "gitlab.inria.fr"; + release."8.15.0".sha256 = "sha256:10qpv4nx1p0wm9sas47yzsg9z22dhvizszfa21yff08a8fr0igya"; + release."8.14.0".sha256 = "sha256:1k6pqhv4dwpkwg81f2rlfg40wh070ks1gy9r0ravm2zhsbxqcfc9"; release."8.13+no".sha256 = "sha256-gXoxtLcHPoyjJkt7WqvzfCMCQlh6kL2KtCGe3N6RC/A="; inherit version; defaultVersion = with versions; switch coq.coq-version [ + { 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; From 7711b57784a0ef0e027f9bd465155a704810ec6a Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Sat, 7 May 2022 07:29:39 +0200 Subject: [PATCH 6/9] coqPackages.smpl: init at 8.14 & 8.15 --- pkgs/development/coq-modules/smpl/default.nix | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/pkgs/development/coq-modules/smpl/default.nix b/pkgs/development/coq-modules/smpl/default.nix index 63bed38ead9c..f03065cf0450 100644 --- a/pkgs/development/coq-modules/smpl/default.nix +++ b/pkgs/development/coq-modules/smpl/default.nix @@ -8,10 +8,14 @@ mkCoqDerivation { release."8.10.2".sha256 = "sha256-TUfTZKBgrSOT6piXRViHSGPE9NSj3bGx2XBIw6YCcEs="; release."8.12".sha256 = "sha256-UQbDHLVBKYk++o+Y2B6ARYRYGglytsnXhguwMatjOHg="; release."8.13".sha256 = "sha256-HxQBaIE2CjyfG4GoIXprfehqjsr/Z74YdodxMmrbzSg="; + release."8.14".sha256 = "sha256:0wmrc741j67ch4rkygjkrz5i9afi01diyyj69i24cmasvx4wad38"; + release."8.15".sha256 = "sha256:0m9xlkdhilvqb0v4q9c4hzfwffbccd6029ks39xg7qbiq6zklpvp"; releaseRev = v: "v${v}"; inherit version; defaultVersion = with versions; switch coq.version [ + { case = isEq "8.15"; out = "8.15"; } + { case = isEq "8.14"; out = "8.14"; } { case = "8.13.2"; out = "8.13"; } { case = "8.12.2"; out = "8.12"; } { case = "8.10.2"; out = "8.10.2"; } From a1cb58e4cfcd499fd08a398ba3011e223040b744 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Sat, 7 May 2022 07:29:42 +0200 Subject: [PATCH 7/9] coqPackages.semantics: enable with Coq 8.15 --- pkgs/development/coq-modules/semantics/default.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pkgs/development/coq-modules/semantics/default.nix b/pkgs/development/coq-modules/semantics/default.nix index 89567d401b22..e112512ec5c7 100644 --- a/pkgs/development/coq-modules/semantics/default.nix +++ b/pkgs/development/coq-modules/semantics/default.nix @@ -16,7 +16,7 @@ mkCoqDerivation rec { inherit version; defaultVersion = with versions; switch coq.coq-version [ - { case = range "8.10" "8.14"; out = "8.14.0"; } + { case = range "8.10" "8.15"; out = "8.14.0"; } { case = "8.9"; out = "8.9.0"; } { case = "8.8"; out = "8.8.0"; } { case = "8.7"; out = "8.7.0"; } From 38dc75293de6fab9620a736962f0177bc049af8c Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Sat, 7 May 2022 07:29:45 +0200 Subject: [PATCH 8/9] coqPackages.mathcomp-tarjan: enable with Coq 8.15 --- pkgs/development/coq-modules/mathcomp-tarjan/default.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pkgs/development/coq-modules/mathcomp-tarjan/default.nix b/pkgs/development/coq-modules/mathcomp-tarjan/default.nix index 6f82532ada30..35e9398f3ad7 100644 --- a/pkgs/development/coq-modules/mathcomp-tarjan/default.nix +++ b/pkgs/development/coq-modules/mathcomp-tarjan/default.nix @@ -9,7 +9,7 @@ with lib; mkCoqDerivation { inherit version; defaultVersion = with versions; switch [ coq.version mathcomp-ssreflect.version ] [{ - cases = [ (range "8.10" "8.14") (isGe "1.12.0") ]; out = "1.0.0"; + cases = [ (range "8.10" "8.15") (isGe "1.12.0") ]; out = "1.0.0"; }] null; release."1.0.0".sha256 = "sha256:0r459r0makshzwlygw6kd4lpvdjc43b3x5y9aa8x77f2z5gymjq1"; From a7241ea207b603f3d3515b45600c3747c71bc39c Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Sat, 7 May 2022 07:29:49 +0200 Subject: [PATCH 9/9] coq: default to 8.15 --- pkgs/top-level/all-packages.nix | 2 +- pkgs/top-level/coq-packages.nix | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index ae0c1c4f8033..e9e2529e19b6 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -12375,7 +12375,7 @@ with pkgs; comby = callPackage ../development/tools/comby { }; - compcert = coqPackages.compcert.override { version = "3.9"; }; + inherit (coqPackages) compcert; computecpp-unwrapped = callPackage ../development/compilers/computecpp {}; computecpp = wrapCCWith rec { diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix index 6af05d761c43..9c3e666c5b3b 100644 --- a/pkgs/top-level/coq-packages.nix +++ b/pkgs/top-level/coq-packages.nix @@ -160,7 +160,7 @@ in rec { coqPackages_8_13 = mkCoqPackages coq_8_13; coqPackages_8_14 = mkCoqPackages coq_8_14; coqPackages_8_15 = mkCoqPackages coq_8_15; - coqPackages = recurseIntoAttrs coqPackages_8_13; + coqPackages = recurseIntoAttrs coqPackages_8_15; coq = coqPackages.coq; }