From 3437b543fd344820710184d6593b4832e1ee73df Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= <theo.zimmermann@inria.fr>
Date: Mon, 27 Sep 2021 21:52:40 +0200
Subject: [PATCH] coq_8_14: init at 8.14+rc1

---
 pkgs/applications/science/logic/coq/default.nix        |  9 ++++++---
 pkgs/development/coq-modules/aac-tactics/default.nix   |  2 ++
 pkgs/development/coq-modules/bignums/default.nix       |  1 +
 pkgs/development/coq-modules/equations/default.nix     |  3 +++
 pkgs/development/coq-modules/fourcolor/default.nix     |  4 ++--
 pkgs/development/coq-modules/goedel/default.nix        |  2 +-
 pkgs/development/coq-modules/graph-theory/default.nix  |  2 +-
 .../coq-modules/hierarchy-builder/default.nix          |  4 ++--
 pkgs/development/coq-modules/iris/default.nix          |  4 ++--
 pkgs/development/coq-modules/itauto/default.nix        |  2 +-
 pkgs/development/coq-modules/multinomials/default.nix  |  2 +-
 pkgs/development/coq-modules/paco/default.nix          |  4 ++--
 pkgs/development/coq-modules/parsec/default.nix        |  2 +-
 pkgs/development/coq-modules/reglang/default.nix       |  2 +-
 .../coq-modules/relation-algebra/default.nix           | 10 +++++-----
 pkgs/development/coq-modules/semantics/default.nix     |  3 +--
 pkgs/development/coq-modules/stdpp/default.nix         |  4 ++--
 pkgs/top-level/all-packages.nix                        |  1 +
 pkgs/top-level/coq-packages.nix                        |  2 ++
 19 files changed, 37 insertions(+), 26 deletions(-)

diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix
index e595bf47c67c..723b67872c23 100644
--- a/pkgs/applications/science/logic/coq/default.nix
+++ b/pkgs/applications/science/logic/coq/default.nix
@@ -44,6 +44,7 @@ let
    "8.13.0".sha256     = "0sjbqmz6qcvnz0hv87xha80qbhvmmyd675wyc5z4rgr34j2l1ymd";
    "8.13.1".sha256     = "0xx2ns84mlip9bg2mkahy3pmc5zfcgrjxsviq9yijbzy1r95wf0n";
    "8.13.2".sha256     = "1884vbmwmqwn9ngibax6dhnqh4cc02l0s2ajc6jb1xgr0i60whjk";
+   "8.14+rc1".sha256   = "0jrkgj7c2959dsinw4x7q4ril1x24qq08snl25hgx33ls4sym5zb";
   };
   releaseRev = v: "V${v}";
   fetched = import ../../../../build-support/coq/meta-fetch/default.nix
@@ -163,7 +164,7 @@ self = stdenv.mkDerivation {
 
   prefixKey = "-prefix ";
 
-  buildFlags = [ "revision" "coq" "coqide" "bin/votour" ];
+  buildFlags = [ "revision" "coq" "coqide" ] ++ optional (!versionAtLeast "8.14") "bin/votour";
   enableParallelBuilding = true;
 
   createFindlibDestdir = true;
@@ -177,9 +178,11 @@ self = stdenv.mkDerivation {
     categories = "Development;Science;Math;IDE;GTK";
   });
 
-  postInstall = ''
+  postInstall = let suffix = if versionAtLeast "8.14" then "-core" else ""; in ''
     cp bin/votour $out/bin/
-    ln -s $out/lib/coq $OCAMLFIND_DESTDIR/coq
+    ln -s $out/lib/coq${suffix} $OCAMLFIND_DESTDIR/coq${suffix}
+  '' + optionalString (versionAtLeast "8.14") ''
+    ln -s $out/lib/coqide-server $OCAMLFIND_DESTDIR/coqide-server
   '' + optionalString buildIde ''
     mkdir -p "$out/share/pixmaps"
     ln -s "$out/share/coq/coq.png" "$out/share/pixmaps/"
diff --git a/pkgs/development/coq-modules/aac-tactics/default.nix b/pkgs/development/coq-modules/aac-tactics/default.nix
index 445a0422446a..c67b47f18776 100644
--- a/pkgs/development/coq-modules/aac-tactics/default.nix
+++ b/pkgs/development/coq-modules/aac-tactics/default.nix
@@ -6,6 +6,7 @@ mkCoqDerivation {
 
   releaseRev = v: "v${v}";
 
+  release."8.14.0".sha256 = "04x47ngb95m1h4jw2gl0v79s5im7qimcw7pafc34gkkf51pyhakp";
   release."8.13.0".sha256 = "sha256-MAnMc4KzC551JInrRcfKED4nz04FO0GyyyuDVRmnYTY=";
   release."8.12.0".sha256 = "sha256-dPNA19kZo/2t3rbyX/R5yfGcaEfMhbm9bo71Uo4ZwoM=";
   release."8.11.0".sha256 = "sha256-CKKMiJLltIb38u+ZKwfQh/NlxYawkafp+okY34cGCYU=";
@@ -17,6 +18,7 @@ mkCoqDerivation {
 
   inherit version;
   defaultVersion = with versions; switch coq.coq-version [
+    { case = "8.14"; out = "8.14.0"; }
     { case = "8.13"; out = "8.13.0"; }
     { case = "8.12"; out = "8.12.0"; }
     { case = "8.11"; out = "8.11.0"; }
diff --git a/pkgs/development/coq-modules/bignums/default.nix b/pkgs/development/coq-modules/bignums/default.nix
index 84dc92a3cd5f..cb83a9fdc339 100644
--- a/pkgs/development/coq-modules/bignums/default.nix
+++ b/pkgs/development/coq-modules/bignums/default.nix
@@ -8,6 +8,7 @@ with lib; mkCoqDerivation {
   defaultVersion = if versions.isGe "8.5" coq.coq-version
     then "${coq.coq-version}.0" else null;
 
+  release."8.14.0".sha256 = "0jsgdvj0ddhkls32krprp34r64y1rb5mwxl34fgaxk2k4664yq06";
   release."8.13.0".sha256 = "1n66i7hd9222b2ks606mak7m4f0dgy02xgygjskmmav6h7g2sx7y";
   release."8.12.0".sha256 = "14ijb3qy2hin3g4djx437jmnswxxq7lkfh3dwh9qvrds9a015yg8";
   release."8.11.0".sha256 = "1xcd7c7qlvs0narfba6px34zq0mz8rffnhxw0kzhhg6i4iw115dp";
diff --git a/pkgs/development/coq-modules/equations/default.nix b/pkgs/development/coq-modules/equations/default.nix
index d19d3826c742..e6d5e11fcc5f 100644
--- a/pkgs/development/coq-modules/equations/default.nix
+++ b/pkgs/development/coq-modules/equations/default.nix
@@ -6,6 +6,7 @@ with lib; mkCoqDerivation {
   repo = "Coq-Equations";
   inherit version;
   defaultVersion = switch coq.coq-version [
+    { case = "8.14"; out = "1.3-8.14"; }
     { case = "8.13"; out = "1.2.4+coq8.13"; }
     { case = "8.12"; out = "1.2.4+coq8.12"; }
     { case = "8.11"; out = "1.2.4+coq8.11"; }
@@ -43,6 +44,8 @@ with lib; mkCoqDerivation {
     release."1.2.4+coq8.12".sha256    = "1n0w8is464qcq8mk2mv7amaf0khbjz5mpc9phf0rhpjm0lb22cb3";
     release."1.2.4+coq8.13".rev       = "v1.2.4-8.13";
     release."1.2.4+coq8.13".sha256    = "0i014lshsdflzw6h0qxra9d2f0q82vffxv2f29awbb9ad0p4rq4q";
+    release."1.3-8.14".rev            = "v1.3-8.14";
+    release."1.3-8.14".sha256         = "19bj9nncd1r9g4273h5qx35gs3i4bw5z9bhjni24b413hyj55hkv";
 
   mlPlugin = true;
   preBuild = "coq_makefile -f _CoqProject -o Makefile";
diff --git a/pkgs/development/coq-modules/fourcolor/default.nix b/pkgs/development/coq-modules/fourcolor/default.nix
index 4de6e2da8b51..84cd739ed6ab 100644
--- a/pkgs/development/coq-modules/fourcolor/default.nix
+++ b/pkgs/development/coq-modules/fourcolor/default.nix
@@ -9,8 +9,8 @@ mkCoqDerivation {
   release."1.2.3".sha256 = "sha256-gwKfUa74fIP7j+2eQgnLD7AswjCtOFGHGaIWb4qI0n4=";
 
   inherit version;
-  defaultVersion = with versions; switch mathcomp.version [
-    { case = pred.inter (isGe "1.11.0") (isLt "1.13"); out = "1.2.3"; }
+  defaultVersion = with versions; switch [ coq.version mathcomp.version ] [
+    { cases = [ (isLe "8.13") (pred.inter (isGe "1.11.0") (isLt "1.13")) ]; out = "1.2.3"; }
   ] null;
 
   propagatedBuildInputs = [ mathcomp.algebra ];
diff --git a/pkgs/development/coq-modules/goedel/default.nix b/pkgs/development/coq-modules/goedel/default.nix
index f6ed9491e98c..965ae1b6ec46 100644
--- a/pkgs/development/coq-modules/goedel/default.nix
+++ b/pkgs/development/coq-modules/goedel/default.nix
@@ -10,7 +10,7 @@ mkCoqDerivation {
 
   inherit version;
   defaultVersion = with versions; switch coq.coq-version [
-    { case = isGe "8.11"; out = "8.12.0"; }
+    { case = range "8.11" "8.13"; out = "8.12.0"; }
   ] null;
 
   propagatedBuildInputs = [ hydra-battles pocklington ];
diff --git a/pkgs/development/coq-modules/graph-theory/default.nix b/pkgs/development/coq-modules/graph-theory/default.nix
index 5607d342a2eb..1ecda185cdd8 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 = isGe "8.13"; out = "0.9"; }
+    { case = isEq "8.13"; out = "0.9"; }
   ] null;
 
   propagatedBuildInputs = [ mathcomp-algebra mathcomp-finmap hierarchy-builder ];
diff --git a/pkgs/development/coq-modules/hierarchy-builder/default.nix b/pkgs/development/coq-modules/hierarchy-builder/default.nix
index 491ff959eced..aff3bc30b5b0 100644
--- a/pkgs/development/coq-modules/hierarchy-builder/default.nix
+++ b/pkgs/development/coq-modules/hierarchy-builder/default.nix
@@ -5,8 +5,8 @@ with lib; mkCoqDerivation {
   owner = "math-comp";
   inherit version;
   defaultVersion = with versions; switch coq.coq-version [
-    { case = isGe "8.12";         out = "1.1.0"; }
-    { case = range "8.11" "8.12"; out = "0.10.0"; }
+    { case = range "8.12" "8.13"; out = "1.1.0"; }
+    { case = isEq "8.11";         out = "0.10.0"; }
   ] null;
   release."1.1.0".sha256  = "sha256-spno5ty4kU4WWiOfzoqbXF8lWlNSlySWcRReR3zE/4Q=";
   release."1.0.0".sha256  = "0yykygs0z6fby6vkiaiv3azy1i9yx4rqg8xdlgkwnf2284hffzpp";
diff --git a/pkgs/development/coq-modules/iris/default.nix b/pkgs/development/coq-modules/iris/default.nix
index d2d9870f3209..c0a9e948440e 100644
--- a/pkgs/development/coq-modules/iris/default.nix
+++ b/pkgs/development/coq-modules/iris/default.nix
@@ -6,8 +6,8 @@ with lib; mkCoqDerivation rec {
   owner = "iris";
   inherit version;
   defaultVersion = with versions; switch coq.coq-version [
-    { case = isGe "8.11";        out = "3.4.0"; }
-    { case = range "8.9" "8.11"; out = "3.3.0"; }
+    { case = range "8.11" "8.13"; out = "3.4.0"; }
+    { case = range "8.9"  "8.10"; out = "3.3.0"; }
   ] null;
   release."3.4.0".sha256 = "0vdc2mdqn5jjd6yz028c0c6blzrvpl0c7apx6xas7ll60136slrb";
   release."3.3.0".sha256 = "0az4gkp5m8sq0p73dlh0r7ckkzhk7zkg5bndw01bdsy5ywj0vilp";
diff --git a/pkgs/development/coq-modules/itauto/default.nix b/pkgs/development/coq-modules/itauto/default.nix
index 66791b130614..843a99de4be6 100644
--- a/pkgs/development/coq-modules/itauto/default.nix
+++ b/pkgs/development/coq-modules/itauto/default.nix
@@ -9,7 +9,7 @@ mkCoqDerivation rec {
   release."8.13+no".sha256 = "sha256-gXoxtLcHPoyjJkt7WqvzfCMCQlh6kL2KtCGe3N6RC/A=";
   inherit version;
   defaultVersion = with versions; switch coq.coq-version [
-    { case = isGe "8.13"; out = "8.13+no"; }
+    { case = isEq "8.13"; out = "8.13+no"; }
   ] null;
 
   mlPlugin = true;
diff --git a/pkgs/development/coq-modules/multinomials/default.nix b/pkgs/development/coq-modules/multinomials/default.nix
index c7fed9ced513..306e68ac0f05 100644
--- a/pkgs/development/coq-modules/multinomials/default.nix
+++ b/pkgs/development/coq-modules/multinomials/default.nix
@@ -9,7 +9,7 @@ with lib; mkCoqDerivation {
 
   inherit version;
   defaultVersion =  with versions; switch [ coq.version mathcomp.version ] [
-      { cases = [ (range "8.10" "8.13") "1.12.0" ];             out = "1.5.4"; }
+      { cases = [ (range "8.10" "8.14") "1.12.0" ];             out = "1.5.4"; }
       { 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"; }
diff --git a/pkgs/development/coq-modules/paco/default.nix b/pkgs/development/coq-modules/paco/default.nix
index 900e52f1682b..0a8bb78eeb70 100644
--- a/pkgs/development/coq-modules/paco/default.nix
+++ b/pkgs/development/coq-modules/paco/default.nix
@@ -5,8 +5,8 @@ with lib; mkCoqDerivation {
   owner = "snu-sf";
   inherit version;
   defaultVersion = with versions; switch coq.coq-version [
-    { case = isGe "8.6";         out = "4.0.2"; }
-    { case = range "8.5" "8.8";  out = "1.2.8"; }
+    { case = range "8.6" "8.13"; out = "4.0.2"; }
+    { case = isEq "8.5";         out = "1.2.8"; }
   ] null;
   release."4.0.2".sha256 = "1q96bsxclqx84xn5vkid501jkwlc1p6fhb8szrlrp82zglj58b0b";
   release."1.2.8".sha256 = "05fskx5x1qgaf9qv626m38y5izichzzqc7g2rglzrkygbskrrwsb";
diff --git a/pkgs/development/coq-modules/parsec/default.nix b/pkgs/development/coq-modules/parsec/default.nix
index ad48809a9fed..fa1aa3c8399a 100644
--- a/pkgs/development/coq-modules/parsec/default.nix
+++ b/pkgs/development/coq-modules/parsec/default.nix
@@ -11,7 +11,7 @@ mkCoqDerivation {
   releaseRev = (v: "v${v}");
 
   inherit version;
-  defaultVersion = if versions.isGe "8.12" coq.version then "0.1.0" else null;
+  defaultVersion = if versions.range "8.12" "8.13" coq.version then "0.1.0" else null;
   release."0.1.0".sha256 = "sha256:01avfcqirz2b9wjzi9iywbhz9szybpnnj3672dgkfsimyg9jgnsr";
 
   meta = {
diff --git a/pkgs/development/coq-modules/reglang/default.nix b/pkgs/development/coq-modules/reglang/default.nix
index bc18108264a1..1908c755cd3a 100644
--- a/pkgs/development/coq-modules/reglang/default.nix
+++ b/pkgs/development/coq-modules/reglang/default.nix
@@ -10,7 +10,7 @@ mkCoqDerivation {
 
   inherit version;
   defaultVersion = with versions; switch coq.coq-version [
-    { case = range "8.10" "8.13"; out = "1.1.2"; }
+    { case = range "8.10" "8.14"; out = "1.1.2"; }
   ] null;
 
 
diff --git a/pkgs/development/coq-modules/relation-algebra/default.nix b/pkgs/development/coq-modules/relation-algebra/default.nix
index da74215d537f..01cb7f63b71a 100644
--- a/pkgs/development/coq-modules/relation-algebra/default.nix
+++ b/pkgs/development/coq-modules/relation-algebra/default.nix
@@ -15,11 +15,11 @@ mkCoqDerivation {
 
   inherit version;
   defaultVersion = with versions; switch coq.coq-version [
-    { case = isGe "8.13"; out = "1.7.5"; }
-    { case = isGe "8.12"; out = "1.7.4"; }
-    { case = isGe "8.11"; out = "1.7.3"; }
-    { case = isGe "8.10"; out = "1.7.2"; }
-    { case = isGe "8.9"; out = "1.7.1"; }
+    { 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;
 
   mlPlugin = true;
diff --git a/pkgs/development/coq-modules/semantics/default.nix b/pkgs/development/coq-modules/semantics/default.nix
index 1fb01312e666..796c9dee0a40 100644
--- a/pkgs/development/coq-modules/semantics/default.nix
+++ b/pkgs/development/coq-modules/semantics/default.nix
@@ -15,8 +15,7 @@ mkCoqDerivation rec {
 
   inherit version;
   defaultVersion = with versions; switch coq.coq-version [
-    { case = isGe "8.13"; out = "8.13.0"; }
-    { case = "8.11"; out = "8.11.1"; }
+    { case = range "8.10" "8.13"; out = "8.13.0"; }
     { case = "8.9"; out = "8.9.0"; }
     { case = "8.8"; out = "8.8.0"; }
     { case = "8.7"; out = "8.7.0"; }
diff --git a/pkgs/development/coq-modules/stdpp/default.nix b/pkgs/development/coq-modules/stdpp/default.nix
index 604a3f48f87b..d49892e3396e 100644
--- a/pkgs/development/coq-modules/stdpp/default.nix
+++ b/pkgs/development/coq-modules/stdpp/default.nix
@@ -6,8 +6,8 @@ with lib; mkCoqDerivation rec {
   domain = "gitlab.mpi-sws.org";
   owner = "iris";
   defaultVersion = with versions; switch coq.coq-version [
-    { case = isGe "8.11";        out = "1.5.0"; }
-    { case = range "8.8" "8.11"; out = "1.4.0"; }
+    { case = range "8.11" "8.13"; out = "1.5.0"; }
+    { case = range "8.8" "8.10";  out = "1.4.0"; }
   ] null;
   release."1.5.0".sha256 = "1ym0fy620imah89p8b6rii8clx2vmnwcrbwxl3630h24k42092nf";
   release."1.4.0".sha256 = "1m6c7ibwc99jd4cv14v3r327spnfvdf3x2mnq51f9rz99rffk68r";
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 53b0f9c450f4..3087a4729844 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -31068,6 +31068,7 @@ with pkgs;
     coqPackages_8_11 coq_8_11
     coqPackages_8_12 coq_8_12
     coqPackages_8_13 coq_8_13
+    coqPackages_8_14 coq_8_14
     coqPackages      coq
   ;
 
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index c785d6c16cf5..dc657ab1df5b 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -131,6 +131,7 @@ in rec {
   coq_8_11 = mkCoq "8.11";
   coq_8_12 = mkCoq "8.12";
   coq_8_13 = mkCoq "8.13";
+  coq_8_14 = mkCoq "8.14";
 
   coqPackages_8_5 = mkCoqPackages coq_8_5;
   coqPackages_8_6 = mkCoqPackages coq_8_6;
@@ -141,6 +142,7 @@ in rec {
   coqPackages_8_11 = mkCoqPackages coq_8_11;
   coqPackages_8_12 = mkCoqPackages coq_8_12;
   coqPackages_8_13 = mkCoqPackages coq_8_13;
+  coqPackages_8_14 = mkCoqPackages coq_8_14;
   coqPackages = recurseIntoAttrs coqPackages_8_13;
   coq = coqPackages.coq;