6 files changed, 77 insertions, 16 deletions
diff --git a/pkgs/development/coq-modules/QuickChick/default.nix b/pkgs/development/coq-modules/QuickChick/default.nix
index 6490391eb63..fcaaaac615e 100644
--- a/pkgs/development/coq-modules/QuickChick/default.nix
+++ b/pkgs/development/coq-modules/QuickChick/default.nix
@@ -1,10 +1,11 @@
-{ lib, mkCoqDerivation, coq, ssreflect, coq-ext-lib, simple-io }:
-with lib;
-let recent = versions.isGe "8.7" coq.coq-version; in
+{ lib, mkCoqDerivation, coq, ssreflect, coq-ext-lib, simple-io, version ? null }:
+
+let recent = lib.versions.isGe "8.7" coq.coq-version; in
 mkCoqDerivation {
   pname = "QuickChick";
   owner = "QuickChick";
-  defaultVersion = with versions; switch [ coq.coq-version ssreflect.version ] [
+  inherit version;
+  defaultVersion = with lib; with versions; lib.switch [ coq.coq-version ssreflect.version ] [
       { cases = [ "8.13" pred.true  ]; out = "1.5.0"; }
       { cases = [ "8.12" pred.true  ]; out = "1.4.0"; }
       { cases = [ "8.11" pred.true  ]; out = "1.3.2"; }
@@ -29,19 +30,19 @@ mkCoqDerivation {
   release."20170512".sha256 = "033ch10i5wmqyw8j6wnr0dlbnibgfpr1vr0c07q3yj6h23xkmqpg";
   releaseRev = v: "v${v}";
 
-  preConfigure = optionalString recent
+  preConfigure = lib.optionalString recent
     "substituteInPlace Makefile --replace quickChickTool.byte quickChickTool.native";
 
   mlPlugin = true;
-  extraBuildInputs = optional recent coq.ocamlPackages.num;
+  extraBuildInputs = lib.optional recent coq.ocamlPackages.num;
   propagatedBuildInputs = [ ssreflect ]
-    ++ optionals recent [ coq-ext-lib simple-io ]
-    ++ optional  recent coq.ocamlPackages.ocamlbuild;
+    ++ lib.optionals recent [ coq-ext-lib simple-io ]
+    ++ lib.optional recent coq.ocamlPackages.ocamlbuild;
   extraInstallFlags = [ "-f Makefile.coq" ];
 
   enableParallelBuilding = false;
 
-  meta = {
+  meta = with lib; {
     description = "Randomized property-based testing plugin for Coq; a clone of Haskell QuickCheck";
     maintainers = with maintainers; [ jwiegley ];
   };
diff --git a/pkgs/development/coq-modules/VST/default.nix b/pkgs/development/coq-modules/VST/default.nix
index 5ee1df77418..1d2a1a3c05f 100644
--- a/pkgs/development/coq-modules/VST/default.nix
+++ b/pkgs/development/coq-modules/VST/default.nix
@@ -1,4 +1,16 @@
-{ lib, mkCoqDerivation, coq, compcert, version ? null }:
+{ lib, mkCoqDerivation, coq, compcert, ITree, version ? null }:
+
+# A few modules that are not built and installed by default
+#  but that may be useful to some users.
+# They depend on ITree.
+let extra_floyd_files = [
+  "ASTsize.v"
+  "io_events.v"
+  "powerlater.v"
+  "printf.v"
+  "quickprogram.v"
+  ];
+in
 
 with lib; mkCoqDerivation {
   pname = "coq${coq.coq-version}-VST";
@@ -12,9 +24,14 @@ with lib; mkCoqDerivation {
   ] null;
   release."2.8".sha256 = "sha256-cyK88uzorRfjapNQ6XgQEmlbWnDsiyLve5po1VG52q0=";
   releaseRev = v: "v${v}";
+  extraBuildInputs = [ ITree ];
   propagatedBuildInputs = [ compcert ];
 
-  preConfigure = "patchShebangs util";
+  preConfigure = ''
+    patchShebangs util
+    substituteInPlace Makefile \
+      --replace 'FLOYD_FILES=' 'FLOYD_FILES= ${toString extra_floyd_files}'
+  '';
 
   makeFlags = [
     "BITSIZE=64"
diff --git a/pkgs/development/coq-modules/category-theory/default.nix b/pkgs/development/coq-modules/category-theory/default.nix
index 339bcb9d6b0..d24cf147930 100644
--- a/pkgs/development/coq-modules/category-theory/default.nix
+++ b/pkgs/development/coq-modules/category-theory/default.nix
@@ -5,6 +5,8 @@ with lib; mkCoqDerivation {
   pname = "category-theory";
   owner = "jwiegley";
 
+  release."20210730".rev    = "d87937faaf7460bcd6985931ac36f551d67e11af";
+  release."20210730".sha256 = "04x7433yvibxknk6gy4971yzb4saa3z4dnfy9n6irhyafzlxyf0f";
   release."20190414".rev    = "706fdb4065cc2302d92ac2bce62cb59713253119";
   release."20190414".sha256 = "16lg4xs2wzbdbsn148xiacgl4wq4xwfqjnjkdhfr3w0qh1s81hay";
   release."20180709".rev    = "3b9ba7b26a64d49a55e8b6ccea570a7f32c11ead";
@@ -12,6 +14,7 @@ with lib; mkCoqDerivation {
 
   inherit version;
   defaultVersion = with versions; switch coq.coq-version [
+    { case = range "8.10" "8.13"; out = "20210730"; }
     { case = range "8.8" "8.9"; out = "20190414"; }
     { case = range "8.6" "8.7"; out = "20180709"; }
   ] null;
diff --git a/pkgs/development/coq-modules/corn/default.nix b/pkgs/development/coq-modules/corn/default.nix
index 6910f487c64..6a3ea81ca0d 100644
--- a/pkgs/development/coq-modules/corn/default.nix
+++ b/pkgs/development/coq-modules/corn/default.nix
@@ -6,10 +6,12 @@ with lib; mkCoqDerivation rec {
   defaultVersion = switch coq.coq-version [
     { case = "8.6"; out = "8.8.1"; }
     { case = (versions.range "8.7" "8.12"); out = "8.12.0"; }
+    { case = (versions.range "8.13" "8.13"); out = "c366d3f01ec1812b145117a4da940518b092d3a6"; }
   ] null;
   release = {
     "8.8.1".sha256 = "0gh32j0f18vv5lmf6nb87nr5450w6ai06rhrnvlx2wwi79gv10wp";
     "8.12.0".sha256 = "0b92vhyzn1j6cs84z2182fn82hxxj0bqq7hk6cs4awwb3vc7dkhi";
+    "c366d3f01ec1812b145117a4da940518b092d3a6".sha256 = "1wzr7mdsnf1rq7q0dvmv55vxzysy85b00ahwbs868bl7m8fk8x5b";
   };
 
   preConfigure = "patchShebangs ./configure.sh";
diff --git a/pkgs/development/coq-modules/graph-theory/default.nix b/pkgs/development/coq-modules/graph-theory/default.nix
new file mode 100644
index 00000000000..5607d342a2e
--- /dev/null
+++ b/pkgs/development/coq-modules/graph-theory/default.nix
@@ -0,0 +1,33 @@
+{ lib, mkCoqDerivation, coq, mathcomp-algebra, mathcomp-finmap
+, hierarchy-builder, version ? null }:
+
+with lib;
+
+mkCoqDerivation {
+  pname = "graph-theory";
+
+  release."0.9".sha256 = "sha256-Hl3JS9YERD8QQziXqZ9DqLHKp63RKI9HxoFYWSkJQZI=";
+
+  releaseRev = v: "v${v}";
+
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = isGe "8.13"; out = "0.9"; }
+  ] null;
+
+  propagatedBuildInputs = [ mathcomp-algebra mathcomp-finmap hierarchy-builder ];
+
+  meta = {
+    description = "Library of formalized graph theory results in Coq";
+    longDescription = ''
+      A library of formalized graph theory results, including various
+      standard results from the literature (e.g., Menger’s Theorem, Hall’s
+      Marriage Theorem, and the excluded minor characterization of
+      treewidth-two graphs) as well as some more recent results arising from
+      the study of relation algebra within the ERC CoVeCe project (e.g.,
+      soundness and completeness of an axiomatization of graph isomorphism).
+    '';
+    maintainers = with maintainers; [ siraben ];
+    license = licenses.cecill-b;
+  };
+}
diff --git a/pkgs/development/coq-modules/interval/default.nix b/pkgs/development/coq-modules/interval/default.nix
index cdb90452365..12fe66b50da 100644
--- a/pkgs/development/coq-modules/interval/default.nix
+++ b/pkgs/development/coq-modules/interval/default.nix
@@ -1,16 +1,18 @@
-{ lib, mkCoqDerivation, which, autoconf, coq, coquelicot, flocq, bignums ? null, version ? null }:
+{ lib, mkCoqDerivation, which, autoconf, coq, coquelicot, flocq, bignums ? null, gnuplot_qt, version ? null }:
 
-with lib; mkCoqDerivation {
+mkCoqDerivation rec {
   pname = "interval";
   owner = "coqinterval";
   domain = "gitlab.inria.fr";
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
-    { case = isGe "8.8" ;        out = "4.1.1"; }
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
+    { case = isGe "8.8" ;        out = "4.3.0"; }
     { 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.3.0".sha256 = "sha256-k8DLC4HYYpHeEEgXUafS8jkaECqlM+/CoYaInmUTYko=";
+  release."4.2.0".sha256 = "sha256-SD5thgpirs3wmZBICjXGpoefg9AAXyExb5t8tz3iZhE=";
   release."4.1.1".sha256 = "sha256-h2NJ6sZt1C/88v7W2xyuftEDoyRt3H6kqm5g2hc1aoU=";
   release."4.0.0".sha256 = "1hhih6zmid610l6c8z3x4yzdzw9jniyjiknd1vpkyb2rxvqm3gzp";
   release."3.4.2".sha256 = "07ngix32qarl3pjnm9d0vqc9fdrgm08gy7zp306hwxjyq7h1v7z0";
@@ -18,8 +20,11 @@ with lib; mkCoqDerivation {
   releaseRev = v: "interval-${v}";
 
   nativeBuildInputs = [ which autoconf ];
-  propagatedBuildInputs = [ bignums coquelicot flocq ];
+  propagatedBuildInputs = [ bignums coquelicot flocq ]
+    ++ lib.optionals (lib.versions.isGe "4.2.0" defaultVersion) [ gnuplot_qt ];
   useMelquiondRemake.logpath = "Interval";
+  mlPlugin = true;
+  enableParallelBuilding = true;
 
   meta = with lib; {
     description = "Tactics for simplifying the proofs of inequalities on expressions of real numbers for the Coq proof assistant";