coqPackages: various 8.16 -> 8.17

14 files changed, 29 insertions, 12 deletions

diff --git a/pkgs/development/coq-modules/coq-elpi/default.nix b/pkgs/development/coq-modules/coq-elpi/default.nix
index 7e7ec784c31..8b932499ca4 100644
--- a/pkgs/development/coq-modules/coq-elpi/default.nix
+++ b/pkgs/development/coq-modules/coq-elpi/default.nix
@@ -8,6 +8,7 @@ with builtins; with lib; let
     { case = "8.14"; out = { version = "1.13.7"; };}
     { case = "8.15"; out = { version = "1.15.0"; };}
     { case = "8.16"; out = { version = "1.16.5"; };}
+    { case = "8.17"; out = { version = "1.16.5"; };}
   ] {} );
 in mkCoqDerivation {
   pname = "elpi";
@@ -15,6 +16,7 @@ in mkCoqDerivation {
   owner = "LPCIC";
   inherit version;
   defaultVersion = lib.switch coq.coq-version [
+    { case = "8.17"; out = "1.17.0"; }
     { case = "8.16"; out = "1.15.6"; }
     { case = "8.15"; out = "1.14.0"; }
     { case = "8.14"; out = "1.11.2"; }
@@ -22,6 +24,7 @@ in mkCoqDerivation {
     { case = "8.12"; out = "1.8.3_8.12"; }
     { case = "8.11"; out = "1.6.3_8.11"; }
   ] null;
+  release."1.17.0".sha256     = "sha256-J8GatRKFU0ekNCG3V5dBI+FXypeHcLgC5QJYGYzFiEM=";
   release."1.15.6".sha256     = "sha256-qc0q01tW8NVm83801HHOBHe/7H1/F2WGDbKO6nCXfno=";
   release."1.15.1".sha256     = "sha256-NT2RlcIsFB9AvBhMxil4ZZIgx+KusMqDflj2HgQxsZg=";
   release."1.14.0".sha256     = "sha256:1v2p5dlpviwzky2i14cj7gcgf8cr0j54bdm9fl5iz1ckx60j6nvp";
diff --git a/pkgs/development/coq-modules/coqeal/default.nix b/pkgs/development/coq-modules/coqeal/default.nix
index 1ccbf9e82a0..65c516d3022 100644
--- a/pkgs/development/coq-modules/coqeal/default.nix
+++ b/pkgs/development/coq-modules/coqeal/default.nix
@@ -8,7 +8,7 @@
 
   inherit version;
   defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ]  [
-      { cases = [ (range "8.13" "8.16") (isGe "1.13.0") ]; out = "1.1.1"; }
+      { cases = [ (range "8.13" "8.17") (isGe "1.13.0") ]; out = "1.1.1"; }
       { cases = [ (range "8.10" "8.15") (isGe "1.12.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"; }
diff --git a/pkgs/development/coq-modules/coquelicot/default.nix b/pkgs/development/coq-modules/coquelicot/default.nix
index 922a601584d..526ba4985c9 100644
--- a/pkgs/development/coq-modules/coquelicot/default.nix
+++ b/pkgs/development/coq-modules/coquelicot/default.nix
@@ -7,7 +7,7 @@ mkCoqDerivation {
   domain = "gitlab.inria.fr";
   inherit version;
   defaultVersion = with lib.versions; lib.switch coq.coq-version [
-    { case = range "8.12" "8.16"; out = "3.3.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"; }
diff --git a/pkgs/development/coq-modules/flocq/default.nix b/pkgs/development/coq-modules/flocq/default.nix
index cf39c8211b7..3ad6f6d4781 100644
--- a/pkgs/development/coq-modules/flocq/default.nix
+++ b/pkgs/development/coq-modules/flocq/default.nix
@@ -7,10 +7,12 @@ mkCoqDerivation {
   domain = "gitlab.inria.fr";
   inherit version;
   defaultVersion = with lib.versions; lib.switch coq.coq-version [
+    { 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;
+  release."4.1.1".sha256 = "sha256-FbClxlV0ZaxITe7s9SlNbpeMNDJli+Dfh2TMrjaMtHo=";
   release."4.1.0".sha256 = "sha256:09rak9cha7q11yfqracbcq75mhmir84331h1218xcawza48rbjik";
   release."3.4.3".sha256 = "sha256-YTdWlEmFJjCcHkl47jSOgrGqdXoApJY4u618ofCaCZE=";
   release."3.4.2".sha256 = "1s37hvxyffx8ccc8mg5aba7ivfc39p216iibvd7f2cb9lniqk1pw";
diff --git a/pkgs/development/coq-modules/graph-theory/default.nix b/pkgs/development/coq-modules/graph-theory/default.nix
index cbd919c7aa6..2c9f4e4cf27 100644
--- a/pkgs/development/coq-modules/graph-theory/default.nix
+++ b/pkgs/development/coq-modules/graph-theory/default.nix
@@ -1,19 +1,21 @@
 { lib, mkCoqDerivation, coq, mathcomp-algebra, mathcomp-finmap, mathcomp-fingroup
-, hierarchy-builder, version ? null }:
+, fourcolor, hierarchy-builder, version ? null }:
 
 mkCoqDerivation {
   pname = "graph-theory";
 
   release."0.9".sha256 = "sha256-Hl3JS9YERD8QQziXqZ9DqLHKp63RKI9HxoFYWSkJQZI=";
+  release."0.9.1".sha256 = "sha256-lRRY+501x+DqNeItBnbwYIqWLDksinWIY4x/iojRNYU=";
 
   releaseRev = v: "v${v}";
 
   inherit version;
   defaultVersion = with lib.versions; lib.switch coq.coq-version [
-    { case = range "8.13" "8.16"; out = "0.9"; }
+    { case = range "8.14" "8.16"; out = "0.9.1"; }
+    { case = range "8.12" "8.12"; out = "0.9"; }
   ] null;
 
-  propagatedBuildInputs = [ mathcomp-algebra mathcomp-finmap mathcomp-fingroup hierarchy-builder ];
+  propagatedBuildInputs = [ mathcomp-algebra mathcomp-finmap mathcomp-fingroup fourcolor hierarchy-builder ];
 
   meta = with lib; {
     description = "Library of formalized graph theory results in Coq";
diff --git a/pkgs/development/coq-modules/hierarchy-builder/default.nix b/pkgs/development/coq-modules/hierarchy-builder/default.nix
index 9bcc07387b1..464ef4fc301 100644
--- a/pkgs/development/coq-modules/hierarchy-builder/default.nix
+++ b/pkgs/development/coq-modules/hierarchy-builder/default.nix
@@ -5,7 +5,7 @@ let hb = mkCoqDerivation {
   owner = "math-comp";
   inherit version;
   defaultVersion = with lib.versions; lib.switch coq.coq-version [
-    { case = range "8.15" "8.16"; out = "1.4.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"; }
diff --git a/pkgs/development/coq-modules/interval/default.nix b/pkgs/development/coq-modules/interval/default.nix
index 02a249549df..7e9ba5f838d 100644
--- a/pkgs/development/coq-modules/interval/default.nix
+++ b/pkgs/development/coq-modules/interval/default.nix
@@ -7,12 +7,14 @@ mkCoqDerivation rec {
   domain = "gitlab.inria.fr";
   inherit version;
   defaultVersion = with lib.versions; lib.switch coq.coq-version [
+    { case = range "8.12" "8.17"; out = "4.6.1"; }
     { 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;
+  release."4.6.1".sha256 = "sha256-ZZSxt8ksz0g6dl/LEido5qJXgsaxHrVLqkGUHu90+e0=";
   release."4.6.0".sha256 = "sha256-n9ECKnV0L6XYcIcbYyOJKwlbisz/RRbNW5YESHo07X0=";
   release."4.5.2".sha256 = "sha256-r0yE9pkC4EYlqsimxkdlCXevRcwKa3HGFZiUH+ueUY8=";
   release."4.5.1".sha256 = "sha256-5OxbSPdw/1FFENubulKSk6fEIEYSPCxfvMMgtgN6j6s=";
diff --git a/pkgs/development/coq-modules/mathcomp-analysis/default.nix b/pkgs/development/coq-modules/mathcomp-analysis/default.nix
index e4f198695f3..27825c0564e 100644
--- a/pkgs/development/coq-modules/mathcomp-analysis/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-analysis/default.nix
@@ -26,10 +26,10 @@ let
   defaultVersion = with versions; lib.switch [ coq.version mathcomp.version ]  [
       { cases = [ (isGe "8.14") (isGe "1.13.0") ];               out = "0.6.1"; }
       { cases = [ (isGe "8.14") (range "1.13" "1.15") ];         out = "0.5.2"; }
-      { cases = [ (isGe "8.13") (range "1.13" "1.14") ];         out = "0.5.1"; }
+      { 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") (isGe "1.12.0") ];       out = "0.3.10"; }
-      { cases = [ (range "8.11" "8.13") "1.11.0" ];              out = "0.3.4"; }
+      { cases = [ (range "8.11" "8.14") (range "1.12" "1.13") ]; out = "0.3.10"; }
+      { cases = [ (range "8.11" "8.12") "1.11.0" ];              out = "0.3.4"; }
       { 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"; }
diff --git a/pkgs/development/coq-modules/mathcomp-bigenough/default.nix b/pkgs/development/coq-modules/mathcomp-bigenough/default.nix
index a4e4a1ecbb5..97e66705998 100644
--- a/pkgs/development/coq-modules/mathcomp-bigenough/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-bigenough/default.nix
@@ -12,7 +12,7 @@ mkCoqDerivation {
   };
   inherit version;
   defaultVersion = with lib.versions; lib.switch coq.version [
-    { case = range "8.10" "8.16"; out = "1.0.1"; }
+    { case = range "8.10" "8.17"; out = "1.0.1"; }
     { case = range "8.5"  "8.14"; out = "1.0.0"; }
   ] null;
 
diff --git a/pkgs/development/coq-modules/mathcomp-finmap/default.nix b/pkgs/development/coq-modules/mathcomp-finmap/default.nix
index 551d33c9fad..749fbb70b80 100644
--- a/pkgs/development/coq-modules/mathcomp-finmap/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-finmap/default.nix
@@ -7,7 +7,7 @@ mkCoqDerivation {
   owner = "math-comp";
   inherit version;
   defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ]  [
-      { cases = [ (range "8.13" "8.16")  (isGe "1.12") ];         out = "1.5.2"; }
+      { cases = [ (range "8.13" "8.17")  (isGe "1.12") ];         out = "1.5.2"; }
       { cases = [ (isGe "8.10")          (isGe "1.11") ];         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"; }
diff --git a/pkgs/development/coq-modules/mathcomp-real-closed/default.nix b/pkgs/development/coq-modules/mathcomp-real-closed/default.nix
index b114a3f290d..cbc6b8cc711 100644
--- a/pkgs/development/coq-modules/mathcomp-real-closed/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-real-closed/default.nix
@@ -8,6 +8,7 @@ mkCoqDerivation {
   owner = "math-comp";
   inherit version;
   release = {
+    "1.1.4".sha256 = "sha256-8Hs6XfowbpeRD8RhMRf4ZJe2xf8kE0e8m7bPUzR/IM4=";
     "1.1.3".sha256 = "1vwmmnzy8i4f203i2s60dn9i0kr27lsmwlqlyyzdpsghvbr8h5b7";
     "1.1.2".sha256 = "0907x4nf7nnvn764q3x9lx41g74rilvq5cki5ziwgpsdgb98pppn";
     "1.1.1".sha256 = "0ksjscrgq1i79vys4zrmgvzy2y4ylxa8wdsf4kih63apw6v5ws6b";
@@ -18,6 +19,7 @@ mkCoqDerivation {
   };
 
   defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ]  [
+      { cases = [ (isGe "8.13")  (isGe "1.13.0") ]; out = "1.1.4"; }
       { cases = [ (isGe "8.13")  (isGe "1.12.0") ]; out = "1.1.3"; }
       { cases = [ (isGe "8.10")  (isGe "1.12.0") ]; out = "1.1.2"; }
       { cases = [ (isGe "8.7")   "1.11.0" ]; out = "1.1.1"; }
diff --git a/pkgs/development/coq-modules/mathcomp-zify/default.nix b/pkgs/development/coq-modules/mathcomp-zify/default.nix
index 86dd239ebf7..3ea78471465 100644
--- a/pkgs/development/coq-modules/mathcomp-zify/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-zify/default.nix
@@ -9,11 +9,13 @@ mkCoqDerivation rec {
 
   defaultVersion = with lib.versions;
      lib.switch [ coq.coq-version mathcomp-algebra.version ] [
+       { cases = [ (range "8.13" "8.17") (isGe "1.12") ]; out = "1.3.0+1.12+8.13"; }
        { cases = [ (range "8.13" "8.16") (isGe "1.12") ]; out = "1.1.0+1.12+8.13"; }
      ] null;
 
   release."1.0.0+1.12+8.13".sha256 = "1j533vx6lacr89bj1bf15l1a0s7rvrx4l00wyjv99aczkfbz6h6k";
   release."1.1.0+1.12+8.13".sha256 = "1plf4v6q5j7wvmd5gsqlpiy0vwlw6hy5daq2x42gqny23w9mi2pr";
+  release."1.3.0+1.12+8.13".sha256 = "sha256-ebfY8HatP4te44M6o84DSLpDCkMu4IroPCy+HqzOnTE=";
 
   propagatedBuildInputs = [ mathcomp-algebra mathcomp-ssreflect mathcomp-fingroup ];
 
diff --git a/pkgs/development/coq-modules/mathcomp/default.nix b/pkgs/development/coq-modules/mathcomp/default.nix
index 031536b7a6e..ac94c3159ba 100644
--- a/pkgs/development/coq-modules/mathcomp/default.nix
+++ b/pkgs/development/coq-modules/mathcomp/default.nix
@@ -19,6 +19,7 @@ let
   owner = "math-comp";
   withDoc = single && (args.withDoc or false);
   defaultVersion = with versions; lib.switch coq.coq-version [
+      { case = range "8.13" "8.17"; 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"; }
@@ -31,6 +32,7 @@ let
       { case = range "8.5" "8.7";   out = "1.6.4";  }
     ] null;
   release = {
+    "1.16.0".sha256 = "sha256-gXTKhRgSGeRBUnwdDezMsMKbOvxdffT+kViZ9e1gEz0=";
     "1.15.0".sha256 = "1bp0jxl35ms54s0mdqky15w9af03f3i0n06qk12k4gw1xzvwqv21";
     "1.14.0".sha256 = "07yamlp1c0g5nahkd2gpfhammcca74ga2s6qr7a3wm6y6j5pivk9";
     "1.13.0".sha256 = "0j4cz2y1r1aw79snkcf1pmicgzf8swbaf9ippz0vg99a572zqzri";
diff --git a/pkgs/development/coq-modules/multinomials/default.nix b/pkgs/development/coq-modules/multinomials/default.nix
index 19c6015ce92..24ca5f77cf3 100644
--- a/pkgs/development/coq-modules/multinomials/default.nix
+++ b/pkgs/development/coq-modules/multinomials/default.nix
@@ -9,7 +9,8 @@
 
   inherit version;
   defaultVersion =  with lib.versions; lib.switch [ coq.version mathcomp.version ] [
-      { cases = [ (isGe "8.10") (isGe "1.12.0") ];      out = "1.5.5"; }
+      { cases = [ (isGe "8.10") (isGe "1.13.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"; }
@@ -17,6 +18,7 @@
       { cases = [ "8.6"                 (range "1.6" "1.7") ];  out = "1.1"; }
     ] null;
   release = {
+    "1.5.6".sha256 = "sha256-cMixgc34T9Ic6v+tYmL49QUNpZpPV5ofaNuHqblX6oY=";
     "1.5.5".sha256 = "sha256-VdXA51vr7DZl/wT/15YYMywdD7Gh91dMP9t7ij47qNQ=";
     "1.5.4".sha256 = "0s4sbh4y88l125hdxahr56325hdhxxdmqmrz7vv8524llyv3fciq";
     "1.5.3".sha256 = "1462x40y2qydjd2wcg8r6qr8cx3xv4ixzh2h8vp9h7arylkja1qd";