Rebase onto e4ad989506ec7d71f7302cc3067abd82730a4beb HEAD rootfs

Signed-off-by: Alyssa Ross <hi@alyssa.is>

29 files changed, 122 insertions, 38 deletions

diff --git a/pkgs/development/coq-modules/ITree/default.nix b/pkgs/development/coq-modules/ITree/default.nix
index df41ab6e161..aee24225021 100644
--- a/pkgs/development/coq-modules/ITree/default.nix
+++ b/pkgs/development/coq-modules/ITree/default.nix
@@ -5,9 +5,10 @@ mkCoqDerivation rec {
   owner = "DeepSpec";
   inherit version;
   defaultVersion = with lib.versions; lib.switch coq.version [
-    { case = range "8.13" "8.17";  out = "5.1.1"; }
+    { case = range "8.13" "8.18";  out = "5.1.2"; }
     { case = range "8.10" "8.16";  out = "4.0.0"; }
   ] null;
+  release."5.1.2".sha256 = "sha256-uKJIjNXGWl0YS0WH52Rnr9Jz98Eo2k0X0qWB9hUYJMk=";
   release."5.1.1".sha256 = "sha256-VlmPNwaGkdWrH7Z6DGXRosGtjuuQ+FBiGcadN2Hg5pY=";
   release."5.1.0".sha256 = "sha256-ny7Mi1KgWADiFznkNJiRgD7Djc5SUclNgKOmWRxK+eo=";
   release."4.0.0".sha256 = "0h5rhndl8syc24hxq1gch86kj7mpmgr89bxp2hmf28fd7028ijsm";
diff --git a/pkgs/development/coq-modules/VST/default.nix b/pkgs/development/coq-modules/VST/default.nix
index 72d88dec6f1..150148cfe00 100644
--- a/pkgs/development/coq-modules/VST/default.nix
+++ b/pkgs/development/coq-modules/VST/default.nix
@@ -23,11 +23,12 @@ mkCoqDerivation {
   repo = "VST";
   inherit version;
   defaultVersion = with lib.versions; lib.switch coq.coq-version [
-    { case = range "8.15" "8.16"; out = "2.11.1"; }
+    { case = range "8.15" "8.17"; out = "2.12"; }
     { case = range "8.14" "8.16"; out = "2.10"; }
     { case = range "8.13" "8.15"; out = "2.9"; }
     { case = range "8.12" "8.13"; out = "2.8"; }
   ] null;
+  release."2.12".sha256 = "sha256-4HL0U4HA5/usKNXC0Dis1UZY/Hb/LRd2IGOrqrvdWkw=";
   release."2.11.1".sha256 = "sha256-unpNstZBnRT4dIqAYOv9n1J0tWJMeRuaaa2RG1U0Xs0=";
   release."2.10".sha256 = "sha256-RIxfPWoHnV1CFkpxCusoGY/LIk07TgC7wWGRP4BSq8w=";
   release."2.9".sha256 = "sha256:1adwzbl1pprrrwrm7cm493098fizxanxpv7nyfbvwdhgbhcnv6qf";
@@ -39,7 +40,7 @@ mkCoqDerivation {
   preConfigure = ''
     patchShebangs util
     substituteInPlace Makefile \
-      --replace 'COQVERSION= ' 'COQVERSION= 8.16.1 or-else 8.16.0 or-else 8.15.2 or-else 8.15.1 or-else '\
+      --replace 'COQVERSION= ' 'COQVERSION= 8.17.1 or-else 8.16.1 or-else 8.16.0 or-else 8.15.2 or-else 8.15.1 or-else '\
       --replace 'FLOYD_FILES=' 'FLOYD_FILES= ${toString extra_floyd_files}'
   '';
 
diff --git a/pkgs/development/coq-modules/coq-lsp/default.nix b/pkgs/development/coq-modules/coq-lsp/default.nix
index fc40fc9789d..7ca44f39e0e 100644
--- a/pkgs/development/coq-modules/coq-lsp/default.nix
+++ b/pkgs/development/coq-modules/coq-lsp/default.nix
@@ -7,15 +7,15 @@ mkCoqDerivation rec {
 
   useDune = true;
 
-  release."0.1.7+8.16".sha256 = "sha256-ZBxwrnnCmT5q4C7ocQ+M+aSJQNnEjeN2HFw4bzPozYs=";
-  release."0.1.7+8.17".sha256 = "sha256-f671wzGQannGjRbmBRHFKXz24BTPX7oVeHUxnv4Vd6Y=";
-  release."0.1.7+8.18".sha256 = "sha256-J+bRIzjdIPRu7DvAGVBKB43O3UJliTo8XQ87OTzsFyc=";
+  release."0.1.8+8.16".sha256 = "sha256-dEEAK5IXGjHB8D/fYJRQG/oCotoXJuWLxXB0GQlY2eo=";
+  release."0.1.8+8.17".sha256 = "sha256-TmaE+osn/yAPU1Dyni/UTd5w/L2+qyPE3H/g6IWvHLQ=";
+  release."0.1.8+8.18".sha256 = "sha256-UYmiDdbax4wxp5dLia/1t1gFyK6UELtJJvDMd5Hd14s=";
 
   inherit version;
   defaultVersion = with lib.versions; lib.switch coq.coq-version [
-    { case = isEq "8.16"; out = "0.1.7+8.16"; }
-    { case = isEq "8.17"; out = "0.1.7+8.17"; }
-    { case = isEq "8.18"; out = "0.1.7+8.18"; }
+    { case = isEq "8.16"; out = "0.1.8+8.16"; }
+    { case = isEq "8.17"; out = "0.1.8+8.17"; }
+    { case = isEq "8.18"; out = "0.1.8+8.18"; }
   ] null;
 
   nativeBuildInputs = [ makeWrapper ];
diff --git a/pkgs/development/coq-modules/coqeal/default.nix b/pkgs/development/coq-modules/coqeal/default.nix
index 0f1f84dceab..a6ef9e0b8a3 100644
--- a/pkgs/development/coq-modules/coqeal/default.nix
+++ b/pkgs/development/coq-modules/coqeal/default.nix
@@ -8,6 +8,7 @@
 
   inherit version;
   defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ]  [
+      { cases = [ (range "8.16" "8.18") (isGe "2.0.0") ]; out = "2.0.0"; }
       { cases = [ (range "8.15" "8.18") (isGe "1.15.0") ]; out = "1.1.3"; }
       { 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"; }
@@ -16,6 +17,7 @@
       { cases = [ (isGe "8.7") "1.10.0" ]; out = "1.0.3"; }
     ] null;
 
+  release."2.0.0".sha256 = "sha256-SG/KVnRJz2P+ZxkWVp1dDOnc/JVgigoexKfRUh1Y0GM";
   release."1.1.3".sha256 = "sha256-xhqWpg86xbU1GbDtXXInNCTArjjPnWZctWiiasq1ScU=";
   release."1.1.1".sha256 = "sha256-ExAdC3WuArNxS+Sa1r4x5aT7ylbCvP/BZXfkdQNAvZ8=";
   release."1.1.0".sha256 = "1vyhfna5frkkq2fl1fkg2mwzpg09k3sbzxxpyp14fjay81xajrxr";
diff --git a/pkgs/development/coq-modules/coqprime/default.nix b/pkgs/development/coq-modules/coqprime/default.nix
index af2f56475fd..9420d69cb4b 100644
--- a/pkgs/development/coq-modules/coqprime/default.nix
+++ b/pkgs/development/coq-modules/coqprime/default.nix
@@ -6,13 +6,14 @@ mkCoqDerivation {
   owner = "thery";
   inherit version;
   defaultVersion = with lib.versions; lib.switch coq.coq-version [
-    { case = range "8.14" "8.18"; out = "8.17"; }
+    { case = range "8.14" "8.18"; out = "8.18"; }
     { case = range "8.12" "8.16"; out = "8.15"; }
     { case = range "8.10" "8.11"; out = "8.10"; }
     { case = range "8.8"  "8.9";  out = "8.8"; }
     { case = "8.7";               out = "8.7.2"; }
   ] null;
 
+  release."8.18".sha256  = "sha256-KObBEYerWhIStmq90G3vs9K5LUEOfB2SPxirwLiWQ6E=";
   release."8.17".sha256  = "sha256-D878t/PijVCopRKHYqfwdNvt3arGlI8yxbK/vI6qZUY=";
   release."8.15".sha256  = "sha256:1zr2q52r08na8265019pj9spcz982ivixk6cnzk6l1srn2g328gv";
   release."8.14.1".sha256= "sha256:0dqf87xkzcpg7gglbxjyx68ad84w1w73icxgy3s7d3w563glc2p7";
diff --git a/pkgs/development/coq-modules/corn/default.nix b/pkgs/development/coq-modules/corn/default.nix
index 7a745a3df34..a33fd8b87e2 100644
--- a/pkgs/development/coq-modules/corn/default.nix
+++ b/pkgs/development/coq-modules/corn/default.nix
@@ -5,6 +5,7 @@ mkCoqDerivation rec {
   inherit version;
   defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = "8.6"; out = "8.8.1"; }
+    { case = (range "8.14" "8.18"); out = "8.18.0"; }
     { case = (range "8.11" "8.17"); out = "8.16.0"; }
     { case = (range "8.7"  "8.15"); out = "8.13.0"; }
   ] null;
@@ -13,6 +14,7 @@ mkCoqDerivation rec {
     "8.12.0".sha256 = "0b92vhyzn1j6cs84z2182fn82hxxj0bqq7hk6cs4awwb3vc7dkhi";
     "8.13.0".sha256 = "1wzr7mdsnf1rq7q0dvmv55vxzysy85b00ahwbs868bl7m8fk8x5b";
     "8.16.0".sha256 = "sha256-ZE/EEIndxHfo/9Me5NX4ZfcH0ZAQ4sRfZY7LRZfLXBQ=";
+    "8.18.0".sha256 = "sha256-ow3mfarZ1PvBGf5WLnI8LdF3E+8A6fN7cOcXHrZJLo0=";
   };
 
   preConfigure = "patchShebangs ./configure.sh";
diff --git a/pkgs/development/coq-modules/deriving/default.nix b/pkgs/development/coq-modules/deriving/default.nix
index 38151f37261..9addbedb364 100644
--- a/pkgs/development/coq-modules/deriving/default.nix
+++ b/pkgs/development/coq-modules/deriving/default.nix
@@ -7,12 +7,14 @@ mkCoqDerivation {
   owner = "arthuraa";
 
   inherit version;
-  defaultVersion = with lib.versions; lib.switch coq.coq-version [
-    { case = range "8.11" "8.18"; out = "0.1.1"; }
+  defaultVersion = with lib.versions; lib.switch [coq.coq-version ssreflect.version] [
+    { cases = [(range "8.17" "8.18") (isGe "2.0.0")] ; out = "0.2.0"; }
+    { cases = [(range "8.11" "8.18") (isLe "2.0.0")] ; out = "0.1.1"; }
   ] null;
 
   releaseRev = v: "v${v}";
 
+  release."0.2.0".sha256 = "sha256-xPsuEayHstjF0PGFJZJ+5cm0oMUrpoGLXN23op97vjM=";
   release."0.1.1".sha256 = "sha256-Gu8aInLxTXfAFE0/gWRYI046Dx3Gv1j1+gx92v/UnPI=";
   release."0.1.0".sha256 = "sha256:11crnjm8hyis1qllkks3d7r07s1rfzwvyvpijya3s6iqfh8c7xwh";
 
diff --git a/pkgs/development/coq-modules/dpdgraph/default.nix b/pkgs/development/coq-modules/dpdgraph/default.nix
index 49333b41697..dac3fb2b74d 100644
--- a/pkgs/development/coq-modules/dpdgraph/default.nix
+++ b/pkgs/development/coq-modules/dpdgraph/default.nix
@@ -8,6 +8,7 @@ mkCoqDerivation {
   repo = "coq-dpdgraph";
   inherit version;
   defaultVersion = lib.switch coq.coq-version [
+    { 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"; }
@@ -19,10 +20,9 @@ mkCoqDerivation {
     { case = "8.9";  out = "0.6.5"; }
     { case = "8.8";  out = "0.6.3"; }
     { case = "8.7";  out = "0.6.2"; }
-    { case = "8.6";  out = "0.6.1"; }
-    { case = "8.5";  out = "0.6"; }
   ] null;
 
+  release."1.0+8.18".sha256 = "sha256-z14MI1VSYzPqmF1PqDXzymXWRMYoTlQAfR/P3Pdf7fI=";
   release."1.0+8.17".sha256 = "sha256-gcvL3vseLKEF9xinT0579jXBBaA5E3rJ5KaU8RfKtm4=";
   release."1.0+8.16".sha256 = "sha256-xy4xcVHaD1OHBdGUzUy3SeZnHtOf1+UIh6YjUYFINm0=";
   release."1.0+8.15".sha256 = "sha256:1pxr0gakcz297y8hhrnssv5j07ccd58pv7rh7qv5g7855pfqrkg7";
diff --git a/pkgs/development/coq-modules/extructures/default.nix b/pkgs/development/coq-modules/extructures/default.nix
index 7240ffdf0db..bce21f0e6c6 100644
--- a/pkgs/development/coq-modules/extructures/default.nix
+++ b/pkgs/development/coq-modules/extructures/default.nix
@@ -9,6 +9,7 @@
 
   inherit version;
   defaultVersion = with lib.versions; lib.switch [coq.coq-version ssreflect.version] [
+    { cases = [(range "8.17" "8.18") (isGe "2.0.0")  ]; out = "0.4.0"; }
     { cases = [(range "8.11" "8.18") (isGe "1.12.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"; }
@@ -16,6 +17,7 @@
 
   releaseRev = v: "v${v}";
 
+  release."0.4.0".sha256 = "sha256-hItFO2XY2LTPSofPTKt3AfOEfiLliaYdzUXgDv4ea9Y=";
   release."0.3.1".sha256 = "sha256-KcuG/11Yq5ACem4FyVnQqHKvy3tNK7hd0ir2SJzzMN0=";
   release."0.3.0".sha256 = "sha256:14rm0726f1732ldds495qavg26gsn30w6dfdn36xb12g5kzavp38";
   release."0.2.2".sha256 = "sha256:1clzza73gccy6p6l95n6gs0adkqd3h4wgl4qg5l0qm4q140grvm7";
diff --git a/pkgs/development/coq-modules/fourcolor/default.nix b/pkgs/development/coq-modules/fourcolor/default.nix
index 195b73dea6f..53f98c13861 100644
--- a/pkgs/development/coq-modules/fourcolor/default.nix
+++ b/pkgs/development/coq-modules/fourcolor/default.nix
@@ -10,11 +10,13 @@ mkCoqDerivation {
   release."1.2.4".sha256 = "sha256-iSW2O1kuunvOqTolmGGXmsYTxo2MJYCdW3BnEhp6Ksg=";
   release."1.2.5".sha256 = "sha256-3qOPNCRjGK2UdHGMSqElpIXhAPVCklpeQgZwf9AFals=";
   release."1.3.0".sha256 = "sha256-h9pa6vaKT6jCEaIdEdcu0498Ou5kEXtZdb9P7WXK1DQ=";
+  release."1.3.1".sha256 = "sha256-wBizm1hJXPYBu0tHFNScQHd22FebsJYoggT5OlhY/zM=";
 
   inherit version;
   defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ] [
-    { cases = [ (isGe "8.16") (isGe "2.0") ]; out = "1.3.0"; }
-    { cases = [ (isGe "8.11") (range "1.12" "1.17") ]; out = "1.2.5"; }
+    { cases = [ (isGe "8.16") (isGe "2.0") ]; out = "1.3.1"; }
+    { cases = [ (isGe "8.16") "2.0.0" ]; out = "1.3.0"; }
+    { cases = [ (isGe "8.11") (range "1.12" "1.18") ]; 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;
diff --git a/pkgs/development/coq-modules/gappalib/default.nix b/pkgs/development/coq-modules/gappalib/default.nix
index 8406fcbd134..ffdb5193ae3 100644
--- a/pkgs/development/coq-modules/gappalib/default.nix
+++ b/pkgs/development/coq-modules/gappalib/default.nix
@@ -6,7 +6,8 @@ mkCoqDerivation {
   owner = "gappa";
   domain = "gitlab.inria.fr";
   inherit version;
-  defaultVersion = if lib.versions.range "8.8" "8.17" coq.coq-version then "1.5.3" else null;
+  defaultVersion = if lib.versions.range "8.8" "8.18" coq.coq-version then "1.5.4" else null;
+  release."1.5.4".sha256 = "sha256-9PlkXqCu4rbFD7qnMF1GSpPCVmwJ3r593RfAvkJbbdA=";
   release."1.5.3".sha256 = "sha256-SuMopX5sm4jh2uBuE7zr6vhWhHYZYnab+epjqYJqg+s=";
   release."1.5.2".sha256 = "sha256-A021Bhqz5r2CZBayfjIiWrCIfUlejcQAfbTmOaf6QTM=";
   release."1.5.1".sha256 = "1806bq1z6q5rq2ma7d5kfbqfyfr755hjg0dq7b2llry8fx9cxjsg";
diff --git a/pkgs/development/coq-modules/graph-theory/default.nix b/pkgs/development/coq-modules/graph-theory/default.nix
index 2c9f4e4cf27..0d28bbc0527 100644
--- a/pkgs/development/coq-modules/graph-theory/default.nix
+++ b/pkgs/development/coq-modules/graph-theory/default.nix
@@ -1,4 +1,4 @@
-{ lib, mkCoqDerivation, coq, mathcomp-algebra, mathcomp-finmap, mathcomp-fingroup
+{ lib, mkCoqDerivation, coq, mathcomp, mathcomp-finmap
 , fourcolor, hierarchy-builder, version ? null }:
 
 mkCoqDerivation {
@@ -6,16 +6,20 @@ mkCoqDerivation {
 
   release."0.9".sha256 = "sha256-Hl3JS9YERD8QQziXqZ9DqLHKp63RKI9HxoFYWSkJQZI=";
   release."0.9.1".sha256 = "sha256-lRRY+501x+DqNeItBnbwYIqWLDksinWIY4x/iojRNYU=";
+  release."0.9.2".sha256 = "sha256-DPYCZS8CzkfgpR+lmYhV2v20ezMtyWp8hdWpuh0OOQU=";
+  release."0.9.3".sha256 = "sha256-9WX3gsw+4btJLqcGg2W+7Qy+jaZtkfw7vCp8sXYmaWw=";
 
   releaseRev = v: "v${v}";
 
   inherit version;
-  defaultVersion = with lib.versions; lib.switch coq.coq-version [
-    { case = range "8.14" "8.16"; out = "0.9.1"; }
-    { case = range "8.12" "8.12"; out = "0.9"; }
+  defaultVersion = with lib.versions; lib.switch [ coq.coq-version mathcomp.version ] [
+    { cases = [ (isGe "8.16") (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;
 
-  propagatedBuildInputs = [ mathcomp-algebra mathcomp-finmap mathcomp-fingroup fourcolor 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/interval/default.nix b/pkgs/development/coq-modules/interval/default.nix
index 1e31323f2e3..9ac4f1c383a 100644
--- a/pkgs/development/coq-modules/interval/default.nix
+++ b/pkgs/development/coq-modules/interval/default.nix
@@ -7,6 +7,7 @@ mkCoqDerivation rec {
   domain = "gitlab.inria.fr";
   inherit version;
   defaultVersion = with lib.versions; lib.switch coq.coq-version [
+    { 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"; }
@@ -14,6 +15,8 @@ mkCoqDerivation rec {
     { case = range "8.7" "8.11"; out = "3.4.2"; }
     { case = range "8.5" "8.6";  out = "3.3.0"; }
   ] null;
+  release."4.9.0".sha256 = "sha256-+5NppyQahcc1idGu/U3B+EIWuZz2L3/oY7dIJR6pitE=";
+  release."4.8.1".sha256 = "sha256-gknZ3bA90YY2AvwfFsP5iMhohwkQ8G96mH+4st2RPDc=";
   release."4.8.0".sha256 = "sha256-YPQ1tuUgGixAVdQUJ9a3lZUNVgm2pKK3RKvl3m+/8rY=";
   release."4.7.0".sha256 = "sha256-Cel25w4BeaNqu9KAW3N2KYO2IGY0EOAK5FQ6VHBPmFQ=";
   release."4.6.1".sha256 = "sha256-ZZSxt8ksz0g6dl/LEido5qJXgsaxHrVLqkGUHu90+e0=";
diff --git a/pkgs/development/coq-modules/iris-named-props/default.nix b/pkgs/development/coq-modules/iris-named-props/default.nix
new file mode 100644
index 00000000000..c4d16775043
--- /dev/null
+++ b/pkgs/development/coq-modules/iris-named-props/default.nix
@@ -0,0 +1,17 @@
+{ lib, mkCoqDerivation, coq, version ? null, iris }:
+
+mkCoqDerivation rec {
+  pname = "iris-named-props";
+  owner = "tchajed";
+  inherit version;
+  defaultVersion = with lib.versions; lib.switch coq.version [
+    { case = range "8.16" "8.18";  out = "2023-08-14"; }
+  ] null;
+  release."2023-08-14".sha256 = "sha256-gu9qOdHO0qJ2B9Y9Vf66q08iNJcfuECJO66fizFB08g=";
+  release."2023-08-14".rev = "ca1871dd33649f27257a0fbf94076acc80ecffbc";
+  propagatedBuildInputs = [ iris ];
+  meta = {
+    description = "Named props for Iris";
+    maintainers = with lib.maintainers; [ ineol ];
+  };
+}
diff --git a/pkgs/development/coq-modules/iris/default.nix b/pkgs/development/coq-modules/iris/default.nix
index 81d9e21d8d7..30d3cb8e51d 100644
--- a/pkgs/development/coq-modules/iris/default.nix
+++ b/pkgs/development/coq-modules/iris/default.nix
@@ -6,11 +6,13 @@ mkCoqDerivation rec {
   owner = "iris";
   inherit version;
   defaultVersion = with lib.versions; lib.switch coq.coq-version [
+    { 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;
+  release."4.1.0".sha256 = "sha256-nTZUeZOXiH7HsfGbMKDE7vGrNVCkbMaWxdMWUcTUNlo=";
   release."4.0.0".sha256 = "sha256-Jc9TmgGvkiDaz9IOoExyeryU1E+Q37GN24NIM397/Gg=";
   release."3.6.0".sha256 = "sha256:02vbq597fjxd5znzxdb54wfp36412wz2d4yash4q8yddgl1kakmj";
   release."3.5.0".sha256 = "0hh14m0anfcv65rxm982ps2vp95vk9fwrpv4br8bxd9vz0091d70";
@@ -29,6 +31,6 @@ mkCoqDerivation rec {
   meta = with lib; {
     description = "The Coq development of the Iris Project";
     license = licenses.bsd3;
-    maintainers = [ maintainers.vbgl ];
+    maintainers = [ maintainers.vbgl maintainers.ineol ];
   };
 }
diff --git a/pkgs/development/coq-modules/math-classes/default.nix b/pkgs/development/coq-modules/math-classes/default.nix
index 6ae6956110a..69d65d4b558 100644
--- a/pkgs/development/coq-modules/math-classes/default.nix
+++ b/pkgs/development/coq-modules/math-classes/default.nix
@@ -5,6 +5,7 @@ mkCoqDerivation {
   pname = "math-classes";
   inherit version;
   defaultVersion = with lib.versions; lib.switch coq.coq-version [
+    { case = range "8.12" "8.18"; out = "8.18.0"; }
     { case = range "8.12" "8.17"; out = "8.17.0"; }
     { case = range "8.6"  "8.16"; out = "8.15.0"; }
   ] null;
@@ -12,6 +13,7 @@ mkCoqDerivation {
   release."8.13.0".sha256 = "1ln7ziivfbxzbdvlhbvyg3v30jgblncmwcsam6gg3d1zz6r7cbby";
   release."8.15.0".sha256 = "10w1hm537k6jx8a8vghq1yx12rsa0sjk2ipv3scgir71ln30hllw";
   release."8.17.0".sha256 = "sha256-WklL8pgYTd0l4TGt7h7tWj1qcFcXvoPn25+XKF1pIKA=";
+  release."8.18.0".sha256 = "sha256-0WwPss8+Vr37zX616xeuS4TvtImtSbToFQkQostIjO8=";
 
   propagatedBuildInputs = [ bignums ];
 
diff --git a/pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix b/pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix
index bfdd3e9b601..a665ea0db30 100644
--- a/pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix
@@ -9,12 +9,14 @@ mkCoqDerivation {
 
   defaultVersion = with lib.versions;
      lib.switch [ coq.coq-version mathcomp-algebra.version ] [
+       { cases = [ (range "8.16" "8.18") (isGe "2.0") ]; out = "1.2.2"; }
        { cases = [ (range "8.16" "8.18") (isGe "1.15") ]; out = "1.1.1"; }
        { cases = [ (range "8.13" "8.16") (isGe "1.12") ]; out = "1.0.0"; }
      ] null;
 
   release."1.0.0".sha256 = "sha256-kszARPBizWbxSQ/Iqpf2vLbxYc6AjpUCLnSNlPcNfls=";
   release."1.1.1".sha256 = "sha256-5wItMeeTRoJlRBH3zBNc2VUZn6pkDde60YAvXTx+J3U=";
+  release."1.2.2".sha256 = "sha256-EU9RJGV3BvnmsX+mGH+6+MDXiGHgDI7aP5sIYiMUXTs=";
 
   propagatedBuildInputs = [ mathcomp-algebra coq-elpi mathcomp-zify ];
 
diff --git a/pkgs/development/coq-modules/mathcomp-analysis/default.nix b/pkgs/development/coq-modules/mathcomp-analysis/default.nix
index 7e608fc61f3..5cbfbdf0c6f 100644
--- a/pkgs/development/coq-modules/mathcomp-analysis/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-analysis/default.nix
@@ -9,6 +9,8 @@ let
   repo  = "analysis";
   owner = "math-comp";
 
+  release."0.6.6".sha256 = "sha256-tWtv6yeB5/vzwpKZINK9OQ0yQsvD8qu9zVSNHvLMX5Y=";
+  release."0.6.5".sha256 = "sha256-oJk9/Jl1SWra2aFAXRAVfX7ZUaDfajqdDksYaW8dv8E=";
   release."0.6.1".sha256 = "sha256-1VyNXu11/pDMuH4DmFYSUF/qZ4Bo+/Zl3Y0JkyrH/r0=";
   release."0.6.0".sha256 = "sha256-0msICcIrK6jbOSiBu0gIVU3RHwoEEvB88CMQqW/06rg=";
   release."0.5.3".sha256 = "sha256-1NjFsi5TITF8ZWx1NyppRmi8g6YaoUtTdS9bU/sUe5k=";
@@ -24,7 +26,9 @@ let
   release."0.2.3".sha256 = "0p9mr8g1qma6h10qf7014dv98ln90dfkwn76ynagpww7qap8s966";
 
   defaultVersion = with versions; lib.switch [ coq.version mathcomp.version ]  [
-      { cases = [ (isGe "8.14") (isGe "1.13.0") ];               out = "0.6.1"; }
+      { cases = [ (isGe "8.17") (range "1.15.0" "1.18.0") ];     out = "0.6.6"; }
+      { cases = [ (isGe "8.14") (range "1.15.0" "1.17.0") ];     out = "0.6.5"; }
+      { cases = [ (isGe "8.14") (range "1.13.0" "1.16.0") ];     out = "0.6.1"; }
       { cases = [ (isGe "8.14") (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"; }
diff --git a/pkgs/development/coq-modules/mathcomp-apery/default.nix b/pkgs/development/coq-modules/mathcomp-apery/default.nix
index 69511693876..0b447909116 100644
--- a/pkgs/development/coq-modules/mathcomp-apery/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-apery/default.nix
@@ -8,7 +8,7 @@ mkCoqDerivation {
 
   inherit version;
   defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ]  [
-      { cases = [ (range "8.13" "8.16") (isGe "1.12.0") ]; out = "1.0.2"; }
+      { cases = [ (range "8.13" "8.16") (range "1.12.0" "1.17.0") ]; out = "1.0.2"; }
     ] null;
 
   release."1.0.2".sha256 = "sha256-llxyMKYvWUA7fyroG1S/jtpioAoArmarR1edi3cikcY=";
diff --git a/pkgs/development/coq-modules/mathcomp-finmap/default.nix b/pkgs/development/coq-modules/mathcomp-finmap/default.nix
index 234d25f909b..fa6032a7f08 100644
--- a/pkgs/development/coq-modules/mathcomp-finmap/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-finmap/default.nix
@@ -8,7 +8,7 @@ mkCoqDerivation {
   inherit version;
   defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ]  [
       { cases = [ (range "8.16" "8.18")  (isGe "2.0") ];          out = "2.0.0"; }
-      { cases = [ (range "8.13" "8.18")  (range "1.12" "1.17") ]; out = "1.5.2"; }
+      { cases = [ (range "8.13" "8.18")  (range "1.12" "1.18") ]; 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"; }
diff --git a/pkgs/development/coq-modules/mathcomp-infotheo/default.nix b/pkgs/development/coq-modules/mathcomp-infotheo/default.nix
index d0bb3fb54a9..a649916892a 100644
--- a/pkgs/development/coq-modules/mathcomp-infotheo/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-infotheo/default.nix
@@ -7,7 +7,7 @@ mkCoqDerivation {
   inherit version;
   defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp-analysis.version] [
     { cases = [ (isGe "8.17") (isGe "0.6.0") ];                  out = "0.5.2"; }
-    { cases = [ (range "8.15" "8.16") (range "0.5.4" "0.6.2") ]; out = "0.5.1"; }
+    { cases = [ (range "8.15" "8.16") (range "0.5.4" "0.6.5") ]; out = "0.5.1"; }
   ] null;
   release."0.5.1".sha256 = "sha256-yBBl5l+V+dggsg5KM59Yo9CULKog/xxE8vrW+ZRnX7Y=";
   release."0.5.2".sha256 = "sha256-8WAnAV53c0pMTdwj8XcUDUkLZbpUgIQbEOgOb63uHQA=";
diff --git a/pkgs/development/coq-modules/mathcomp-real-closed/default.nix b/pkgs/development/coq-modules/mathcomp-real-closed/default.nix
index cbc6b8cc711..5746c9c6387 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 = {
+    "2.0.0".sha256 = "sha256-sZvfiC5+5Lg4nRhfKKqyFzovCj2foAhqaq/w9F2bdU8=";
     "1.1.4".sha256 = "sha256-8Hs6XfowbpeRD8RhMRf4ZJe2xf8kE0e8m7bPUzR/IM4=";
     "1.1.3".sha256 = "1vwmmnzy8i4f203i2s60dn9i0kr27lsmwlqlyyzdpsghvbr8h5b7";
     "1.1.2".sha256 = "0907x4nf7nnvn764q3x9lx41g74rilvq5cki5ziwgpsdgb98pppn";
@@ -19,6 +20,7 @@ mkCoqDerivation {
   };
 
   defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ]  [
+      { cases = [ (isGe "8.16")  (isGe "2.0.0") ]; out = "2.0.0"; }
       { 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"; }
diff --git a/pkgs/development/coq-modules/mathcomp-zify/default.nix b/pkgs/development/coq-modules/mathcomp-zify/default.nix
index bbb94420ab4..bc4ed1f1f74 100644
--- a/pkgs/development/coq-modules/mathcomp-zify/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-zify/default.nix
@@ -10,7 +10,7 @@ mkCoqDerivation rec {
   defaultVersion = with lib.versions;
      lib.switch [ coq.coq-version mathcomp-algebra.version ] [
        { cases = [ (range "8.16" "8.18") (isGe "2.0.0") ]; out = "1.5.0+2.0+8.16"; }
-       { cases = [ (range "8.13" "8.18") (range "1.12" "1.17.0") ]; out = "1.3.0+1.12+8.13"; }
+       { cases = [ (range "8.13" "8.18") (range "1.12" "1.18.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;
 
diff --git a/pkgs/development/coq-modules/mathcomp/default.nix b/pkgs/development/coq-modules/mathcomp/default.nix
index 6adcb3af7d5..f95f1d425ea 100644
--- a/pkgs/development/coq-modules/mathcomp/default.nix
+++ b/pkgs/development/coq-modules/mathcomp/default.nix
@@ -19,7 +19,9 @@ let
   owner = "math-comp";
   withDoc = single && (args.withDoc or false);
   defaultVersion = with versions; lib.switch coq.coq-version [
-      { case = isGe "8.15"; out = "1.17.0"; }
+      { case = isGe "8.17"; out = "1.18.0"; }
+      { case = range "8.15" "8.18"; out = "1.17.0"; }
+      { case = range "8.16" "8.18"; out = "2.1.0"; }
       { case = range "8.16" "8.18"; out = "2.0.0"; }
       { case = range "8.13" "8.18"; out = "1.16.0"; }
       { case = range "8.14" "8.16"; out = "1.15.0"; }
@@ -34,7 +36,9 @@ let
       { case = range "8.5" "8.7";   out = "1.6.4";  }
     ] null;
   release = {
+    "2.1.0".sha256  = "sha256-XDLx0BIkVRkSJ4sGCIE51j3rtkSGemNTs/cdVmTvxqo=";
     "2.0.0".sha256  = "sha256-dpOmrHYUXBBS9kmmz7puzufxlbNpIZofpcTvJFLG5DI=";
+    "1.18.0".sha256 = "sha256-mJJ/zvM2WtmBZU3U4oid/zCMvDXei/93v5hwyyqwiiY=";
     "1.17.0".sha256 = "sha256-bUfoSTMiW/GzC1jKFay6DRqGzKPuLOSUsO6/wPSFwNg=";
     "1.16.0".sha256 = "sha256-gXTKhRgSGeRBUnwdDezMsMKbOvxdffT+kViZ9e1gEz0=";
     "1.15.0".sha256 = "1bp0jxl35ms54s0mdqky15w9af03f3i0n06qk12k4gw1xzvwqv21";
diff --git a/pkgs/development/coq-modules/multinomials/default.nix b/pkgs/development/coq-modules/multinomials/default.nix
index b11283e8c58..d2bb38f8683 100644
--- a/pkgs/development/coq-modules/multinomials/default.nix
+++ b/pkgs/development/coq-modules/multinomials/default.nix
@@ -8,9 +8,10 @@
   owner = "math-comp";
 
   inherit version;
-  defaultVersion =  with lib.versions; lib.switch [ coq.version mathcomp.version ] [
-      { cases = [ (isGe "8.16") (isGe "2.0.0") ];               out = "2.0.0"; }
-      { cases = [ (isGe "8.15") (range "1.15.0" "1.17.0") ];    out = "1.6.0"; }
+  defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ] [
+      { cases = [ (isGe "8.16") (isGe "2.1.0") ];               out = "2.1.0"; }
+      { cases = [ (isGe "8.16") "2.0.0" ];                      out = "2.0.0"; }
+      { cases = [ (isGe "8.15") (range "1.15.0" "1.18.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"; }
@@ -20,6 +21,7 @@
       { cases = [ "8.6"                 (range "1.6" "1.7") ];  out = "1.1"; }
     ] null;
   release = {
+    "2.1.0".sha256 = "sha256-QT91SBJ6DXhyg4j/okTvPP6yj2DnnPbnSlJ/p8pvZbY=";
     "2.0.0".sha256 = "sha256-2zWHzMBsO2j8EjN7CgCmKQcku9Be8aVlme0LD5p4ab8=";
     "1.6.0".sha256 = "sha256-lEM+sjqajIOm1c3lspHqcSIARgMR9RHbTQH4veHLJfU=";
     "1.5.6".sha256 = "sha256-cMixgc34T9Ic6v+tYmL49QUNpZpPV5ofaNuHqblX6oY=";
diff --git a/pkgs/development/coq-modules/reglang/default.nix b/pkgs/development/coq-modules/reglang/default.nix
index 2fc26cbfef8..fd5a37c677e 100644
--- a/pkgs/development/coq-modules/reglang/default.nix
+++ b/pkgs/development/coq-modules/reglang/default.nix
@@ -1,20 +1,22 @@
-{ lib, mkCoqDerivation, coq, ssreflect, version ? null }:
+{ lib, mkCoqDerivation, coq, mathcomp, version ? null }:
 
 mkCoqDerivation {
   pname = "reglang";
 
   releaseRev = v: "v${v}";
 
+  release."1.2.0".sha256 = "sha256-gSqQ7D2HLwM4oYopTWkMFYfYXxsH/7VxI3AyrLwNf3o=";
   release."1.1.3".sha256 = "sha256-kaselYm8K0JBsTlcI6K24m8qpv8CZ9+VNDJrOtFaExg=";
   release."1.1.2".sha256 = "sha256-SEnMilLNxh6a3oiDNGLaBr8quQ/nO2T9Fwdf/1il2Yk=";
 
   inherit version;
-  defaultVersion = with lib.versions; lib.switch coq.coq-version [
-    { case = range "8.10" "8.18"; out = "1.1.3"; }
+  defaultVersion = with lib.versions; lib.switch [ coq.coq-version mathcomp.version ] [
+    { cases = [ (range "8.16" "8.18") (isGe "2.0.0") ]; out = "1.2.0"; }
+    { cases = [ (range "8.10" "8.18") (isLt "2.0.0") ]; out = "1.1.3"; }
   ] null;
 
 
-  propagatedBuildInputs = [ ssreflect ];
+  propagatedBuildInputs = [ mathcomp.ssreflect ];
 
   meta = with lib; {
     description = "Regular Language Representations in Coq";
diff --git a/pkgs/development/coq-modules/serapi/default.nix b/pkgs/development/coq-modules/serapi/default.nix
index acb7b11c4c3..ca50f35646b 100644
--- a/pkgs/development/coq-modules/serapi/default.nix
+++ b/pkgs/development/coq-modules/serapi/default.nix
@@ -89,7 +89,7 @@ in
     then [
       ./janestreet-0.15.patch
     ]
-    else if version == "8.17.0+0.17.0"
+    else if version == "8.16.0+0.16.3" || version == "8.17.0+0.17.0"
     then [
       ./janestreet-0.16.patch
     ]
diff --git a/pkgs/development/coq-modules/stdpp/default.nix b/pkgs/development/coq-modules/stdpp/default.nix
index 4eb721e2f1c..370ab6e95f5 100644
--- a/pkgs/development/coq-modules/stdpp/default.nix
+++ b/pkgs/development/coq-modules/stdpp/default.nix
@@ -6,11 +6,13 @@ mkCoqDerivation rec {
   domain = "gitlab.mpi-sws.org";
   owner = "iris";
   defaultVersion = with lib.versions; lib.switch coq.coq-version [
+    { 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;
+  release."1.9.0".sha256 = "sha256-OXeB+XhdyzWMp5Karsz8obp0rTeMKrtG7fu/tmc9aeI=";
   release."1.8.0".sha256 = "sha256-VkIGBPHevHeHCo/Q759Q7y9WyhSF/4SMht4cOPuAXHU=";
   release."1.7.0".sha256 = "sha256:0447wbzm23f9rl8byqf6vglasfn6c1wy6cxrrwagqjwsh3i5lx8y";
   release."1.6.0".sha256 = "1l1w6srzydjg0h3f4krrfgvz455h56shyy2lbcnwdbzjkahibl7v";
@@ -27,6 +29,6 @@ mkCoqDerivation rec {
   meta = with lib; {
     description = "An extended “Standard Library” for Coq";
     license = licenses.bsd3;
-    maintainers = [ maintainers.vbgl ];
+    maintainers = [ maintainers.vbgl maintainers.ineol ];
   };
 }
diff --git a/pkgs/development/coq-modules/vcfloat/default.nix b/pkgs/development/coq-modules/vcfloat/default.nix
new file mode 100644
index 00000000000..5d1805c2573
--- /dev/null
+++ b/pkgs/development/coq-modules/vcfloat/default.nix
@@ -0,0 +1,24 @@
+{ lib, mkCoqDerivation, coq, interval, compcert, flocq, bignums, version ? null }:
+
+with lib; mkCoqDerivation {
+  pname = "vcfloat";
+  owner = "VeriNum";
+  inherit version;
+  sourceRoot = "source/vcfloat";
+  postPatch = ''
+    coq_makefile -o Makefile -f _CoqProject *.v
+  '';
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = range "8.16" "8.17"; out = "2.1.1"; }
+  ] null;
+  release."2.1.1".sha256 = "sha256-bd/XSQhyFUAnSm2bhZEZBWB6l4/Ptlm9JrWu6w9BOpw=";
+  releaseRev = v: "v${v}";
+
+  propagatedBuildInputs = [ interval compcert flocq bignums ];
+
+  meta = {
+    description = "A tool for Coq proofs about floating-point round-off error";
+    maintainers = with maintainers; [ quinn-dougherty ];
+    license = licenses.lgpl3Plus;
+  };
+}