uboot: (firmwareOdroidC2/C4) don't invoke patch tool, use patches = [] instead

https://github.com/NixOS/nixpkgs/blob/master/pkgs/stdenv/generic/setup.sh#L948 this can do it nicely. Signed-off-by: Anton Arapov <anton@deadbeef.mx>
2021-04-03 12:58:10 +02:00 · 2021-04-03 12:58:10 +02:00 · 56de2bcd43
commit 56de2bcd43
30691 changed files with 3076956 additions and 0 deletions
--- a/pkgs/development/coq-modules/Cheerios/default.nix
+++ b/pkgs/development/coq-modules/Cheerios/default.nix
@ -0,0 +1,13 @@
+{ lib, mkCoqDerivation, coq, StructTact, version ? null }:
+
+with lib; mkCoqDerivation {
+  pname   = "cheerios";
+  owner   = "uwplse";
+  inherit version;
+  defaultVersion = if versions.isGe "8.6" coq.coq-version then "20200201" else null;
+  release."20200201".rev    = "9c7f66e57b91f706d70afa8ed99d64ed98ab367d";
+  release."20200201".sha256 = "1h55s6lk47bk0lv5ralh81z55h799jbl9mhizmqwqzy57y8wqgs1";
+
+  propagatedBuildInputs = [ StructTact ];
+  preConfigure = "patchShebangs ./configure";
+}
--- a/pkgs/development/coq-modules/CoLoR/default.nix
+++ b/pkgs/development/coq-modules/CoLoR/default.nix
@ -0,0 +1,31 @@
+{ lib, mkCoqDerivation, coq, bignums, version ? null }:
+
+with lib; mkCoqDerivation {
+  pname = "color";
+  owner = "fblanqui";
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    {case = range "8.12" "8.15"; out = "1.8.2"; }
+    {case = range "8.10" "8.11"; out = "1.7.0"; }
+    {case = range "8.8"  "8.9";  out = "1.6.0"; }
+    {case = range "8.6"  "8.7";  out = "1.4.0"; }
+  ] null;
+
+  release."1.8.2".sha256 = "sha256:1gvx5cxm582793vxzrvsmhxif7px18h9xsb2jljy2gkphdmsnpqj";
+  release."1.8.1".sha256 = "0knhca9fffmyldn4q16h9265i7ih0h4jhcarq4rkn0wnn7x8w8yw";
+  release."1.7.0".rev    = "08b5481ed6ea1a5d2c4c068b62156f5be6d82b40";
+  release."1.7.0".sha256 = "1w7fmcpf0691gcwq00lm788k4ijlwz3667zj40j5jjc8j8hj7cq3";
+  release."1.6.0".rev    = "328aa06270584b578edc0d2925e773cced4f14c8";
+  release."1.6.0".sha256 = "07sy9kw1qlynsqy251adgi8b3hghrc9xxl2rid6c82mxfsp329sd";
+  release."1.4.0".rev    = "168c6b86c7d3f87ee51791f795a8828b1521589a";
+  release."1.4.0".sha256 = "1d2whsgs3kcg5wgampd6yaqagcpmzhgb6a0hp6qn4lbimck5dfmm";
+
+  propagatedBuildInputs = [ bignums ];
+  enableParallelBuilding = false;
+
+  meta = {
+    homepage = "https://github.com/fblanqui/color";
+    description = "CoLoR is a library of formal mathematical definitions and proofs of theorems on rewriting theory and termination whose correctness has been mechanically checked by the Coq proof assistant.";
+    maintainers = with maintainers; [ jpas jwiegley ];
+  };
+}
--- a/pkgs/development/coq-modules/HoTT/default.nix
+++ b/pkgs/development/coq-modules/HoTT/default.nix
@ -0,0 +1,48 @@
+{ lib, mkCoqDerivation, autoconf, automake, coq, version ? null }:
+
+with lib; mkCoqDerivation {
+  pname = "HoTT";
+  owner = "HoTT";
+  inherit version;
+  defaultVersion = if coq.coq-version == "8.6" then "20170921" else null;
+  release."20170921".rev    = "e3557740a699167e6adb1a65855509d55a392fa1";
+  release."20170921".sha256 = "0zwfp8g62b50vmmbb2kmskj3v6w7qx1pbf43yw0hr7asdz2zbx5v";
+
+  nativeBuildInputs = [ autoconf automake ];
+
+  preConfigure = ''
+    patchShebangs ./autogen.sh
+    ./autogen.sh
+
+    mkdir -p "$out/bin"
+  '';
+
+  configureFlags = [
+    "--bindir=$(out)/bin"
+  ];
+
+  patchPhase = ''
+    patchShebangs etc
+    patchShebangs hoqc hoqchk hoqdep hoqide hoqtop
+  '';
+
+  postBuild = ''
+    patchShebangs hoq-config
+  '';
+
+  # Currently, all the scripts like hoqc and hoqtop assume that the *.vo files are
+  # either (1) in the same directory as the scripts, or (2) in /usr/share/hott.
+  # We fulfill (1), which means that these files are only accessible via hoqtop,
+  # hoqc, etc and not via coqtop, coqc, etc.
+  postInstall = ''
+    mv $out/share/hott/* "$out/bin"
+    rmdir $out/share/hott
+    rmdir $out/share
+  '';
+
+  meta = {
+    homepage = "http://homotopytypetheory.org/";
+    description = "Homotopy type theory";
+    maintainers = with maintainers; [ siddharthist ];
+  };
+}
--- a/pkgs/development/coq-modules/ITree/default.nix
+++ b/pkgs/development/coq-modules/ITree/default.nix
@ -0,0 +1,17 @@
+{ lib, mkCoqDerivation, coq, version ? null , paco, coq-ext-lib }:
+
+with lib; mkCoqDerivation rec {
+  pname = "InteractionTrees";
+  owner = "DeepSpec";
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = range "8.10" "8.15";  out = "4.0.0"; }
+  ] null;
+  release."4.0.0".sha256 = "0h5rhndl8syc24hxq1gch86kj7mpmgr89bxp2hmf28fd7028ijsm";
+  releaseRev = v: "${v}";
+  propagatedBuildInputs = [ coq-ext-lib paco ];
+  meta = {
+    description = "A Library for Representing Recursive and Impure Programs in Coq";
+    maintainers = with maintainers; [ larsr ];
+  };
+}
--- a/pkgs/development/coq-modules/InfSeqExt/default.nix
+++ b/pkgs/development/coq-modules/InfSeqExt/default.nix
@ -0,0 +1,11 @@
+{ lib, mkCoqDerivation, coq, version ? null }:
+
+mkCoqDerivation {
+  pname = "InfSeqExt";
+  owner = "DistributedComponents";
+  inherit version;
+  defaultVersion = if lib.versions.isGe "8.5" coq.coq-version then "20200131" else null;
+  release."20200131".rev    = "203d4c20211d6b17741f1fdca46dbc091f5e961a";
+  release."20200131".sha256 = "0xylkdmb2dqnnqinf3pigz4mf4zmczcbpjnn59g5g76m7f2cqxl0";
+  preConfigure = "patchShebangs ./configure";
+}
--- a/pkgs/development/coq-modules/LibHyps/default.nix
+++ b/pkgs/development/coq-modules/LibHyps/default.nix
@ -0,0 +1,21 @@
+{ lib, mkCoqDerivation, coq, version ? null }:
+
+with lib;
+mkCoqDerivation {
+  pname = "LibHyps";
+  owner = "Matafou";
+  inherit version;
+  defaultVersion = if (versions.range "8.11" "8.15") coq.version then "2.0.4.1" else null;
+  release = {
+    "2.0.4.1".sha256 = "09p89701zhrfdmqlpxw3mziw8yylj1w1skb4b0xpbdwd1vsn4k3h";
+  };
+
+  configureScript = "./configure.sh";
+
+  releaseRev = (v: "libhyps-${v}");
+
+  meta = {
+    description = "Hypotheses manipulation library";
+    license = licenses.mit;
+  };
+}
--- a/pkgs/development/coq-modules/QuickChick/default.nix
+++ b/pkgs/development/coq-modules/QuickChick/default.nix
@ -0,0 +1,57 @@
+{ 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";
+  inherit version;
+  defaultVersion = with lib; with versions; lib.switch [ coq.coq-version ssreflect.version ] [
+      { cases = [ (isGe "8.13") pred.true  ]; out = "1.6.2"; }
+      { 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"; }
+      { cases = [ "8.10" pred.true  ]; out = "1.2.1"; }
+      { cases = [ "8.9"  pred.true  ];  out = "1.1.0"; }
+      { cases = [ "8.8"  pred.true  ];  out = "20190311"; }
+      { cases = [ "8.7"  isLe "1.8" ];  out = "1.0.0"; }
+      { cases = [ "8.6"  pred.true  ];  out = "20171102"; }
+      { cases = [ "8.5"  pred.true  ];  out = "20170512"; }
+    ] null;
+  release."1.6.2".sha256    = "0g5q9zw3xd4zndihq96nxkq4w3dh05418wzlwdk1nnn3b6vbx6z0";
+  release."1.5.0".sha256    = "1lq8x86vd3vqqh2yq6hvyagpnhfq5wmk5pg2z0xq7b7dcw7hyfkw";
+  release."1.4.0".sha256    = "068p48pm5yxjc3yv8qwzp25bp9kddvxj81l31mjkyx3sdrsw3kyc";
+  release."1.3.2".sha256    = "0lciwaqv288dh2f13xk2x0lrn6zyrkqy6g4yy927wwzag2gklfrs";
+  release."1.2.1".sha256    = "17vz88xjzxh3q7hs6hnndw61r3hdfawxp5awqpgfaxx4w6ni8z46";
+  release."1.1.0".sha256    = "1c34v1k37rk7v0xk2czv5n79mbjxjrm6nh3llg2mpfmdsqi68wf3";
+  release."1.0.0".sha256    = "1gqy9a4yavd0sa7kgysf9gf2lq4p8dmn4h89y8081f2j8zli0w5y";
+  release."20190311".rev    = "22af9e9a223d0038f05638654422e637e863b355";
+  release."20190311".sha256 = "00rnr19lg6lg0haq1sy4ld38p7imzand6fc52fvfq27gblxkp2aq";
+  release."20171102".rev    = "0fdb769e1dc87a278383b44a9f5102cc7ccbafcf";
+  release."20171102".sha256 = "0fri4nih40vfb0fbr82dsi631ydkw48xszinq43lyinpknf54y17";
+  release."20170512".rev    = "31eb050ae5ce57ab402db9726fb7cd945a0b4d03";
+  release."20170512".sha256 = "033ch10i5wmqyw8j6wnr0dlbnibgfpr1vr0c07q3yj6h23xkmqpg";
+  releaseRev = v: "v${v}";
+
+  preConfigure = lib.optionalString recent
+    "substituteInPlace Makefile --replace quickChickTool.byte quickChickTool.native";
+
+  mlPlugin = true;
+  nativeBuildInputs = lib.optional recent coq.ocamlPackages.ocamlbuild;
+  propagatedBuildInputs = [ ssreflect ]
+    ++ lib.optionals recent [ coq-ext-lib simple-io ];
+  extraInstallFlags = [ "-f Makefile.coq" ];
+
+  enableParallelBuilding = false;
+
+  meta = with lib; {
+    description = "Randomized property-based testing plugin for Coq; a clone of Haskell QuickCheck";
+    maintainers = with maintainers; [ jwiegley ];
+  };
+}).overrideAttrs (o:
+  let after_1_6 = lib.versions.isGe "1.6" o.version || o.version == "dev";
+  in {
+    nativeBuildInputs = o.nativeBuildInputs
+    ++ lib.optional after_1_6 coq.ocamlPackages.cppo;
+    propagatedBuildInputs = o.propagatedBuildInputs
+    ++ lib.optionals after_1_6 (with coq.ocamlPackages; [ findlib zarith ]);
+})
--- a/pkgs/development/coq-modules/StructTact/default.nix
+++ b/pkgs/development/coq-modules/StructTact/default.nix
@ -0,0 +1,16 @@
+{ lib, mkCoqDerivation, coq, version ? null }:
+
+with lib; mkCoqDerivation {
+  pname = "StructTact";
+  owner = "uwplse";
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = range "8.6" "8.15"; out = "20210328"; }
+    { case = range "8.5" "8.13"; out = "20181102"; }
+  ] null;
+  release."20210328".rev =    "179bd5312e9d8b63fc3f4071c628cddfc496d741";
+  release."20210328".sha256 = "sha256:1y5r1zm3hli10ah6lnj7n8hxad6rb6rgldd0g7m2fjibzvwqzhdg";
+  release."20181102".rev =    "82a85b7ec07e71fa6b30cfc05f6a7bfb09ef2510";
+  release."20181102".sha256 = "08zry20flgj7qq37xk32kzmg4fg6d4wi9m7pf9aph8fd3j2a0b5v";
+  preConfigure = "patchShebangs ./configure";
+}
--- a/pkgs/development/coq-modules/VST/default.nix
+++ b/pkgs/development/coq-modules/VST/default.nix
@ -0,0 +1,63 @@
+{ lib, mkCoqDerivation, coq, compcert, ITree, version ? null }:
+
+with lib;
+
+# 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"
+  ]
+  # floyd/printf.v is broken in VST 2.9
+  ++ optional (!versions.isGe "8.13" coq.coq-version) "printf.v"
+  ++ [
+  "quickprogram.v"
+  ];
+in
+
+mkCoqDerivation {
+  pname = "coq${coq.coq-version}-VST";
+  namePrefix = [];
+  displayVersion = { coq = false; };
+  owner = "PrincetonUniversity";
+  repo = "VST";
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = range "8.13" "8.15"; out = "2.9"; }
+    { case = range "8.12" "8.13"; out = "2.8"; }
+  ] null;
+  release."2.9".sha256 = "sha256:1adwzbl1pprrrwrm7cm493098fizxanxpv7nyfbvwdhgbhcnv6qf";
+  release."2.8".sha256 = "sha256-cyK88uzorRfjapNQ6XgQEmlbWnDsiyLve5po1VG52q0=";
+  releaseRev = v: "v${v}";
+  buildInputs = [ ITree ];
+  propagatedBuildInputs = [ compcert ];
+
+  preConfigure = ''
+    patchShebangs util
+    substituteInPlace Makefile \
+      --replace 'COQVERSION= ' 'COQVERSION= 8.15.2 or-else 8.15.1 or-else '\
+      --replace 'FLOYD_FILES=' 'FLOYD_FILES= ${toString extra_floyd_files}'
+  '';
+
+  makeFlags = [
+    "BITSIZE=64"
+    "COMPCERT=inst_dir"
+    "COMPCERT_INST_DIR=${compcert.lib}/lib/coq/${coq.coq-version}/user-contrib/compcert"
+    "INSTALLDIR=$(out)/lib/coq/${coq.coq-version}/user-contrib/VST"
+  ];
+
+  postInstall = ''
+    for d in msl veric floyd sepcomp progs64
+    do
+      cp -r $d $out/lib/coq/${coq.coq-version}/user-contrib/VST/
+    done
+  '';
+
+  meta = {
+    description = "Verified Software Toolchain";
+    homepage = "https://vst.cs.princeton.edu/";
+    inherit (compcert.meta) platforms;
+  };
+}
--- a/pkgs/development/coq-modules/Velisarios/default.nix
+++ b/pkgs/development/coq-modules/Velisarios/default.nix
@ -0,0 +1,19 @@
+{ lib, mkCoqDerivation, coq, version ? null }:
+
+with lib; mkCoqDerivation {
+  pname = "Velisarios";
+  owner = "vrahli";
+  inherit version;
+  defaultVersion = if versions.range "8.6" "8.8" coq.coq-version then "20180221" else null;
+
+  release."20180221".rev    = "e1eee1f10d5d46331a560bd8565ac101229d0d6b";
+  release."20180221".sha256 = "0l9885nxy0n955fj1gnijlxl55lyxiv9yjfmz8hmfrn9hl8vv1m2";
+  mlPlugin = true;
+
+  buildPhase = "make -j$NIX_BUILD_CORES";
+  preBuild = "./create-makefile.sh";
+  installPhase = ''
+    mkdir -p $out/lib/coq/${coq.coq-version}/Velisarios
+    cp -pR model/*.vo $out/lib/coq/${coq.coq-version}/Velisarios
+  '';
+}
--- a/pkgs/development/coq-modules/Verdi/default.nix
+++ b/pkgs/development/coq-modules/Verdi/default.nix
@ -0,0 +1,25 @@
+{ lib, mkCoqDerivation, coq, Cheerios, InfSeqExt, ssreflect, version ? null }:
+
+
+with lib; mkCoqDerivation {
+  pname = "verdi";
+  owner = "uwplse";
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = range "8.7" "8.15"; out = "20211026"; }
+    { case = range "8.7" "8.14"; out = "20210524"; }
+    { case = range "8.7" "8.13"; out = "20200131"; }
+    { case = "8.6"; out = "20181102"; }
+  ] null;
+  release."20211026".rev    = "064cc4fb2347453bf695776ed820ffb5fbc1d804";
+  release."20211026".sha256 = "sha256:13xrcyzay5sjszf5lg4s44wl9nrcz22n6gi4h95pkpj0ni5clinx";
+  release."20210524".rev    = "54597d8ac7ab7dd4dae683f651237644bf77701e";
+  release."20210524".sha256 = "sha256:05wb0km2jkhvi8807glxk9fi1kll4lwisiyzkxhqvymz4x6v8xqv";
+  release."20200131".rev    = "fdb4ede19d2150c254f0ebcfbed4fb9547a734b0";
+  release."20200131".sha256 = "1a2k19f9q5k5djbxplqmmpwck49kw3lrm3aax920h4yb40czkd8m";
+  release."20181102".rev    = "25b79cf1be5527ab8dc1b8314fcee93e76a2e564";
+  release."20181102".sha256 = "1vw47c37k5vaa8vbr6ryqy8riagngwcrfmb3rai37yi9xhdqg55z";
+
+  propagatedBuildInputs = [ Cheerios InfSeqExt ssreflect ];
+  preConfigure = "patchShebangs ./configure";
+}
--- a/pkgs/development/coq-modules/aac-tactics/default.nix
+++ b/pkgs/development/coq-modules/aac-tactics/default.nix
@ -0,0 +1,52 @@
+{ lib, mkCoqDerivation, coq, version ? null }:
+with lib;
+
+mkCoqDerivation {
+  pname = "aac-tactics";
+
+  releaseRev = v: "v${v}";
+
+  release."8.15.1".sha256 = "sha256:0k2sl3ns897a5ll11bazgpv4ppgi1vmx4n89v2dnxabm5dglyglp";
+  release."8.14.1".sha256 = "sha256:1w99jgm7mxwdxnalxhralmhmpwwbd52pbbifq0mx13ixkv6iqm1a";
+  release."8.14.0".sha256 = "04x47ngb95m1h4jw2gl0v79s5im7qimcw7pafc34gkkf51pyhakp";
+  release."8.13.2".sha256 = "sha256-MAnMc4KzC551JInrRcfKED4nz04FO0GyyyuDVRmnYTa=";
+  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=";
+  release."8.10.0".sha256 = "sha256-Ny3AgfLAzrz3FnoUqejXLApW+krlkHBmYlo3gAG0JsM=";
+  release."8.9.0".sha256 = "sha256-6Pp0dgYEnVaSnkJR/2Cawt5qaxWDpBI4m0WAbQboeWY=";
+  release."8.8.0".sha256 = "sha256-mwIKp3kf/6i9IN3cyIWjoRtW8Yf8cc3MV744zzFM3u4=";
+  release."8.6.1".sha256 = "sha256-PfovQ9xJnzr0eh/tO66yJ3Yp7A5E1SQG46jLIrrbZFg=";
+  release."8.5.0".sha256 = "sha256-7yNxJn6CH5xS5w/zsXfcZYORa6e5/qS9v8PUq2o02h4=";
+
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = "8.15"; out = "8.15.1"; }
+    { case = "8.14"; out = "8.14.1"; }
+    { case = "8.13"; out = "8.13.2"; }
+    { case = "8.12"; out = "8.12.0"; }
+    { case = "8.11"; out = "8.11.0"; }
+    { case = "8.10"; out = "8.10.0"; }
+    { case = "8.9"; out = "8.9.0"; }
+    { case = "8.8"; out = "8.8.0"; }
+    { case = "8.6"; out = "8.6.1"; }
+    { case = "8.5"; out = "8.5.0"; }
+  ] null;
+
+  mlPlugin = true;
+
+  meta = {
+    description = "Coq plugin providing tactics for rewriting universally quantified equations";
+    longDescription = ''
+      This Coq plugin provides tactics for rewriting universally quantified
+      equations, modulo associativity and commutativity of some operator.
+      The tactics can be applied for custom operators by registering the
+      operators and their properties as type class instances. Many common
+      operator instances, such as for Z binary arithmetic and booleans, are
+      provided with the plugin.
+    '';
+    maintainers = with maintainers; [ siraben ];
+    license = licenses.gpl3Plus;
+    platforms = platforms.unix;
+  };
+}
--- a/pkgs/development/coq-modules/addition-chains/default.nix
+++ b/pkgs/development/coq-modules/addition-chains/default.nix
@ -0,0 +1,36 @@
+{ lib, mkCoqDerivation, coq, mathcomp-ssreflect, mathcomp-algebra, mathcomp-fingroup, paramcoq
+, version ? null }:
+with lib;
+
+mkCoqDerivation {
+  pname = "addition-chains";
+  repo = "hydra-battles";
+
+  release."0.4".sha256 = "1f7pc4w3kir4c9p0fjx5l77401bx12y72nmqxrqs3qqd3iynvqlp";
+  release."0.5".sha256 = "121pcbn6v59l0c165ha9n00whbddpy11npx2y9cn7g879sfk2nqk";
+  release."0.6".sha256 = "1dri4sisa7mhclf8w4kw7ixs5zxm8xyjr034r1377p96rdk3jj0j";
+  releaseRev = (v: "v${v}");
+
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = range "8.13" "8.15"; out = "0.6"; }
+    { case = range "8.11" "8.12"; out = "0.4"; }
+  ] null;
+
+  propagatedBuildInputs = [ mathcomp-ssreflect mathcomp-algebra mathcomp-fingroup paramcoq ];
+
+  useDune2 = true;
+
+  meta = {
+    description = "Exponentiation algorithms following addition chains";
+    longDescription = ''
+      Addition chains are algorithms for computations of the p-th
+      power of some x, with the least number of multiplication as
+      possible. We present a few implementations of addition chains,
+      with proofs of their correctness.
+    '';
+    maintainers = with maintainers; [ Zimmi48 ];
+    license = licenses.mit;
+    platforms = platforms.unix;
+  };
+}
--- a/pkgs/development/coq-modules/autosubst/default.nix
+++ b/pkgs/development/coq-modules/autosubst/default.nix
@ -0,0 +1,23 @@
+{ lib, mkCoqDerivation, coq, mathcomp-ssreflect, version ? null }:
+with lib;
+
+mkCoqDerivation {
+  pname = "autosubst";
+
+  release."1.7".rev    = "v1.7";
+  release."1.7".sha256 = "sha256-qoyteQ5W2Noxf12uACOVeHhPLvgmTzrvEo6Ts+FKTGI=";
+
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = isGe "8.10"; out = "1.7"; }
+  ] null;
+
+  propagatedBuildInputs = [ mathcomp-ssreflect ];
+
+  meta = {
+    homepage = "https://www.ps.uni-saarland.de/autosubst/";
+    description = "Automation for de Bruijn syntax and substitution in Coq";
+    maintainers = with maintainers; [ siraben jwiegley ];
+    license = licenses.mit;
+  };
+}
--- a/pkgs/development/coq-modules/bignums/default.nix
+++ b/pkgs/development/coq-modules/bignums/default.nix
@ -0,0 +1,27 @@
+{ lib, mkCoqDerivation, coq, version ? null }:
+
+with lib; mkCoqDerivation {
+  pname = "bignums";
+  owner = "coq";
+  displayVersion = { bignums = ""; };
+  inherit version;
+  defaultVersion = if versions.isGe "8.6" coq.coq-version
+    then "${coq.coq-version}.0" else null;
+
+  release."8.15.0".sha256 = "093klwlhclgyrba1iv18dyz1qp5f0lwiaa7y0qwvgmai8rll5fns";
+  release."8.14.0".sha256 = "0jsgdvj0ddhkls32krprp34r64y1rb5mwxl34fgaxk2k4664yq06";
+  release."8.13.0".sha256 = "1n66i7hd9222b2ks606mak7m4f0dgy02xgygjskmmav6h7g2sx7y";
+  release."8.12.0".sha256 = "14ijb3qy2hin3g4djx437jmnswxxq7lkfh3dwh9qvrds9a015yg8";
+  release."8.11.0".sha256 = "1xcd7c7qlvs0narfba6px34zq0mz8rffnhxw0kzhhg6i4iw115dp";
+  release."8.10.0".sha256 = "0bpb4flckn4nqxbs3wjiznyx1k7r8k93qdigp3qwmikp2lxvcbw5";
+  release."8.9.0".sha256  = "03qz1w2xb2j5p06liz5yyafl0fl9vprcqm6j0iwi7rxwghl00p01";
+  release."8.8.0".sha256  = "1ymxyrvjygscxkfj3qkq66skl3vdjhb670rzvsvgmwrjkrakjnfg";
+  release."8.7.0".sha256  = "11c4sdmpd3l6jjl4v6k213z9fhrmmm1xnly3zmzam1wrrdif4ghl";
+  release."8.6.0".rev     = "v8.6.0";
+  release."8.6.0".sha256  = "0553pcsy21cyhmns6k9qggzb67az8kl31d0lwlnz08bsqswigzrj";
+  releaseRev = v: "V${v}";
+
+  mlPlugin = true;
+
+  meta = { license = licenses.lgpl2; };
+}
--- a/pkgs/development/coq-modules/category-theory/default.nix
+++ b/pkgs/development/coq-modules/category-theory/default.nix
@ -0,0 +1,31 @@
+{ lib, mkCoqDerivation, coq, ssreflect, equations, version ? null }:
+
+with lib; mkCoqDerivation {
+
+  pname = "category-theory";
+  owner = "jwiegley";
+
+  release."20211213".rev    = "449e30e929d56f6f90c22af2c91ffcc4d79837be";
+  release."20211213".sha256 = "sha256:0vgfmph5l1zn6j4b851rcm43s8y9r83swsz07rpzhmfg34pk0nl0";
+  release."20210730".rev    = "d87937faaf7460bcd6985931ac36f551d67e11af";
+  release."20210730".sha256 = "04x7433yvibxknk6gy4971yzb4saa3z4dnfy9n6irhyafzlxyf0f";
+  release."20190414".rev    = "706fdb4065cc2302d92ac2bce62cb59713253119";
+  release."20190414".sha256 = "16lg4xs2wzbdbsn148xiacgl4wq4xwfqjnjkdhfr3w0qh1s81hay";
+  release."20180709".rev    = "3b9ba7b26a64d49a55e8b6ccea570a7f32c11ead";
+  release."20180709".sha256 = "0f2nr8dgn1ab7hr7jrdmr1zla9g9h8216q4yf4wnff9qkln8sbbs";
+
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { 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;
+
+  mlPlugin = true;
+  propagatedBuildInputs = [ ssreflect equations ];
+
+  meta = {
+    description = "A formalization of category theory in Coq for personal study and practical work";
+    maintainers = with maintainers; [ jwiegley ];
+  };
+}
--- a/pkgs/development/coq-modules/ceres/default.nix
+++ b/pkgs/development/coq-modules/ceres/default.nix
@ -0,0 +1,19 @@
+{ lib, mkCoqDerivation, coq, version ? null }:
+
+with lib;
+mkCoqDerivation {
+
+  pname = "ceres";
+  repo = "coq-ceres";
+  owner = "Lysxia";
+
+  inherit version;
+  defaultVersion = if versions.isGe "8.8" coq.version then "0.4.0" else null;
+  release."0.4.0".sha256 = "sha256:0zwp3pn6fdj0qdig734zdczrls886al06mxqhhabms0jvvqijmbi";
+
+  meta = {
+    description = "Library for serialization to S-expressions";
+    license = licenses.mit;
+    maintainers = with maintainers; [ Zimmi48 ];
+  };
+}
--- a/pkgs/development/coq-modules/compcert/default.nix
+++ b/pkgs/development/coq-modules/compcert/default.nix
@ -0,0 +1,141 @@
+{ lib, fetchzip, mkCoqDerivation
+, coq, flocq, compcert
+, ocamlPackages, fetchpatch, makeWrapper, coq2html
+, stdenv, tools ? stdenv.cc
+, version ? null
+}:
+
+with lib;
+
+let compcert = mkCoqDerivation rec {
+
+  pname = "compcert";
+  owner = "AbsInt";
+
+  inherit version;
+  releaseRev = v: "v${v}";
+
+  defaultVersion =  with versions; switch coq.version [
+      { case = range "8.13" "8.15"; out = "3.10"; }
+      { case = isEq "8.12"       ; out = "3.9"; }
+      { case = range "8.8" "8.11"; out = "3.8"; }
+    ] null;
+
+  release = {
+    "3.8".sha256 = "1gzlyxvw64ca12qql3wnq3bidcx9ygsklv9grjma3ib4hvg7vnr7";
+    "3.9".sha256 = "1srcz2dqrvmbvv5cl66r34zqkm0hsbryk7gd3i9xx4slahc9zvdb";
+    "3.10".sha256 = "sha256:19rmx8r8v46101ij5myfrz60arqjy7q3ra3fb8mxqqi3c8c4l4j6";
+  };
+
+  nativeBuildInputs = [ makeWrapper ];
+  buildInputs = with ocamlPackages; [ ocaml findlib menhir menhirLib ] ++ [ coq coq2html ];
+  propagatedBuildInputs = [ flocq ];
+
+  enableParallelBuilding = true;
+
+  postPatch = ''
+    substituteInPlace ./configure \
+      --replace \$\{toolprefix\}ar 'ar' \
+      --replace '{toolprefix}gcc' '{toolprefix}cc'
+  '';
+
+  configurePhase = ''
+    ./configure -clightgen \
+    -prefix $out \
+    -coqdevdir $lib/lib/coq/${coq.coq-version}/user-contrib/compcert/ \
+    -toolprefix ${tools}/bin/ \
+    -use-external-Flocq \
+    ${if stdenv.isDarwin then "x86_64-macosx" else "x86_64-linux"}
+  '';
+
+  installTargets = "documentation install";
+  installFlags = []; # trust ./configure
+  preInstall = ''
+    mkdir -p $out/share/man
+    mkdir -p $man/share
+  '';
+  postInstall = ''
+    # move man into place
+    mv $out/share/man/ $man/share/
+
+    # move docs into place
+    mkdir -p $doc/share/doc/compcert
+    mv doc/html $doc/share/doc/compcert/
+
+    # wrap ccomp to undefine _FORTIFY_SOURCE; ccomp invokes cc1 which sets
+    # _FORTIFY_SOURCE=2 by default, but undefines __GNUC__ (as it should),
+    # which causes a warning in libc. this suppresses it.
+    for x in ccomp clightgen; do
+      wrapProgram $out/bin/$x --add-flags "-U_FORTIFY_SOURCE"
+    done
+  '';
+
+  outputs = [ "out" "lib" "doc" "man" ];
+
+  meta = with lib; {
+    description = "Formally verified C compiler";
+    homepage    = "https://compcert.org";
+    license     = licenses.inria-compcert;
+    platforms   = [ "x86_64-linux" "x86_64-darwin" ];
+    maintainers = with maintainers; [ thoughtpolice jwiegley vbgl ];
+  };
+}; in
+compcert.overrideAttrs (o:
+  {
+    patches = with versions; switch [ coq.version o.version ] [
+      { cases = [ (range "8.12.2" "8.13.2") "3.8" ];
+        out = [
+          # Support for Coq 8.12.2
+          (fetchpatch {
+            url = "https://github.com/AbsInt/CompCert/commit/06956421b4307054af221c118c5f59593c0e67b9.patch";
+            sha256 = "1f90q6j3xfvnf3z830bkd4d8526issvmdlrjlc95bfsqs78i1yrl";
+          })
+          # Support for Coq 8.13.0
+          (fetchpatch {
+            url = "https://github.com/AbsInt/CompCert/commit/0895388e7ebf9c9f3176d225107e21968919fb97.patch";
+            sha256 = "0qhkzgb2xl5kxys81pldp3mr39gd30lvr2l2wmplij319vp3xavd";
+          })
+          # Support for Coq 8.13.1
+          (fetchpatch {
+            url = "https://github.com/AbsInt/CompCert/commit/6bf310dd678285dc193798e89fc2c441d8430892.patch";
+            sha256 = "026ahhvpj5pksy90f8pnxgmhgwfqk4kwyvcf8x3dsanvz98d4pj5";
+          })
+          # Drop support for Coq < 8.9
+          (fetchpatch {
+            url = "https://github.com/AbsInt/CompCert/commit/7563a5df926a4c6fb1489a7a4c847641c8a35095.patch";
+            sha256 = "05vkslzy399r3dm6dmjs722rrajnyfa30xsyy3djl52isvn4gyfb";
+          })
+          # Support for Coq 8.13.2
+          (fetchpatch {
+            url = "https://github.com/AbsInt/CompCert/commit/48bc183167c4ce01a5c9ea86e49d60530adf7290.patch";
+            sha256 = "0j62lppfk26d1brdp3qwll2wi4gvpx1k70qivpvby5f7dpkrkax1";
+          })
+        ];
+      }
+      { cases = [ (range "8.14" "8.15") "3.10" ];
+        out = [
+          # Support for Coq 8.14.1
+          (fetchpatch {
+            url = "https://github.com/AbsInt/CompCert/commit/a79f0f99831aa0b0742bf7cce459cc9353bd7cd0.patch";
+            sha256 = "sha256:0g20x8gfzvplpad9y9vr1p33k6qv6rsp691x6687v9ffvz7zsz94";
+          })
+          # Support for Coq 8.15.0
+          (fetchpatch {
+            url = "https://github.com/AbsInt/CompCert/commit/a882f78c069f7337dd9f4abff117d4df98ef38a6.patch";
+            sha256 = "sha256:16i87s608fj9ni7cvd5wrd7gicqniad7w78wi26pxdy0pacl7bjg";
+          })
+          # Support for Coq 8.15.1
+          (fetchpatch {
+            url = "https://github.com/AbsInt/CompCert/commit/10a976994d7fd30d143354c289ae735d210ccc09.patch";
+            sha256 = "sha256:0bg58gpkgxlmxzp6sg0dvybrfk0pxnm7qd6vxlrbsbm2w6wk03jv";
+          })
+          # Support for Coq 8.15.2
+          (fetchpatch {
+            url = "https://github.com/AbsInt/CompCert/commit/283a5be7296c4c0a94d863b427c77007ab875733.patch";
+            sha256 = "sha256:1s7hvb5ii3p8kkcjlzwldvk8xc3iiibxi9935qjbrh25xi6qs66k";
+          })
+        ];
+      }
+    ] [];
+  }
+)
--- a/pkgs/development/coq-modules/contribs/default.nix
+++ b/pkgs/development/coq-modules/contribs/default.nix
--- a/pkgs/development/coq-modules/coq-bits/default.nix
+++ b/pkgs/development/coq-modules/coq-bits/default.nix
@ -0,0 +1,22 @@
+{ lib, mkCoqDerivation, coq, mathcomp-algebra, version ? null }:
+
+with lib; mkCoqDerivation {
+  pname = "coq-bits";
+  repo = "bits";
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = isGe "8.10"; out = "1.1.0"; }
+    { case = isGe "8.7";  out = "1.0.0"; }
+  ] null;
+
+  release."1.1.0".sha256 = "sha256-TCw1kSXeW0ysIdLeNr+EGmpGumEE9i8tinEMp57UXaE=";
+  release."1.0.0".sha256 = "0nv5mdgrd075dpd8bc7h0xc5i95v0pkm0bfyq5rj6ii1s54dwcjl";
+
+  propagatedBuildInputs = [ mathcomp-algebra ];
+
+  meta = {
+    description = "A formalization of bitset operations in Coq";
+    license = licenses.asl20;
+    maintainers = with maintainers; [ ptival ];
+  };
+}
--- a/pkgs/development/coq-modules/coq-elpi/default.nix
+++ b/pkgs/development/coq-modules/coq-elpi/default.nix
@ -0,0 +1,60 @@
+{ lib, mkCoqDerivation, which, coq, version ? null }:
+
+with builtins; with lib; let
+  elpi = coq.ocamlPackages.elpi.override (lib.switch coq.coq-version [
+    { case = "8.11"; out = { version = "1.11.4"; };}
+    { case = "8.12"; out = { version = "1.12.0"; };}
+    { case = "8.13"; out = { version = "1.13.7"; };}
+    { case = "8.14"; out = { version = "1.13.7"; };}
+    { case = "8.15"; out = { version = "1.15.0"; };}
+  ] {} );
+in mkCoqDerivation {
+  pname = "elpi";
+  repo  = "coq-elpi";
+  owner = "LPCIC";
+  inherit version;
+  defaultVersion = lib.switch coq.coq-version [
+    { case = "8.15"; out = "1.14.0"; }
+    { case = "8.14"; out = "1.11.2"; }
+    { case = "8.13"; out = "1.11.1"; }
+    { case = "8.12"; out = "1.8.3_8.12"; }
+    { case = "8.11"; out = "1.6.3_8.11"; }
+  ] null;
+  release."1.14.0".sha256     = "sha256:1v2p5dlpviwzky2i14cj7gcgf8cr0j54bdm9fl5iz1ckx60j6nvp";
+  release."1.13.0".sha256     = "1j7s7dlnjbw222gnbrsjgmjck1yrx7h6hwm8zikcyxi0zys17w7n";
+  release."1.12.1".sha256     = "sha256-4mO6/co7NcIQSGIQJyoO8lNWXr6dqz+bIYPO/G0cPkY=";
+  release."1.11.2".sha256     = "0qk5cfh15y2zrja7267629dybd3irvxk1raz7z8qfir25a81ckd4";
+  release."1.11.1".sha256     = "10j076vc2hdcbm15m6s7b6xdzibgfcbzlkgjnlkr2vv9k13qf8kc";
+  release."1.10.1".sha256     = "1zsyx26dvj7pznfd2msl2w7zbw51q1nsdw0bdvdha6dga7ijf7xk";
+  release."1.9.7".sha256      = "0rvn12h9dpk9s4pxy32p8j0a1h7ib7kg98iv1cbrdg25y5vs85n1";
+  release."1.9.5".sha256      = "0gjdwmb6bvb5gh0a6ra48bz5fb3pr5kpxijb7a8mfydvar5i9qr6";
+  release."1.9.4".sha256      = "0nii7238mya74f9g6147qmpg6gv6ic9b54x5v85nb6q60d9jh0jq";
+  release."1.9.3".sha256      = "198irm800fx3n8n56vx1c6f626cizp1d7jfkrc6ba4iqhb62ma0z";
+  release."1.9.2".sha256      = "1rr2fr8vjkc0is7vh1461aidz2iwkigdkp6bqss4hhv0c3ijnn07";
+  release."1.8.3_8.12".sha256  = "15z2l4zy0qpw0ws7bvsmpmyv543aqghrfnl48nlwzn9q0v89p557";
+  release."1.8.3_8.12".version = "1.8.3";
+  release."1.8.2_8.12".sha256  = "1n6jwcdazvjgj8vsv2r9zgwpw5yqr5a1ndc2pwhmhqfl04b5dk4y";
+  release."1.8.2_8.12".version = "1.8.2";
+  release."1.8.1".sha256      = "1fbbdccdmr8g4wwpihzp4r2xacynjznf817lhijw6kqfav75zd0r";
+  release."1.8.0".sha256      = "13ywjg94zkbki22hx7s4gfm9rr87r4ghsgan23xyl3l9z8q0idd1";
+  release."1.7.0".sha256      = "1ws5cqr0xawv69prgygbl3q6dgglbaw0vc397h9flh90kxaqgyh8";
+  release."1.6.3_8.11".sha256 = "1j340cr2bv95clzzkkfmsjkklham1mj84cmiyprzwv20q89zr1hp";
+  release."1.6.3_8.11".version = "1.6.3";
+  release."1.6.2_8.11".sha256 = "06xrx0ljilwp63ik2sxxr7h617dgbch042xfcnfpy5x96br147rn";
+  release."1.6.2_8.11".version = "1.6.2";
+  release."1.6.1_8.11".sha256 = "0yyyh35i1nb3pg4hw7cak15kj4y6y9l84nwar9k1ifdsagh5zq53";
+  release."1.6.1_8.11".version = "1.6.1";
+  release."1.6.0_8.11".sha256 = "0ahxjnzmd7kl3gl38kyjqzkfgllncr2ybnw8bvgrc6iddgga7bpq";
+  release."1.6.0_8.11".version = "1.6.0";
+  release."1.6.0".sha256      = "0kf99i43mlf750fr7fric764mm495a53mg5kahnbp6zcjcxxrm0b";
+  releaseRev = v: "v${v}";
+
+  mlPlugin = true;
+  propagatedBuildInputs = [ elpi ];
+
+  meta = {
+    description = "Coq plugin embedding ELPI.";
+    maintainers = [ maintainers.cohencyril ];
+    license = licenses.lgpl21Plus;
+  };
+}
--- a/pkgs/development/coq-modules/coq-ext-lib/default.nix
+++ b/pkgs/development/coq-modules/coq-ext-lib/default.nix
@ -0,0 +1,33 @@
+{ lib, mkCoqDerivation, coq, version ? null }:
+
+with lib; mkCoqDerivation rec {
+  pname = "coq-ext-lib";
+  owner = "coq-ext-lib";
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = range "8.8" "8.15"; out = "0.11.6"; }
+    { case = range "8.8" "8.14"; out = "0.11.4"; }
+    { case = range "8.8" "8.13"; out = "0.11.3"; }
+    { case = "8.7";              out = "0.9.7"; }
+    { case = "8.6";              out = "0.9.5"; }
+    { case = "8.5";              out = "0.9.4"; }
+  ] null;
+  release."0.11.6".sha256 = "0w6iyrdszz7zc8kaybhy3mwjain2d2f83q79xfd5di0hgdayh7q7";
+  release."0.11.4".sha256 = "0yp8mhrhkc498nblvhq1x4j6i9aiidkjza4wzvrkp9p8rgx5g5y3";
+  release."0.11.3".sha256 = "1w99nzpk72lffxis97k235axss5lmzhy5z3lga2i0si95mbpil42";
+  release."0.11.2".sha256 = "0iyka81g26x5n99xic7kqn8vxqjw8rz7vw9rs27iw04lf137vzv6";
+  release."0.10.3".sha256 = "0795gs2dlr663z826mp63c8h2zfadn541dr8q0fvnvi2z7kfyslb";
+  release."0.11.1".sha256 = "0dmf1p9j8lm0hwaq0af18jxdwg869xi2jm8447zng7krrq3kvkg5";
+  release."0.10.2".sha256 = "1b150rc5bmz9l518r4m3vwcrcnnkkn9q5lrwygkh0a7mckgg2k9f";
+  release."0.10.1".sha256 = "0r1vspad8fb8bry3zliiz4hfj4w1iib1l2gm115a94m6zbiksd95";
+  release."0.10.0".sha256 = "1kxi5bmjwi5zqlqgkyzhhxwgcih7wf60cyw9398k2qjkmi186r4a";
+  release."0.9.7".sha256  = "00v4bm4glv1hy08c8xsm467az6d1ashrznn8p2bmbmmp52lfg7ag";
+  release."0.9.5".sha256  = "1b4cvz3llxin130g13calw5n1zmvi6wdd5yb8a41q7yyn2hd3msg";
+  release."0.9.4".sha256  = "1y66pamgsdxlq2w1338lj626ln70cwj7k53hxcp933g8fdsa4hp0";
+  releaseRev = v: "v${v}";
+
+  meta = {
+    description = "A collection of theories and plugins that may be useful in other Coq developments";
+    maintainers = with maintainers; [ jwiegley ptival ];
+  };
+}
--- a/pkgs/development/coq-modules/coq-haskell/default.nix
+++ b/pkgs/development/coq-modules/coq-haskell/default.nix
@ -0,0 +1,21 @@
+{ lib, mkCoqDerivation, coq, ssreflect, version ? null }:
+
+with lib; mkCoqDerivation {
+
+  pname = "coq-haskell";
+  owner = "jwiegley";
+  inherit version;
+  defaultVersion = if versions.range "8.5" "8.8" coq.coq-version then "20171215" else null;
+  release."20171215".rev    = "e2cf8b270c2efa3b56fab1ef6acc376c2c3de968";
+  release."20171215".sha256 = "09dq1vvshhlhgjccrhqgbhnq2hrys15xryfszqq11rzpgvl2zgdv";
+
+  mlPlugin = true;
+  extraInstallFlags = [ "-f Makefile.coq" ];
+  propagatedBuildInputs = [ coq ssreflect ];
+  enableParallelBuilding = false;
+
+  meta = {
+    description = "A library for formalizing Haskell types and functions in Coq";
+    maintainers = with maintainers; [ jwiegley ];
+  };
+}
--- a/pkgs/development/coq-modules/coq-record-update/default.nix
+++ b/pkgs/development/coq-modules/coq-record-update/default.nix
@ -0,0 +1,17 @@
+{ lib, mkCoqDerivation, coq, version ? null , paco, coq-ext-lib }:
+
+with lib; mkCoqDerivation rec {
+  pname = "coq-record-update";
+  owner = "tchajed";
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = range "8.10" "8.15";  out = "0.3.0"; }
+  ] null;
+  release."0.3.0".sha256 = "1ffr21dd6hy19gxnvcd4if2450iksvglvkd6q5713fajd72hmc0z";
+  releaseRev = v: "v${v}";
+  buildFlags = "NO_TEST=1";
+  meta = {
+    description = "Library to create Coq record update functions";
+    maintainers = with maintainers; [ ineol ];
+  };
+}
--- a/pkgs/development/coq-modules/coqeal/default.nix
+++ b/pkgs/development/coq-modules/coqeal/default.nix
@ -0,0 +1,34 @@
+{ coq, mkCoqDerivation, mathcomp, bignums, paramcoq, multinomials,
+  mathcomp-real-closed,
+  lib, version ? null }:
+
+with lib;
+
+(mkCoqDerivation {
+
+  pname = "CoqEAL";
+
+  inherit version;
+  defaultVersion = with versions; switch [ coq.version mathcomp.version ]  [
+      { 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"; }
+      { cases = [ (isGe "8.7") "1.10.0" ]; out = "1.0.3"; }
+    ] null;
+
+  release."1.1.0".sha256 = "1vyhfna5frkkq2fl1fkg2mwzpg09k3sbzxxpyp14fjay81xajrxr";
+  release."1.0.6".sha256 = "0lqkyfj4qbq8wr3yk8qgn7mclw582n3fjl9l19yp8cnchspzywx0";
+  release."1.0.5".sha256 = "0cmvky8glb5z2dy3q62aln6qbav4lrf2q1589f6h1gn5bgjrbzkm";
+  release."1.0.4".sha256 = "1g5m26lr2lwxh6ld2gykailhay4d0ayql4bfh0aiwqpmmczmxipk";
+  release."1.0.3".sha256 = "0hc63ny7phzbihy8l7wxjvn3haxx8jfnhi91iw8hkq8n29i23v24";
+
+  propagatedBuildInputs = [ mathcomp.algebra bignums paramcoq multinomials ];
+
+  meta = {
+    description = "CoqEAL - The Coq Effective Algebra Library";
+    license = licenses.mit;
+  };
+}).overrideAttrs (o: {
+  propagatedBuildInputs = o.propagatedBuildInputs
+  ++ optional (versions.isGe "1.1" o.version || o.version == "dev") mathcomp-real-closed;
+})
--- a/pkgs/development/coq-modules/coqhammer/default.nix
+++ b/pkgs/development/coq-modules/coqhammer/default.nix
@ -0,0 +1,66 @@
+{ lib, mkCoqDerivation, coq, version ? null }:
+
+with lib; mkCoqDerivation {
+  inherit version;
+  pname = "coqhammer";
+  owner = "lukaszcz";
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = "8.15"; out = "1.3.2-coq8.15"; }
+    { case = "8.14"; out = "1.3.2-coq8.14"; }
+    { case = "8.13"; out = "1.3.2-coq8.13"; }
+    { case = "8.12"; out = "1.3.2-coq8.12"; }
+    { case = "8.11"; out = "1.3.2-coq8.11"; }
+    { case = "8.10"; out = "1.3.2-coq8.10"; }
+    { case = "8.9";  out = "1.1.1-coq8.9"; }
+    { case = "8.8";  out = "1.1-coq8.8"; }
+  ] null;
+  release."1.3.2-coq8.15".sha256 = "sha256:0n0y9wda8bx88r17ls9541ibxw013ghp73zshgb65bi7ibznbhha";
+  release."1.3.2-coq8.15".rev = "9a3e689036f12c09800ca3bac05054af0cc49233";
+  release."1.3.2-coq8.14".sha256 = "sha256:1pvs4p95lr31jb86f33p2q9v8zq3xbci1fk6s6a2g2snfxng1574";
+  release."1.3.2-coq8.13".sha256 = "sha256:0krsm8qj9lgfbggxv2jhkbk3vy2cz63qypnarnl31fdmpykchi4b";
+  release."1.3.2-coq8.12".sha256 = "sha256:08mnr13lrdnpims6kf8pk6axf4s8qqs0a71hzg3frkx21d6nawhh";
+  release."1.3.2-coq8.11".sha256 = "sha256:1z54lmr180rdkv549f0dygxlmamsx3fygvsm0d7rz9j88f2z8kc5";
+  release."1.3.2-coq8.10".sha256 = "sha256:08d63ckiwjx07hy5smg5c7a6b3m3a8ra4ljk3z6597633dx85cd0";
+  release."1.3.1-coq8.13".sha256 = "033j6saw24anb1lqbgsg1zynxi2rnxq7pgqwh11k8r8y3xisz78w";
+  release."1.3.1-coq8.12".sha256 = "0xy3vy4rv8w5ydwb9nq8y4dcimd91yr0hak2j4kn02svssg1kv1y";
+  release."1.3.1-coq8.11".sha256 = "0i9nlcayq0ac95vc09d1w8sd221gdjs0g215n086qscqjwimnz8j";
+  release."1.3.1-coq8.10".sha256 = "0aq9qwqx680lkidhb77fmyq403rvfcdxch849x1pzy6a48rz5yra";
+  release."1.3-coq8.12".sha256   = "1q1y3cwhd98pkm98g71fsdjz85bfwgcz2xn7s7wwmiraifv5l6z8";
+  release."1.3-coq8.11".sha256   = "08zf8qfna7b9p2myfaz4g7bas3a1q1156x78n5isqivlnqfrjc1b";
+  release."1.3-coq8.10".sha256   = "1fj8497ir4m79hyrmmmmrag01001wrby0h24wv6525vz0w5py3cd";
+  release."1.1.1-coq8.9" = { sha256 = "1knjmz4hr8vlp103j8n4fyb2lfxysnm512gh3m2kp85n6as6fvb9";
+                             rev    = "f8b4d81a213aa1f25afbe53c7c9ca1b15e3d42bc"; };
+  release."1.1-coq8.8" =   { sha256 = "0ms086wp4jmrzyglb8wymchzyflflk01nsfsk4r6qv8rrx81nx9h";
+                             rev    = "c3cb54b4d5f33fab372d33c7189861368a08fa22"; };
+
+  release."1.3.1-coq8.13".version  = "1.3.1";
+  release."1.3.1-coq8.12".version  = "1.3.1";
+  release."1.3.1-coq8.11".version  = "1.3.1";
+  release."1.3.1-coq8.10".version  = "1.3.1";
+  release."1.3-coq8.12".version  = "1.3";
+  release."1.3-coq8.11".version  = "1.3";
+  release."1.3-coq8.10".version  = "1.3";
+  release."1.1.1-coq8.9".version = "1.1.1";
+  release."1.1-coq8.9".version   = "1.1";
+  releaseRev = v: "v${v}";
+
+  postPatch = ''
+    substituteInPlace Makefile.coq.local --replace \
+      '$(if $(COQBIN),$(COQBIN),`coqc -where | xargs dirname | xargs dirname`/bin/)' \
+      '$(out)/bin/'
+    substituteInPlace Makefile.coq.local --replace 'g++' 'c++' --replace 'gcc' 'cc'
+  '';
+
+  preInstall = ''
+    mkdir -p $out/bin
+  '';
+
+  mlPlugin = true;
+
+  meta = {
+    homepage = "http://cl-informatik.uibk.ac.at/cek/coqhammer/";
+    description = "Automation for Dependent Type Theory";
+    license = licenses.lgpl21;
+    maintainers = [ maintainers.vbgl ];
+  };
+}
--- a/pkgs/development/coq-modules/coqprime/default.nix
+++ b/pkgs/development/coq-modules/coqprime/default.nix
@ -0,0 +1,30 @@
+{ which, lib, mkCoqDerivation, coq, bignums, version ? null }:
+
+with lib; mkCoqDerivation {
+
+  pname = "coqprime";
+  owner = "thery";
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = range "8.12" "8.15"; 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.15".sha256  = "sha256:1zr2q52r08na8265019pj9spcz982ivixk6cnzk6l1srn2g328gv";
+  release."8.14.1".sha256= "sha256:0dqf87xkzcpg7gglbxjyx68ad84w1w73icxgy3s7d3w563glc2p7";
+  release."8.12".sha256  = "1slka4w0pya15js4drx9frj7lxyp3k2lzib8v23givzpnxs8ijdj";
+  release."8.10".sha256  = "0r9gnh5a5ykiiz5h1i8xnzgiydpwc4z9qhndxyya85xq0f910qaz";
+  release."8.8".sha256   = "075yjczk79pf1hd3lgdjiz84ilkzfxjh18lgzrhhqp7d3kz5lxp5";
+  release."8.7.2".sha256 = "15zlcrx06qqxjy3nhh22wzy0rb4npc8l4nx2bbsfsvrisbq1qb7k";
+  releaseRev = v: "v${v}";
+
+  propagatedBuildInputs = [ bignums ];
+
+  meta = with lib; {
+    description = "Library to certify primality using Pocklington certificate and Elliptic Curve Certificate";
+    license = licenses.lgpl21;
+    maintainers = [ maintainers.vbgl ];
+  };
+}
--- a/pkgs/development/coq-modules/coqtail-math/default.nix
+++ b/pkgs/development/coq-modules/coqtail-math/default.nix
@ -0,0 +1,22 @@
+{ lib, mkCoqDerivation, coq, version ? null }:
+
+with lib;
+
+mkCoqDerivation {
+  pname = "coqtail-math";
+  owner = "coq-community";
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = range "8.11" "8.15"; out = "8.14"; }
+    { case = range "8.11" "8.13"; out = "20201124"; }
+  ] null;
+
+  release."8.14".sha256 = "sha256:1k8f8idjnx0mf4z479vcx55iz42rjxrbplbznv80m2famxakq03c";
+  release."20201124".rev    = "5c22c3d7dcd8cf4c47cf84a281780f5915488e9e";
+  release."20201124".sha256 = "sha256-wd+Lh7dpAD4zfpyKuztDmSFEZo5ZiFrR8ti2jUCVvoQ=";
+  mlPlugin = true;
+  meta = {
+    license = licenses.lgpl3Only;
+    maintainers = [ maintainers.siraben ];
+  };
+}
--- a/pkgs/development/coq-modules/coquelicot/default.nix
+++ b/pkgs/development/coq-modules/coquelicot/default.nix
@ -0,0 +1,29 @@
+{ lib, mkCoqDerivation, autoconf,
+  coq, ssreflect, version ? null }:
+
+with lib; mkCoqDerivation {
+  pname = "coquelicot";
+  owner = "coquelicot";
+  domain = "gitlab.inria.fr";
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = isGe "8.8" ;        out = "3.2.0"; }
+    { case = range "8.8" "8.13"; out = "3.1.0"; }
+    { case = range "8.5" "8.9";  out = "3.0.2"; }
+  ] null;
+  release."3.2.0".sha256 = "07w7dbl8x7xxnbr2q39wrdh054gvi3daqjpdn1jm53crsl1fjxm4";
+  release."3.1.0".sha256 = "02i0djar13yk01hzaqprcldhhscn9843x9nf6x3jkv4wv1jwnx9f";
+  release."3.0.2".sha256 = "1rqfbbskgz7b1bcpva8wh3v3456sq2364y804f94sc8y5sij23nl";
+  releaseRev = v: "coquelicot-${v}";
+
+  nativeBuildInputs = [ autoconf ];
+  propagatedBuildInputs = [ ssreflect ];
+  useMelquiondRemake.logpath = "Coquelicot";
+
+  meta = {
+    homepage = "http://coquelicot.saclay.inria.fr/";
+    description = "A Coq library for Reals";
+    license = licenses.lgpl3;
+    maintainers = [ maintainers.vbgl ];
+  };
+}
--- a/pkgs/development/coq-modules/corn/default.nix
+++ b/pkgs/development/coq-modules/corn/default.nix
@ -0,0 +1,28 @@
+{ lib, mkCoqDerivation, coq, bignums, math-classes, version ? null }:
+
+with lib; mkCoqDerivation rec {
+  pname = "corn";
+  inherit version;
+  defaultVersion = switch coq.coq-version [
+    { case = "8.6"; out = "8.8.1"; }
+    { case = (versions.range "8.7" "8.15"); out = "8.13.0"; }
+  ] null;
+  release = {
+    "8.8.1".sha256 = "0gh32j0f18vv5lmf6nb87nr5450w6ai06rhrnvlx2wwi79gv10wp";
+    "8.12.0".sha256 = "0b92vhyzn1j6cs84z2182fn82hxxj0bqq7hk6cs4awwb3vc7dkhi";
+    "8.13.0".sha256 = "1wzr7mdsnf1rq7q0dvmv55vxzysy85b00ahwbs868bl7m8fk8x5b";
+  };
+
+  preConfigure = "patchShebangs ./configure.sh";
+  configureScript = "./configure.sh";
+  dontAddPrefix = true;
+
+  propagatedBuildInputs = [ bignums math-classes ];
+
+  meta = {
+    homepage = "http://c-corn.github.io/";
+    license = licenses.gpl2;
+    description = "A Coq library for constructive analysis";
+    maintainers = [ maintainers.vbgl ];
+  };
+}
--- a/pkgs/development/coq-modules/deriving/default.nix
+++ b/pkgs/development/coq-modules/deriving/default.nix
@ -0,0 +1,29 @@
+{ lib, mkCoqDerivation, coq, version ? null
+, ssreflect
+}:
+with lib;
+
+mkCoqDerivation {
+  pname = "deriving";
+  owner = "arthuraa";
+
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = range "8.11" "8.15"; out = "0.1.0"; }
+  ] null;
+
+  releaseRev = v: "v${v}";
+
+  release."0.1.0".sha256 = "sha256:11crnjm8hyis1qllkks3d7r07s1rfzwvyvpijya3s6iqfh8c7xwh";
+
+  propagatedBuildInputs = [ ssreflect ];
+
+  mlPlugin = true;
+
+  meta = {
+    description = "Generic instances of MathComp classes";
+    license = licenses.mit;
+    maintainers = [ maintainers.vbgl ];
+  };
+
+}
--- a/pkgs/development/coq-modules/dpdgraph/default.nix
+++ b/pkgs/development/coq-modules/dpdgraph/default.nix
@ -0,0 +1,65 @@
+{ lib, mkCoqDerivation, autoreconfHook, coq, version ? null }:
+
+with lib;
+let hasWarning = versionAtLeast coq.ocamlPackages.ocaml.version "4.08"; in
+
+mkCoqDerivation {
+  pname = "dpdgraph";
+  owner = "Karmaki";
+  repo = "coq-dpdgraph";
+  inherit version;
+  defaultVersion = switch coq.coq-version [
+    { case = "8.15"; out = "1.0+8.15"; }
+    { case = "8.14"; out = "1.0+8.14"; }
+    { case = "8.13"; out = "1.0+8.13"; }
+    { case = "8.12"; out = "0.6.8"; }
+    { case = "8.11"; out = "0.6.7"; }
+    { case = "8.10"; out = "0.6.6"; }
+    { 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.15".sha256 = "sha256:1pxr0gakcz297y8hhrnssv5j07ccd58pv7rh7qv5g7855pfqrkg7";
+  release."1.0+8.14".sha256 = "sha256:01pmi7jcc77431jii6x6nd4m8jg4vycachiyi1h6dx9rp3a2508s";
+  release."1.0+8.13".sha256 = "sha256:0f8lj8b99n8nsq2jf5m0snblfs8yz50hmlqqq9nlw4qklq7j4z5z";
+  release."0.6.9".sha256 = "11mbydpcgk7y8pqzickbzx0ig7g9k9al71i9yfrcscd2xj8fwj8z";
+  release."0.6.8".sha256 = "1mj6sknsd53xfb387sp3kdwvl4wn80ck24bfzf3s6mgw1a12vyps";
+  release."0.6.7".sha256 = "01vpi7scvkl4ls1z2k2x9zd65wflzb667idj759859hlz3ps9z09";
+  release."0.6.6".sha256 = "1gjrm5zjzw4cisiwdr5b3iqa7s4cssa220xr0k96rwgk61rcjd8w";
+  release."0.6.5".sha256 = "1f34z24yg05b1096gqv36jr3vffkcjkf9qncii3pzhhvagxd0w2f";
+  release."0.6.3".rev    = "0acbd0a594c7e927574d5f212cc73a486b5305d2";
+  release."0.6.3".sha256 = "0c95b0bz2kjm6swr5na4gs06lxxywradszxbr5ldh2zx02r3f3rx";
+  release."0.6.2".rev    = "d76ddde37d918569945774733b7997e8b24daf51";
+  release."0.6.2".sha256 = "04lnf4b25yarysj848cfl8pd3i3pr3818acyp9hgwdgd1rqmhjwm";
+  release."0.6.1".rev    = "c3b87af6bfa338e18b83f014ebd0e56e1f611663";
+  release."0.6.1".sha256 = "1jaafkwsb5450378nprjsds1illgdaq60gryi8kspw0i25ykz2c9";
+  release."0.6".sha256   = "0qvar8gfbrcs9fmvkph5asqz4l5fi63caykx3bsn8zf0xllkwv0n";
+  releaseRev = v: "v${v}";
+
+  nativeBuildInputs = [ autoreconfHook ];
+  mlPlugin = true;
+  buildInputs = [ coq.ocamlPackages.ocamlgraph ];
+
+  # dpd_compute.ml uses deprecated Pervasives.compare
+  # Versions prior to 0.6.5 do not have the WARN_ERR build flag
+  preConfigure = optionalString hasWarning ''
+    substituteInPlace Makefile.in --replace "-warn-error +a " ""
+  '';
+
+  buildFlags = optional hasWarning "WARN_ERR=";
+
+  preInstall = ''
+    mkdir -p $out/bin
+  '';
+
+  extraInstallFlags = [ "BINDIR=$(out)/bin" ];
+
+  meta = {
+    description = "Build dependency graphs between Coq objects";
+    license = licenses.lgpl21;
+    maintainers = with maintainers; [ vbgl ];
+  };
+}
--- a/pkgs/development/coq-modules/equations/default.nix
+++ b/pkgs/development/coq-modules/equations/default.nix
@ -0,0 +1,63 @@
+{ lib, mkCoqDerivation, coq, version ? null }:
+
+with lib; mkCoqDerivation {
+  pname = "equations";
+  owner = "mattam82";
+  repo = "Coq-Equations";
+  inherit version;
+  defaultVersion = switch coq.coq-version [
+    { case = "8.15"; out = "1.3+8.15"; }
+    { case = "8.14"; out = "1.3+8.14"; }
+    { case = "8.13"; out = "1.3+8.13"; }
+    { case = "8.12"; out = "1.2.4+coq8.12"; }
+    { case = "8.11"; out = "1.2.4+coq8.11"; }
+    { case = "8.10"; out = "1.2.1+coq8.10-2"; }
+    { case = "8.9";  out = "1.2.1+coq8.9"; }
+    { case = "8.8";  out = "1.2+coq8.8"; }
+    { case = "8.7";  out = "1.0+coq8.7"; }
+    { case = "8.6";  out = "1.0+coq8.6"; }
+  ] null;
+
+    release."1.0+coq8.6".version      = "1.0";
+    release."1.0+coq8.6".rev          = "v1.0";
+    release."1.0+coq8.6".sha256       = "19ylw9v9g35607w4hm86j7mmkghh07hmkc1ls5bqlz3dizh5q4pj";
+    release."1.0+coq8.7".version      = "1.0";
+    release."1.0+coq8.7".rev          = "v1.0-8.7";
+    release."1.0+coq8.7".sha256       = "1bavg4zl1xn0jqrdq8iw7xqzdvdf39ligj9saz5m9c507zri952h";
+    release."1.2+coq8.8".version      = "1.2";
+    release."1.2+coq8.8".rev          = "v1.2-8.8";
+    release."1.2+coq8.8".sha256       = "06452fyzalz7zcjjp73qb7d6xvmqb6skljkivf8pfm55fsc8s7kx";
+    release."1.2.1+coq8.9".version    = "1.2.1";
+    release."1.2.1+coq8.9".rev        = "v1.2.1-8.9";
+    release."1.2.1+coq8.9".sha256     = "0d8ddj6nc6p0k25cd8fs17cq427zhzbc3v9pk2wd2fnvk70nlfij";
+    release."1.2.1+coq8.10-2".version = "1.2.1";
+    release."1.2.1+coq8.10-2".rev     = "v1.2.1-8.10-2";
+    release."1.2.1+coq8.10-2".sha256  = "0j3z4l5nrbyi9zbbyqkc6kassjanwld2188mwmrbqspaypm2ys68";
+    release."1.2.3+coq8.11".version   = "1.2.3";
+    release."1.2.3+coq8.11".rev       = "v1.2.3-8.11";
+    release."1.2.3+coq8.11".sha256    = "1srxz1rws8jsh7402g2x2vcqgjbbsr64dxxj5d2zs48pmhb20csf";
+    release."1.2.3+coq8.12".version   = "1.2.3";
+    release."1.2.3+coq8.12".rev       = "v1.2.3-8.12";
+    release."1.2.3+coq8.12".sha256    = "1y0jkvzyz5ssv5vby41p1i8zs7nsdc8g3pzyq73ih9jz8h252643";
+    release."1.2.4+coq8.11".rev       = "v1.2.4-8.11";
+    release."1.2.4+coq8.11".sha256    = "01fihyav8jbjinycgjc16adpa0zy5hcav5mlkf4s9zvqxka21i52";
+    release."1.2.4+coq8.12".rev       = "v1.2.4-8.12";
+    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.13".rev            = "v1.3-8.13";
+    release."1.3+8.13".sha256         = "1jwjbkkkk4bwf6pz4zzz8fy5bb17aqyf4smkja59rgj9ya6nrdhg";
+    release."1.3+8.14".rev            = "v1.3-8.14";
+    release."1.3+8.14".sha256         = "19bj9nncd1r9g4273h5qx35gs3i4bw5z9bhjni24b413hyj55hkv";
+    release."1.3+8.15".rev            = "v1.3-8.15";
+    release."1.3+8.15".sha256         = "1vfcfpsp9zyj0sw0cwibk76nj6n0r6gwh8m1aa3lbvc0b1kbm32k";
+
+  mlPlugin = true;
+  preBuild = "coq_makefile -f _CoqProject -o Makefile";
+
+  meta = {
+    homepage = "https://mattam82.github.io/Coq-Equations/";
+    description = "A plugin for Coq to add dependent pattern-matching";
+    maintainers = with maintainers; [ jwiegley ];
+  };
+}
--- a/pkgs/development/coq-modules/extructures/default.nix
+++ b/pkgs/development/coq-modules/extructures/default.nix
@ -0,0 +1,35 @@
+{ lib, mkCoqDerivation, coq, version ? null
+, ssreflect
+, deriving
+}:
+with lib;
+
+(mkCoqDerivation {
+  pname = "extructures";
+  owner = "arthuraa";
+
+  inherit version;
+  defaultVersion = with versions; switch [coq.coq-version ssreflect.version] [
+    { cases = [(isGe "8.11") (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"; }
+  ] null;
+
+  releaseRev = v: "v${v}";
+
+  release."0.3.1".sha256 = "sha256-KcuG/11Yq5ACem4FyVnQqHKvy3tNK7hd0ir2SJzzMN0=";
+  release."0.3.0".sha256 = "sha256:14rm0726f1732ldds495qavg26gsn30w6dfdn36xb12g5kzavp38";
+  release."0.2.2".sha256 = "sha256:1clzza73gccy6p6l95n6gs0adkqd3h4wgl4qg5l0qm4q140grvm7";
+
+  propagatedBuildInputs = [ ssreflect ];
+
+  meta = {
+    description = "Finite data structures with extensional reasoning";
+    license = licenses.mit;
+    maintainers = [ maintainers.vbgl ];
+  };
+
+}).overrideAttrs (o: {
+  propagatedBuildInputs = o.propagatedBuildInputs
+  ++ optional (versionAtLeast o.version "0.3.0") deriving;
+})
--- a/pkgs/development/coq-modules/fiat/HEAD.nix
+++ b/pkgs/development/coq-modules/fiat/HEAD.nix
@ -0,0 +1,34 @@
+{lib, mkCoqDerivation, coq, python27, version ? null }:
+
+with lib; mkCoqDerivation rec {
+  pname = "fiat";
+  owner = "mit-plv";
+  repo = "fiat";
+  displayVersion = { fiat = v: "unstable-${v}"; };
+  inherit version;
+  defaultVersion = if coq.coq-version == "8.5" then "2016-10-24" else null;
+  release."2016-10-24".rev    = "7feb6c64be9ebcc05924ec58fe1463e73ec8206a";
+  release."2016-10-24".sha256 = "16y57vibq3f5i5avgj80f4i3aw46wdwzx36k5d3pf3qk17qrlrdi";
+
+  mlPlugin = true;
+  buildInputs = [ python27 ];
+
+  prePatch = "patchShebangs etc/coq-scripts";
+
+  doCheck = false;
+
+  enableParallelBuilding = false;
+  buildPhase = "make -j$NIX_BUILD_CORES";
+
+  installPhase = ''
+    COQLIB=$out/lib/coq/${coq.coq-version}/
+    mkdir -p $COQLIB/user-contrib/Fiat
+    cp -pR src/* $COQLIB/user-contrib/Fiat
+  '';
+
+  meta = {
+    homepage = "http://plv.csail.mit.edu/fiat/";
+    description = "A library for the Coq proof assistant for synthesizing efficient correct-by-construction programs from declarative specifications";
+    maintainers = with maintainers; [ jwiegley ];
+  };
+}
--- a/pkgs/development/coq-modules/flocq/default.nix
+++ b/pkgs/development/coq-modules/flocq/default.nix
@ -0,0 +1,28 @@
+{ lib, bash, autoconf, automake,
+  mkCoqDerivation, coq, version ? null }:
+
+with lib; mkCoqDerivation {
+  pname = "flocq";
+  owner = "flocq";
+  domain = "gitlab.inria.fr";
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = range "8.7" "8.15"; out = "3.4.3"; }
+    { case = range "8.5" "8.8"; out = "2.6.1"; }
+  ] null;
+  release."3.4.3".sha256 = "sha256-YTdWlEmFJjCcHkl47jSOgrGqdXoApJY4u618ofCaCZE=";
+  release."3.4.2".sha256 = "1s37hvxyffx8ccc8mg5aba7ivfc39p216iibvd7f2cb9lniqk1pw";
+  release."3.3.1".sha256 = "1mk8adhi5hrllsr0hamzk91vf2405sjr4lh5brg9201mcw11abkz";
+  release."2.6.1".sha256 = "0q5a038ww5dn72yvwn5298d3ridkcngb1dik8hdyr3xh7gr5qibj";
+  releaseRev = v: "flocq-${v}";
+
+  nativeBuildInputs = [ bash autoconf ];
+  mlPlugin = true;
+  useMelquiondRemake.logpath = "Flocq";
+
+  meta = {
+    description = "A floating-point formalization for the Coq system";
+    license = licenses.lgpl3;
+    maintainers = with maintainers; [ jwiegley ];
+  };
+}
--- a/pkgs/development/coq-modules/fourcolor/default.nix
+++ b/pkgs/development/coq-modules/fourcolor/default.nix
@ -0,0 +1,27 @@
+{ lib, mkCoqDerivation, coq, mathcomp, version ? null }:
+with lib;
+
+mkCoqDerivation {
+  pname = "fourcolor";
+  owner = "math-comp";
+
+  release."1.2.3".rev    = "v1.2.3";
+  release."1.2.3".sha256 = "sha256-gwKfUa74fIP7j+2eQgnLD7AswjCtOFGHGaIWb4qI0n4=";
+  release."1.2.4".rev    = "v1.2.4";
+  release."1.2.4".sha256 = "sha256-iSW2O1kuunvOqTolmGGXmsYTxo2MJYCdW3BnEhp6Ksg=";
+
+  inherit version;
+  defaultVersion = with versions; switch [ coq.version mathcomp.version ] [
+    { cases = [ (isGe "8.11") (isGe "1.11.0") ]; out = "1.2.4"; }
+    { cases = [ (isLe "8.13") (pred.inter (isGe "1.11.0") (isLt "1.13")) ]; out = "1.2.3"; }
+  ] null;
+
+  propagatedBuildInputs = [ mathcomp.algebra mathcomp.ssreflect mathcomp.fingroup ];
+
+  meta = {
+    description = "Formal proof of the Four Color Theorem ";
+    maintainers = with maintainers; [ siraben ];
+    license = licenses.cecill-b;
+    platforms = platforms.unix;
+  };
+}
--- a/pkgs/development/coq-modules/gaia-hydras/default.nix
+++ b/pkgs/development/coq-modules/gaia-hydras/default.nix
@ -0,0 +1,36 @@
+{ lib, mkCoqDerivation, coq, hydra-battles, gaia,
+  mathcomp-zify, mathcomp, version ? null }:
+
+with lib; mkCoqDerivation rec {
+  pname = "gaia-hydras";
+  repo = "hydra-battles";
+
+  release."0.5".sha256 = "121pcbn6v59l0c165ha9n00whbddpy11npx2y9cn7g879sfk2nqk";
+  release."0.6".sha256 = "1dri4sisa7mhclf8w4kw7ixs5zxm8xyjr034r1377p96rdk3jj0j";
+  releaseRev = (v: "v${v}");
+
+  inherit version;
+  defaultVersion = with versions; switch [coq.coq-version mathcomp.version] [
+    { cases = [ (range "8.14" "8.15") (isGe "1.12.0") ]; out = "0.6"; }
+    { cases = [ (range "8.13" "8.14") (isGe "1.12.0") ]; out = "0.5"; }
+  ] null;
+
+  propagatedBuildInputs = [
+    hydra-battles
+    gaia
+    mathcomp-zify
+  ];
+
+  useDune2 = true;
+
+  meta = {
+    description = "Comparison between ordinals in Gaia and Hydra battles";
+    longDescription = ''
+      The Gaia and Hydra battles projects develop different notions of ordinals.
+      This development bridges the different notions.
+    '';
+    maintainers = with maintainers; [ Zimmi48 ];
+    license = licenses.mit;
+    platforms = platforms.unix;
+  };
+}
--- a/pkgs/development/coq-modules/gaia/default.nix
+++ b/pkgs/development/coq-modules/gaia/default.nix
@ -0,0 +1,25 @@
+{ lib, mkCoqDerivation, coq, mathcomp, version ? null }:
+
+with lib; mkCoqDerivation {
+  pname = "gaia";
+
+  release."1.11".sha256 = "sha256:0gwb0blf37sv9gb0qpn34dab71zdcx7jsnqm3j9p58qw65cgsqn5";
+  release."1.12".sha256 = "sha256:0c6cim4x6f9944g8v0cp0lxs244lrhb04ms4y2s6y1wh321zj5mi";
+  release."1.13".sha256 = "sha256:0i8ix2rbw10v34bi0yrx0z89ng96ydqbxm8rv2rnfgy4d1b27x6q";
+  releaseRev = (v: "v${v}");
+
+  inherit version;
+  defaultVersion = with versions; switch [ coq.version mathcomp.version ] [
+    { cases = [ (range "8.10" "8.15") (isGe "1.12.0") ]; out = "1.13"; }
+    { cases = [ (range "8.10" "8.12") "1.11.0" ]; out = "1.11"; }
+  ] null;
+
+  propagatedBuildInputs =
+    [ mathcomp.ssreflect mathcomp.algebra mathcomp.fingroup ];
+
+  meta = {
+    description = "Implementation of books from Bourbaki's Elements of Mathematics in Coq";
+    maintainers = with maintainers; [ Zimmi48 ];
+    license = licenses.mit;
+  };
+}
--- a/pkgs/development/coq-modules/gappalib/default.nix
+++ b/pkgs/development/coq-modules/gappalib/default.nix
@ -0,0 +1,26 @@
+{ which, lib, mkCoqDerivation, autoconf, coq, flocq, version ? null }:
+
+with lib; mkCoqDerivation {
+  pname = "gappalib";
+  repo = "coq";
+  owner = "gappa";
+  domain = "gitlab.inria.fr";
+  inherit version;
+  defaultVersion = if versions.range "8.8" "8.15" coq.coq-version then "1.5.1" else null;
+  release."1.5.1".sha256 = "1806bq1z6q5rq2ma7d5kfbqfyfr755hjg0dq7b2llry8fx9cxjsg";
+  release."1.5.0".sha256 = "1i1c0gakffxqqqqw064cbvc243yl325hxd50jmczr6mk18igk41n";
+  release."1.4.5".sha256 = "081hib1d9wfm29kis390qsqch8v6fs3q71g2rgbbzx5y5cf48n9k";
+  release."1.4.4".sha256 = "114q2hgw64j6kqa9mg3qcp1nlf0ia46z2xadq81fnkxqm856ml7l";
+  releaseRev = v: "gappalib-coq-${v}";
+
+  nativeBuildInputs = [ autoconf ];
+  mlPlugin = true;
+  propagatedBuildInputs = [ flocq ];
+  useMelquiondRemake.logpath = "Gappa";
+
+  meta = {
+    description = "Coq support library for Gappa";
+    license = licenses.lgpl21;
+    maintainers = [ maintainers.vbgl ];
+  };
+}
--- a/pkgs/development/coq-modules/goedel/default.nix
+++ b/pkgs/development/coq-modules/goedel/default.nix
@ -0,0 +1,26 @@
+{ lib, mkCoqDerivation, coq, hydra-battles, pocklington, version ? null }:
+with lib;
+
+mkCoqDerivation {
+  pname = "goedel";
+  owner = "coq-community";
+
+  releaseRev = (v: "v${v}");
+
+  release."8.12.0".sha256 = "sha256-4lAwWFHGUzPcfHI9u5b+N+7mQ0sLJ8bH8beqQubfFEQ=";
+  release."8.13.0".sha256 = "0sqqkmj6wsk4xmhrnqkhcsbsrqjzn2gnk67nqzgrmjpw5danz8y5";
+
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = range "8.11" "8.15"; out = "8.13.0"; }
+  ] null;
+
+  propagatedBuildInputs = [ hydra-battles pocklington ];
+
+  meta = {
+    description = "The Gödel-Rosser 1st incompleteness theorem in Coq";
+    maintainers = with maintainers; [ siraben ];
+    license = licenses.mit;
+    platforms = platforms.unix;
+  };
+}
--- a/pkgs/development/coq-modules/graph-theory/default.nix
+++ b/pkgs/development/coq-modules/graph-theory/default.nix
@ -0,0 +1,33 @@
+{ lib, mkCoqDerivation, coq, mathcomp-algebra, mathcomp-finmap, mathcomp-fingroup
+, 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 = range "8.13" "8.15"; out = "0.9"; }
+  ] null;
+
+  propagatedBuildInputs = [ mathcomp-algebra mathcomp-finmap mathcomp-fingroup 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;
+  };
+}
--- a/pkgs/development/coq-modules/heq/default.nix
+++ b/pkgs/development/coq-modules/heq/default.nix
@ -0,0 +1,27 @@
+{lib, fetchzip, mkCoqDerivation, coq, version ? null }:
+
+let fetcher = {rev, repo, owner, sha256, domain, ...}:
+  fetchzip {
+    url = "https://${domain}/${owner}/${repo}/download/${repo}-${rev}.zip";
+    inherit sha256;
+   }; in
+with lib; mkCoqDerivation {
+  pname = "heq";
+  repo = "Heq";
+  owner = "gil.hur";
+  domain = "sf.snu.ac.kr";
+  inherit version fetcher;
+  defaultVersion = if versions.isLt "8.8" coq.coq-version then "0.92" else null;
+  release."0.92".sha256 = "0cf8y6728n81wwlbpq3vi7l2dbzi7759klypld4gpsjjp1y1fj74";
+
+  mlPlugin = true;
+  preBuild = "cd src";
+
+  extraInstallFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
+
+  meta = {
+    homepage = "https://ropas.snu.ac.kr/~gil.hur/Heq/";
+    description = "Heq : a Coq library for Heterogeneous Equality";
+    maintainers = with maintainers; [ jwiegley ];
+  };
+}
--- a/pkgs/development/coq-modules/hierarchy-builder/default.nix
+++ b/pkgs/development/coq-modules/hierarchy-builder/default.nix
@ -0,0 +1,35 @@
+{ lib, mkCoqDerivation, coq, coq-elpi, version ? null }:
+
+with lib; let hb = mkCoqDerivation {
+  pname = "hierarchy-builder";
+  owner = "math-comp";
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = isGe "8.15"; out = "1.2.1"; }
+    { 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"; }
+  ] null;
+  release."1.2.1".sha256  = "sha256-pQYZJ34YzvdlRSGLwsrYgPdz3p/l5f+KhJjkYT08Mj0=";
+  release."1.2.0".sha256  = "0sk01rvvk652d86aibc8rik2m8iz7jn6mw9hh6xkbxlsvh50719d";
+  release."1.1.0".sha256  = "sha256-spno5ty4kU4WWiOfzoqbXF8lWlNSlySWcRReR3zE/4Q=";
+  release."1.0.0".sha256  = "0yykygs0z6fby6vkiaiv3azy1i9yx4rqg8xdlgkwnf2284hffzpp";
+  release."0.10.0".sha256 = "1a3vry9nzavrlrdlq3cys3f8kpq3bz447q8c4c7lh2qal61wb32h";
+  releaseRev = v: "v${v}";
+
+  propagatedBuildInputs = [ coq-elpi ];
+
+  mlPlugin = true;
+
+  extraInstallFlags = [ "VFILES=structures.v" ];
+
+  meta = {
+    description = "High level commands to declare a hierarchy based on packed classes";
+    maintainers = with maintainers; [ cohencyril siraben ];
+    license = licenses.mit;
+  };
+}; in
+hb.overrideAttrs (o:
+  optionalAttrs (versions.isGe "1.2.0" o.version || o.version == "dev")
+    { buildPhase = "make build"; }
+)
--- a/pkgs/development/coq-modules/hydra-battles/default.nix
+++ b/pkgs/development/coq-modules/hydra-battles/default.nix
@ -0,0 +1,37 @@
+{ lib, mkCoqDerivation, coq, equations, LibHyps, version ? null }:
+with lib;
+
+(mkCoqDerivation {
+  pname = "hydra-battles";
+  owner = "coq-community";
+
+  release."0.4".sha256 = "1f7pc4w3kir4c9p0fjx5l77401bx12y72nmqxrqs3qqd3iynvqlp";
+  release."0.5".sha256 = "121pcbn6v59l0c165ha9n00whbddpy11npx2y9cn7g879sfk2nqk";
+  release."0.6".sha256 = "1dri4sisa7mhclf8w4kw7ixs5zxm8xyjr034r1377p96rdk3jj0j";
+  releaseRev = (v: "v${v}");
+
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = range "8.13" "8.15"; out = "0.6"; }
+    { case = range "8.11" "8.12"; out = "0.4"; }
+  ] null;
+
+  useDune2 = true;
+
+  meta = {
+    description = "Exploration of some properties of Kirby and Paris' hydra battles, with the help of Coq";
+    longDescription = ''
+      An exploration of some properties of Kirby and Paris' hydra
+      battles, with the help of the Coq Proof assistant. This
+      development includes the study of several representations of
+      ordinal numbers, and a part of the so-called Ketonen and Solovay
+      machinery (combinatorial properties of epsilon0).
+    '';
+    maintainers = with maintainers; [ siraben Zimmi48 ];
+    license = licenses.mit;
+    platforms = platforms.unix;
+  };
+}).overrideAttrs(o:
+  let inherit (o) version; in {
+    propagatedBuildInputs = [ equations ] ++ optional (versions.isGe "0.6" version || version == "dev") LibHyps;
+  })
--- a/pkgs/development/coq-modules/interval/default.nix
+++ b/pkgs/development/coq-modules/interval/default.nix
@ -0,0 +1,37 @@
+{ lib, mkCoqDerivation, autoconf, coq, coquelicot, flocq,
+  mathcomp-ssreflect, mathcomp-fingroup, bignums ? null, gnuplot_qt, version ? null }:
+
+mkCoqDerivation rec {
+  pname = "interval";
+  owner = "coqinterval";
+  domain = "gitlab.inria.fr";
+  inherit version;
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
+    { case = isGe "8.8"; out = "4.5.1"; }
+    { 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.5.1".sha256 = "sha256-5OxbSPdw/1FFENubulKSk6fEIEYSPCxfvMMgtgN6j6s=";
+  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";
+  release."3.3.0".sha256 = "0lz2hgggzn4cvklvm8rpaxvwaryf37i8mzqajqgdxdbd8f12acsz";
+  releaseRev = v: "interval-${v}";
+
+  nativeBuildInputs = [ autoconf ];
+  propagatedBuildInputs = lib.optional (lib.versions.isGe "8.6" coq.coq-version) bignums
+    ++ [ coquelicot flocq mathcomp-ssreflect mathcomp-fingroup ]
+    ++ 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";
+    license = licenses.cecill-c;
+    maintainers = with maintainers; [ vbgl ];
+  };
+}
--- a/pkgs/development/coq-modules/iris/default.nix
+++ b/pkgs/development/coq-modules/iris/default.nix
@ -0,0 +1,33 @@
+{ lib, mkCoqDerivation, coq, stdpp, version ? null }:
+
+with lib; mkCoqDerivation rec {
+  pname = "iris";
+  domain = "gitlab.mpi-sws.org";
+  owner = "iris";
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = range "8.13" "8.15"; out = "3.6.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."3.6.0".sha256 = "sha256:02vbq597fjxd5znzxdb54wfp36412wz2d4yash4q8yddgl1kakmj";
+  release."3.5.0".sha256 = "0hh14m0anfcv65rxm982ps2vp95vk9fwrpv4br8bxd9vz0091d70";
+  release."3.4.0".sha256 = "0vdc2mdqn5jjd6yz028c0c6blzrvpl0c7apx6xas7ll60136slrb";
+  release."3.3.0".sha256 = "0az4gkp5m8sq0p73dlh0r7ckkzhk7zkg5bndw01bdsy5ywj0vilp";
+  releaseRev = v: "iris-${v}";
+
+  propagatedBuildInputs = [ stdpp ];
+
+  preBuild = ''
+    if [[ -f coq-lint.sh ]]
+    then patchShebangs coq-lint.sh
+    fi
+  '';
+
+  meta = {
+    description = "The Coq development of the Iris Project";
+    license = licenses.bsd3;
+    maintainers = [ maintainers.vbgl ];
+  };
+}
--- a/pkgs/development/coq-modules/itauto/default.nix
+++ b/pkgs/development/coq-modules/itauto/default.nix
@ -0,0 +1,28 @@
+{ lib, mkCoqDerivation, coq, version ? null }:
+with lib;
+
+mkCoqDerivation rec {
+  pname = "itauto";
+  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;
+
+  mlPlugin = true;
+  nativeBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]);
+  enableParallelBuilding = false;
+
+  meta = {
+    description = "A reflexive SAT solver parameterised by a leaf tactic and Nelson-Oppen support";
+    maintainers = with maintainers; [ siraben ];
+    license = licenses.gpl3Plus;
+  };
+}
--- a/pkgs/development/coq-modules/ltac2/default.nix
+++ b/pkgs/development/coq-modules/ltac2/default.nix
@ -0,0 +1,27 @@
+{ lib, mkCoqDerivation, which, coq, version ? null }:
+
+with lib; mkCoqDerivation {
+  pname = "ltac2";
+  owner = "coq";
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = "8.10"; out = "0.3"; }
+    { case = "8.9";  out = "0.2"; }
+    { case = "8.8";  out = "0.1"; }
+    { case = "8.7";  out = "0.1-8.7"; }
+  ] null;
+  release."0.3".sha256 = "0pzs5nsakh4l8ffwgn4ryxbnxdv2x0r1i7bc598ij621haxdirrr";
+  release."0.2".sha256 = "0xby1kb26r9gcvk5511wqj05fqm9paynwfxlfqkmwkgnfmzk0x73";
+  release."0.1".sha256 = "1zz26cyv99whj7rrpgnhhm9dfqnpmrx5pqizn8ihf8jkq8d4drz7";
+  release."0.1-8.7".version = "0.1";
+  release."0.1-8.7".rev     = "v0.1-8.7";
+  release."0.1-8.7".sha256  = "0l6wiwi4cvd0i324fb29i9mdh0ijlxzggw4mrjjy695l2qdnlgg0";
+
+  mlPlugin = true;
+
+  meta = {
+    description = "A robust and expressive tactic language for Coq";
+    maintainers = [ maintainers.vbgl ];
+    license = licenses.lgpl21;
+  };
+}
--- a/pkgs/development/coq-modules/math-classes/default.nix
+++ b/pkgs/development/coq-modules/math-classes/default.nix
@ -0,0 +1,19 @@
+{ lib, mkCoqDerivation, coq, bignums, version ? null }:
+
+with lib; mkCoqDerivation {
+
+  pname = "math-classes";
+  inherit version;
+  defaultVersion = if versions.range "8.6" "8.15" coq.coq-version then "8.15.0" else null;
+  release."8.12.0".sha256 = "14nd6a08zncrl5yg2gzk0xf4iinwq4hxnsgm4fyv07ydbkxfb425";
+  release."8.13.0".sha256 = "1ln7ziivfbxzbdvlhbvyg3v30jgblncmwcsam6gg3d1zz6r7cbby";
+  release."8.15.0".sha256 = "10w1hm537k6jx8a8vghq1yx12rsa0sjk2ipv3scgir71ln30hllw";
+
+  propagatedBuildInputs = [ bignums ];
+
+  meta = {
+    homepage = "https://math-classes.github.io";
+    description = "A library of abstract interfaces for mathematical structures in Coq.";
+    maintainers = with maintainers; [ siddharthist jwiegley ];
+  };
+}
--- a/pkgs/development/coq-modules/mathcomp-abel/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-abel/default.nix
@ -0,0 +1,27 @@
+{ coq, mkCoqDerivation, mathcomp, mathcomp-real-closed, lib, version ? null }:
+
+mkCoqDerivation {
+
+  namePrefix = [ "coq" "mathcomp" ];
+  pname = "abel";
+  owner = "math-comp";
+
+  inherit version;
+  defaultVersion = with lib; with versions; switch [ coq.version mathcomp.version ]  [
+      { cases = [ (range "8.10" "8.15") (isGe "1.12.0") ];           out = "1.2.0"; }
+      { cases = [ (range "8.10" "8.14") (range "1.11.0" "1.12.0") ]; out = "1.1.2"; }
+    ] null;
+
+  release."1.2.0".sha256 = "1picd4m85ipj22j3b84cv8ab3330radzrhd6kp0gpxq14dhv02c2";
+  release."1.1.2".sha256 = "0565w713z1cwxvvdlqws2z5lgdys8lddf0vpwfdj7bpd7pq9hwxg";
+  release."1.0.0".sha256 = "190jd8hb8anqsvr9ysr514pm5sh8qhw4030ddykvwxx9d9q6rbp3";
+
+
+  propagatedBuildInputs = [ mathcomp.field mathcomp-real-closed ];
+
+  meta = with lib; {
+    description = "Abel - Galois and Abel - Ruffini Theorems";
+    license = licenses.cecill-b;
+    maintainers = [ maintainers.cohencyril ];
+  };
+}
--- a/pkgs/development/coq-modules/mathcomp-analysis/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-analysis/default.nix
@ -0,0 +1,47 @@
+{ coq, mkCoqDerivation, mathcomp, mathcomp-finmap, mathcomp-bigenough, mathcomp-real-closed,
+  hierarchy-builder, lib, version ? null }:
+
+with lib;
+let mca = mkCoqDerivation {
+
+  namePrefix = [ "coq" "mathcomp" ];
+  pname = "analysis";
+  owner = "math-comp";
+
+  release."0.3.13".sha256 = "sha256-Yaztew79KWRC933kGFOAUIIoqukaZOdNOdw4XszR1Hg=";
+  release."0.3.10".sha256 = "sha256-FBH2c8QRibq5Ycw/ieB8mZl0fDiPrYdIzZ6W/A3pIhI=";
+  release."0.3.9".sha256 = "sha256-uUU9diBwUqBrNRLiDc0kz0CGkwTZCUmigPwLbpDOeg4=";
+  release."0.3.6".sha256 = "0g2j7b2hca4byz62ssgg90bkbc8wwp7xkb2d3225bbvihi92b4c5";
+  release."0.3.4".sha256 = "18mgycjgg829dbr7ps77z6lcj03h3dchjbj5iir0pybxby7gd45c";
+  release."0.3.3".sha256 = "1m2mxcngj368vbdb8mlr91hsygl430spl7lgyn9qmn3jykack867";
+  release."0.3.1".sha256 = "1iad288yvrjv8ahl9v18vfblgqb1l5z6ax644w49w9hwxs93f2k8";
+  release."0.2.3".sha256 = "0p9mr8g1qma6h10qf7014dv98ln90dfkwn76ynagpww7qap8s966";
+
+  inherit version;
+  defaultVersion = with versions; switch [ coq.version mathcomp.version ]  [
+      { cases = [ (isGe "8.13") (isGe "1.12.0") ];      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.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"; }
+    ] null;
+
+  propagatedBuildInputs =
+    [ mathcomp.ssreflect mathcomp.field
+      mathcomp-finmap mathcomp-bigenough mathcomp-real-closed ];
+
+  meta = {
+    description = "Analysis library compatible with Mathematical Components";
+    maintainers = [ maintainers.cohencyril ];
+    license = licenses.cecill-c;
+  };
+}; in
+mca.overrideAttrs (o:
+  let ext = { propagatedBuildInputs = o.propagatedBuildInputs
+                                      ++ [ hierarchy-builder ]; };
+  in with versions; switch o.version [
+    {case = "dev";        out = ext;}
+    {case = isGe "0.3.4"; out = ext;}
+  ] {}
+)
--- a/pkgs/development/coq-modules/mathcomp-bigenough/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-bigenough/default.nix
@ -0,0 +1,25 @@
+{ coq, mkCoqDerivation, mathcomp, lib, version ? null }:
+
+with lib; mkCoqDerivation {
+
+  namePrefix = [ "coq" "mathcomp" ];
+  pname = "bigenough";
+  owner = "math-comp";
+
+  release = {
+    "1.0.0".sha256 = "10g0gp3hk7wri7lijkrqna263346wwf6a3hbd4qr9gn8hmsx70wg";
+    "1.0.1".sha256 = "sha256:02f4dv4rz72liciwxb2k7acwx6lgqz4381mqyq5854p3nbyn06aw";
+  };
+  inherit version;
+  defaultVersion = with versions; switch coq.version [
+    { case = range "8.10" "8.15"; out = "1.0.1"; }
+    { case = range "8.5"  "8.14"; out = "1.0.0"; }
+  ] null;
+
+  propagatedBuildInputs = [ mathcomp.ssreflect ];
+
+  meta = {
+    description = "A small library to do epsilon - N reasonning";
+    license = licenses.cecill-b;
+  };
+}
--- a/pkgs/development/coq-modules/mathcomp-finmap/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-finmap/default.nix
@ -0,0 +1,36 @@
+{ coq, mkCoqDerivation, mathcomp, lib, version ? null }:
+
+with lib; mkCoqDerivation {
+
+  namePrefix = [ "coq" "mathcomp" ];
+  pname = "finmap";
+  owner = "math-comp";
+  inherit version;
+  defaultVersion = with versions; switch [ coq.version mathcomp.version ]  [
+      { 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"; }
+      { cases = [ (range "8.7" "8.11.0") (range "1.8" "1.10") ];  out = "1.4.0"; }
+      { cases = [ (range "8.7" "8.11.0") (range "1.8" "1.10") ];  out = "1.3.4"; }
+      { cases = [ (range "8.7" "8.9")    "1.7.0" ];               out = "1.1.0"; }
+      { cases = [ (range "8.6" "8.7")    (range "1.6.1" "1.7") ]; out = "1.0.0"; }
+    ] null;
+  release = {
+    "1.5.1".sha256          = "0ryfml4pf1dfya16d8ma80favasmrygvspvb923n06kfw9v986j7";
+    "1.5.0".sha256          = "0vx9n1fi23592b3hv5p5ycy7mxc8qh1y5q05aksfwbzkk5zjkwnq";
+    "1.4.1".sha256          = "0kx4nx24dml1igk0w0qijmw221r5bgxhwhl5qicnxp7ab3c35s8p";
+    "1.4.0+coq-8.11".sha256 = "1fd00ihyx0kzq5fblh9vr8s5mr1kg7p6pk11c4gr8svl1n69ppmb";
+    "1.4.0".sha256          = "0mp82mcmrs424ff1vj3cvd8353r9vcap027h3p0iprr1vkkwjbzd";
+    "1.3.4".sha256          = "0f5a62ljhixy5d7gsnwd66gf054l26k3m79fb8nz40i2mgp6l9ii";
+    "1.2.1".sha256          = "0jryb5dq8js3imbmwrxignlk5zh8gwfb1wr4b1s7jbwz410vp7zf";
+    "1.1.0".sha256          = "05df59v3na8jhpsfp7hq3niam6asgcaipg2wngnzxzqnl86srp2a";
+    "1.0.0".sha256          = "0sah7k9qm8sw17cgd02f0x84hki8vj8kdz7h15i7rmz08rj0whpa";
+  };
+
+  propagatedBuildInputs = [ mathcomp.ssreflect ];
+
+  meta = {
+    description = "A finset and finmap library";
+    license = licenses.cecill-b;
+  };
+}
--- a/pkgs/development/coq-modules/mathcomp-real-closed/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-real-closed/default.nix
@ -0,0 +1,40 @@
+{ coq, mkCoqDerivation, mathcomp, mathcomp-bigenough,
+  lib, version ? null }:
+
+with lib; mkCoqDerivation {
+
+  namePrefix = [ "coq" "mathcomp" ];
+  pname = "real-closed";
+  owner = "math-comp";
+  inherit version;
+  release = {
+    "1.1.2".sha256 = "0907x4nf7nnvn764q3x9lx41g74rilvq5cki5ziwgpsdgb98pppn";
+    "1.1.1".sha256 = "0ksjscrgq1i79vys4zrmgvzy2y4ylxa8wdsf4kih63apw6v5ws6b";
+    "1.0.5".sha256 = "0q8nkxr9fba4naylr5xk7hfxsqzq2pvwlg1j0xxlhlgr3fmlavg2";
+    "1.0.4".sha256 = "058v9dj973h9kfhqmvcy9a6xhhxzljr90cf99hdfcdx68fi2ha1b";
+    "1.0.3".sha256 = "1xbzkzqgw5p42dx1liy6wy8lzdk39zwd6j14fwvv5735k660z7yb";
+    "1.0.1".sha256 = "0j81gkjbza5vg89v4n9z598mfdbql416963rj4b8fzm7dp2r4rxg";
+  };
+
+  defaultVersion = with versions; switch [ coq.version mathcomp.version ]  [
+      { cases = [ (isGe "8.10")  (isGe "1.12.0") ]; out = "1.1.2"; }
+      { cases = [ (isGe "8.7")   "1.11.0" ]; out = "1.1.1"; }
+      { cases = [ (isGe "8.7")   (range "1.9.0" "1.10.0") ]; out = "1.0.4"; }
+      { cases = [ (isGe "8.7")   "1.8.0"  ]; out = "1.0.3"; }
+      { cases = [ (isGe "8.7")   "1.7.0"  ]; out = "1.0.1"; }
+    ] null;
+
+  propagatedBuildInputs = [
+    mathcomp.ssreflect
+    mathcomp.algebra
+    mathcomp.field
+    mathcomp.fingroup
+    mathcomp.solvable
+    mathcomp-bigenough
+  ];
+
+  meta = {
+    description = "Mathematical Components Library on real closed fields";
+    license = licenses.cecill-c;
+  };
+}
--- a/pkgs/development/coq-modules/mathcomp-tarjan/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-tarjan/default.nix
@ -0,0 +1,22 @@
+{ coq, mkCoqDerivation, mathcomp-ssreflect, mathcomp-fingroup,
+  lib, version ? null }@args:
+with lib; mkCoqDerivation {
+
+  namePrefix = [ "coq" "mathcomp" ];
+  pname = "tarjan";
+  owner = "math-comp";
+
+  inherit version;
+  defaultVersion = with versions;
+    switch [ coq.version mathcomp-ssreflect.version ] [{
+      cases = [ (range "8.10" "8.15") (isGe "1.12.0") ]; out = "1.0.0";
+  }] null;
+  release."1.0.0".sha256 = "sha256:0r459r0makshzwlygw6kd4lpvdjc43b3x5y9aa8x77f2z5gymjq1";
+
+  propagatedBuildInputs = [ mathcomp-ssreflect mathcomp-fingroup ];
+
+  meta = {
+    description = "Proofs of Tarjan and Kosaraju connected components algorithms";
+    license = licenses.cecill-b;
+  };
+}
--- a/pkgs/development/coq-modules/mathcomp-word/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-word/default.nix
@ -0,0 +1,28 @@
+{ coq, mkCoqDerivation, mathcomp, lib, version ? null }:
+
+with lib;
+mkCoqDerivation {
+  namePrefix = [ "coq" "mathcomp" ];
+  pname = "word";
+  owner = "jasmin-lang";
+  repo = "coqword";
+  useDune2 = true;
+
+  releaseRev = v: "v${v}";
+
+  release."1.1".sha256 = "sha256:0jb28vgkr4xpg9d6k85rq7abpx5ch612iw9ps5w8q80q1jpjlc4z";
+  release."1.0".sha256 = "sha256:0703m97rnivcbc7vvbd9rl2dxs6l8n52cbykynw61c6w9rhxspcg";
+
+  inherit version;
+  defaultVersion = with versions; switch [ coq.version mathcomp.version ] [
+    { cases = [ (range "8.12" "8.15") (isGe "1.12") ]; out = "1.1"; }
+  ] null;
+
+  propagatedBuildInputs = [ mathcomp.algebra mathcomp.ssreflect mathcomp.fingroup ];
+
+  meta = {
+    description = "Yet Another Coq Library on Machine Words";
+    maintainers = [ maintainers.vbgl ];
+    license = licenses.mit;
+  };
+}
--- a/pkgs/development/coq-modules/mathcomp-zify/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-zify/default.nix
@ -0,0 +1,24 @@
+{ lib, mkCoqDerivation, coq, mathcomp-algebra, mathcomp-ssreflect,  mathcomp-fingroup, version ? null }:
+
+with lib; mkCoqDerivation rec {
+  namePrefix = [ "coq" "mathcomp" ];
+  pname = "zify";
+  repo = "mczify";
+  owner = "math-comp";
+  inherit version;
+
+  defaultVersion = with versions;
+     switch [ coq.coq-version mathcomp-algebra.version ] [
+       { cases = [ (range "8.13" "8.15") (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";
+
+  propagatedBuildInputs = [ mathcomp-algebra mathcomp-ssreflect mathcomp-fingroup ];
+
+  meta = {
+    description = "Micromega tactics for Mathematical Components";
+    maintainers = with maintainers; [ cohencyril ];
+  };
+}
--- a/pkgs/development/coq-modules/mathcomp/default.nix
+++ b/pkgs/development/coq-modules/mathcomp/default.nix
@ -0,0 +1,121 @@
+############################################################################
+# This file mainly provides the `mathcomp` derivation, which is            #
+# essentially a meta-package containing all core mathcomp libraries        #
+# (ssreflect fingroup algebra solvable field character). They can be       #
+# accessed individually through the passthrough attributes of mathcomp     #
+# bearing the same names (mathcomp.ssreflect, etc).                        #
+############################################################################
+# Compiling a custom version of mathcomp using `mathcomp.override`.        #
+# This is the replacement for the former `mathcomp_ config` function.      #
+# See the documentation at doc/languages-frameworks/coq.section.md.        #
+############################################################################
+
+{ lib, ncurses, graphviz, lua, fetchzip,
+  mkCoqDerivation, recurseIntoAttrs, withDoc ? false, single ? false,
+  coqPackages, coq, version ? null }@args:
+with builtins // lib;
+let
+  repo  = "math-comp";
+  owner = "math-comp";
+  withDoc = single && (args.withDoc or false);
+  defaultVersion = with versions; switch coq.coq-version [
+      { case = isGe  "8.11";        out = "1.14.0"; }
+      { case = range "8.11" "8.15"; out = "1.13.0"; }
+      { case = range "8.10" "8.13"; out = "1.12.0"; }
+      { case = range "8.7"  "8.12"; out = "1.11.0"; }
+      { case = range "8.7" "8.11";  out = "1.10.0"; }
+      { case = range "8.7" "8.11";  out = "1.9.0";  }
+      { case = range "8.7" "8.9";   out = "1.8.0";  }
+      { case = range "8.6" "8.9";   out = "1.7.0";  }
+      { case = range "8.5" "8.7";   out = "1.6.4";  }
+    ] null;
+  release = {
+    "1.14.0".sha256 = "07yamlp1c0g5nahkd2gpfhammcca74ga2s6qr7a3wm6y6j5pivk9";
+    "1.13.0".sha256 = "0j4cz2y1r1aw79snkcf1pmicgzf8swbaf9ippz0vg99a572zqzri";
+    "1.12.0".sha256 = "1ccfny1vwgmdl91kz5xlmhq4wz078xm4z5wpd0jy5rn890dx03wp";
+    "1.11.0".sha256 = "06a71d196wd5k4wg7khwqb7j7ifr7garhwkd54s86i0j7d6nhl3c";
+    "1.10.0".sha256 = "1b9m6pwxxyivw7rgx82gn5kmgv2mfv3h3y0mmjcjfypi8ydkrlbv";
+    "1.9.0".sha256  = "0lid9zaazdi3d38l8042lczb02pw5m9wq0yysiilx891hgq2p81r";
+    "1.8.0".sha256  = "07l40is389ih8bi525gpqs3qp4yb2kl11r9c8ynk1ifpjzpnabwp";
+    "1.7.0".sha256  = "0wnhj9nqpx2bw6n1l4i8jgrw3pjajvckvj3lr4vzjb3my2lbxdd1";
+    "1.6.4".sha256  = "09ww48qbjsvpjmy1g9yhm0rrkq800ffq21p6fjkbwd34qvd82raz";
+    "1.6.1".sha256  = "1ilw6vm4dlsdv9cd7kmf0vfrh2kkzr45wrqr8m37miy0byzr4p9i";
+  };
+  releaseRev = v: "mathcomp-${v}";
+
+  # list of core mathcomp packages sorted by dependency order
+  packages = [ "ssreflect" "fingroup" "algebra" "solvable" "field" "character" "all" ];
+
+  mathcomp_ = package: let
+      mathcomp-deps = if package == "single" then []
+        else map mathcomp_ (head (splitList (pred.equal package) packages));
+      pkgpath = if package == "single" then "mathcomp" else "mathcomp/${package}";
+      pname = if package == "single" then "mathcomp" else "mathcomp-${package}";
+      pkgallMake = ''
+        echo "all.v"  > Make
+        echo "-I ." >>   Make
+        echo "-R . mathcomp.all" >> Make
+      '';
+      derivation = mkCoqDerivation ({
+        inherit version pname defaultVersion release releaseRev repo owner;
+
+        mlPlugin = versions.isLe "8.6" coq.coq-version;
+        nativeBuildInputs = optionals withDoc [ graphviz lua ];
+        buildInputs = [ ncurses ];
+        propagatedBuildInputs = mathcomp-deps;
+
+        buildFlags = optional withDoc "doc";
+
+        preBuild = ''
+          if [[ -f etc/utils/ssrcoqdep ]]
+          then patchShebangs etc/utils/ssrcoqdep
+          fi
+          if [[ -f etc/buildlibgraph ]]
+          then patchShebangs etc/buildlibgraph
+          fi
+        '' + ''
+          cd ${pkgpath}
+        '' + optionalString (package == "all") pkgallMake;
+
+        meta = {
+          homepage    = "https://math-comp.github.io/";
+          license     = licenses.cecill-b;
+          maintainers = with maintainers; [ vbgl jwiegley cohencyril ];
+        };
+      } // optionalAttrs (package != "single")
+        { passthru = genAttrs packages mathcomp_; }
+        // optionalAttrs withDoc {
+            htmldoc_template =
+              fetchzip {
+                url = "https://github.com/math-comp/math-comp.github.io/archive/doc-1.12.0.zip";
+                sha256 = "0y1352ha2yy6k2dl375sb1r68r1qi9dyyy7dyzj5lp9hxhhq69x8";
+              };
+            postBuild = ''
+              cp -rf _build_doc/* .
+              rm -r _build_doc
+            '';
+            postInstall =
+              let tgt = "$out/share/coq/${coq.coq-version}/"; in
+              optionalString withDoc ''
+              mkdir -p ${tgt}
+              cp -r htmldoc ${tgt}
+              cp -r $htmldoc_template/htmldoc_template/* ${tgt}/htmldoc/
+            '';
+            buildTargets = "doc";
+            extraInstallFlags = [ "-f Makefile.coq" ];
+          });
+    patched-derivation1 = derivation.overrideAttrs (o:
+      optionalAttrs (o.pname != null && o.pname == "mathcomp-all" &&
+         o.version != null && o.version != "dev" && versions.isLt "1.7" o.version)
+      { preBuild = ""; buildPhase = ""; installPhase = "echo doing nothing"; }
+    );
+    patched-derivation = patched-derivation1.overrideAttrs (o:
+      optionalAttrs (versions.isLe "8.7" coq.coq-version ||
+            (o.version != "dev" && versions.isLe "1.7" o.version))
+      {
+        installFlags = o.installFlags ++ [ "-f Makefile.coq" ];
+      }
+    );
+    in patched-derivation;
+in
+mathcomp_ (if single then "single" else "all")
--- a/pkgs/development/coq-modules/metacoq/default.nix
+++ b/pkgs/development/coq-modules/metacoq/default.nix
@ -0,0 +1,74 @@
+{ lib, fetchzip,
+  mkCoqDerivation, recurseIntoAttrs,  single ? false,
+  coqPackages, coq, equations, version ? null }@args:
+with builtins // lib;
+let
+  repo  = "metacoq";
+  owner = "MetaCoq";
+  defaultVersion = with versions; switch coq.coq-version [
+      { case = "8.11"; out = "1.0-beta2-8.11"; }
+      { case = "8.12"; out = "1.0-beta2-8.12"; }
+      # Do not provide 8.13 because it does not compile with equations 1.3 provided by default (only 1.2.3)
+      # { case = "8.13"; out = "1.0-beta2-8.13"; }
+    ] null;
+  release = {
+    "1.0-beta2-8.11".sha256 = "sha256-I9YNk5Di6Udvq5/xpLSNflfjRyRH8fMnRzbo3uhpXNs=";
+    "1.0-beta2-8.12".sha256 = "sha256-I8gpmU9rUQJh0qfp5KOgDNscVvCybm5zX4TINxO1TVA=";
+    "1.0-beta2-8.13".sha256 = "sha256-IC56/lEDaAylUbMCfG/3cqOBZniEQk8jmI053DBO5l8=";
+  };
+  releaseRev = v: "v${v}";
+
+  # list of core metacoq packages sorted by dependency order
+  packages = [ "template-coq" "pcuic" "safechecker" "erasure" "all" ];
+
+  template-coq = metacoq_ "template-coq";
+
+  metacoq_ = package: let
+      metacoq-deps = if package == "single" then []
+        else map metacoq_ (head (splitList (pred.equal package) packages));
+      pkgpath = if package == "single" then "./" else "./${package}";
+      pname = if package == "all" then "metacoq" else "metacoq-${package}";
+      pkgallMake = ''
+          mkdir all
+          echo "all:" > all/Makefile
+          echo "install:" >> all/Makefile
+        '' ;
+      derivation = mkCoqDerivation ({
+        inherit version pname defaultVersion release releaseRev repo owner;
+
+        mlPlugin = true;
+        propagatedBuildInputs = [ equations coq.ocamlPackages.zarith ] ++ metacoq-deps;
+
+        patchPhase =  ''
+          patchShebangs ./configure.sh
+          patchShebangs ./template-coq/update_plugin.sh
+          patchShebangs ./template-coq/gen-src/to-lower.sh
+          patchShebangs ./pcuic/clean_extraction.sh
+          patchShebangs ./safechecker/clean_extraction.sh
+          patchShebangs ./erasure/clean_extraction.sh
+          echo "CAMLFLAGS+=-w -60 # Unused module" >> ./safechecker/Makefile.plugin.local
+          sed -i -e 's/mv $i $newi;/mv $i tmp; mv tmp $newi;/' ./template-coq/gen-src/to-lower.sh ./pcuic/clean_extraction.sh ./safechecker/clean_extraction.sh ./erasure/clean_extraction.sh
+        '' ;
+
+        configurePhase = optionalString (package == "all") pkgallMake + ''
+          touch ${pkgpath}/metacoq-config
+        '' + optionalString (elem package ["safechecker" "erasure"]) ''
+          echo  "-I ${template-coq}/lib/coq/${coq.coq-version}/user-contrib/MetaCoq/Template/" > ${pkgpath}/metacoq-config
+        '' + optionalString (package == "single") ''
+          ./configure.sh local
+        '';
+
+        preBuild = ''
+          cd ${pkgpath}
+        '' ;
+
+        meta = {
+          homepage    = "https://metacoq.github.io/";
+          license     = licenses.mit;
+          maintainers = with maintainers; [ cohencyril ];
+        };
+      } // optionalAttrs (package != "single")
+        { passthru = genAttrs packages metacoq_; });
+    in derivation;
+in
+metacoq_ (if single then "single" else "all")
--- a/pkgs/development/coq-modules/metalib/default.nix
+++ b/pkgs/development/coq-modules/metalib/default.nix
@ -0,0 +1,21 @@
+{ lib, mkCoqDerivation, coq, version ? null }:
+
+with lib; mkCoqDerivation {
+  pname = "metalib";
+  owner = "plclub";
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = range "8.14" "8.15"; out = "8.15"; }
+    { case = range "8.10" "8.13"; out = "8.10"; }
+  ] null;
+  releaseRev = v: "coq${v}";
+  release."8.15".sha256 = "0wbp058zwa4bkdjj38aysy2g1avf9nrh8q23a3dil0q00qczi616";
+  release."8.10".sha256 = "0wbypc05d2lqfm9qaw98ynr5yc1p0ipsvyc3bh1rk9nz7zwirmjs";
+
+  sourceRoot = "source/Metalib";
+
+  meta = {
+    license = licenses.mit;
+    maintainers = [ maintainers.jwiegley ];
+  };
+}
--- a/pkgs/development/coq-modules/multinomials/default.nix
+++ b/pkgs/development/coq-modules/multinomials/default.nix
@ -0,0 +1,48 @@
+{ coq, mkCoqDerivation, mathcomp, mathcomp-finmap, mathcomp-bigenough,
+  lib, version ? null, useDune2 ? false }@args:
+with lib; mkCoqDerivation {
+
+  namePrefix = [ "coq" "mathcomp" ];
+  pname = "multinomials";
+
+  owner = "math-comp";
+
+  inherit version;
+  defaultVersion =  with versions; switch [ coq.version mathcomp.version ] [
+      { cases = [ (isGe "8.10") (isGe "1.12.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"; }
+      { cases = [ (range "8.7" "8.10")  (range "1.8" "1.10") ]; out = "1.4"; }
+      { cases = [ "8.6"                 (range "1.6" "1.7") ];  out = "1.1"; }
+    ] null;
+  release = {
+    "1.5.5".sha256 = "sha256-VdXA51vr7DZl/wT/15YYMywdD7Gh91dMP9t7ij47qNQ=";
+    "1.5.4".sha256 = "0s4sbh4y88l125hdxahr56325hdhxxdmqmrz7vv8524llyv3fciq";
+    "1.5.3".sha256 = "1462x40y2qydjd2wcg8r6qr8cx3xv4ixzh2h8vp9h7arylkja1qd";
+    "1.5.2".sha256 = "15aspf3jfykp1xgsxf8knqkxv8aav2p39c2fyirw7pwsfbsv2c4s";
+    "1.5.1".sha256 = "13nlfm2wqripaq671gakz5mn4r0xwm0646araxv0nh455p9ndjs3";
+    "1.5.0".sha256 = "064rvc0x5g7y1a0nip6ic91vzmq52alf6in2bc2dmss6dmzv90hw";
+    "1.5.0".rev    = "1.5";
+    "1.4".sha256   = "0vnkirs8iqsv8s59yx1fvg1nkwnzydl42z3scya1xp1b48qkgn0p";
+    "1.3".sha256   = "0l3vi5n094nx3qmy66hsv867fnqm196r8v605kpk24gl0aa57wh4";
+    "1.2".sha256   = "1mh1w339dslgv4f810xr1b8v2w7rpx6fgk9pz96q0fyq49fw2xcq";
+    "1.1".sha256   = "1q8alsm89wkc0lhcvxlyn0pd8rbl2nnxg81zyrabpz610qqjqc3s";
+    "1.0".sha256   = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m";
+  };
+
+  useDune2ifVersion = v: versions.isGe "1.5.3" v || v == "dev";
+
+  preConfigure = ''
+    patchShebangs configure || true
+  '';
+
+  propagatedBuildInputs =
+    [ mathcomp.ssreflect mathcomp.algebra mathcomp-finmap mathcomp.fingroup mathcomp-bigenough ];
+
+  meta = {
+    description = "A Coq/SSReflect Library for Monoidal Rings and Multinomials";
+    license = licenses.cecill-c;
+  };
+}
+// optionalAttrs (args?useDune2) { inherit useDune2; }
--- a/pkgs/development/coq-modules/odd-order/default.nix
+++ b/pkgs/development/coq-modules/odd-order/default.nix
@ -0,0 +1,35 @@
+{ lib, mkCoqDerivation, mathcomp, version ? null }:
+with lib;
+
+mkCoqDerivation {
+  pname = "odd-order";
+  owner = "math-comp";
+
+  release."1.13.0".rev    = "mathcomp-odd-order.1.13.0";
+  release."1.13.0".sha256 = "sha256-EzNKR/JzM8T17sMhPhgZNs14e50X4dY3OwFi133IsT0=";
+  release."1.12.0".rev    = "mathcomp-odd-order.1.12.0";
+  release."1.12.0".sha256 = "sha256-omsfdc294CxKAHNMMeqJCcVimvyRCHgxcQ4NJOWSfNM=";
+
+  inherit version;
+  defaultVersion = with versions; switch mathcomp.character.version [
+    { case = (range "1.12.0" "1.14.0"); out = "1.13.0"; }
+    { case = (range "1.10.0" "1.12.0"); out = "1.12.0"; }
+  ] null;
+
+  propagatedBuildInputs = [
+    mathcomp.character
+    mathcomp.ssreflect
+    mathcomp.fingroup
+    mathcomp.algebra
+    mathcomp.solvable
+    mathcomp.field
+    mathcomp.all
+  ];
+
+  meta = {
+    description = "Formal proof of the Odd Order Theorem";
+    maintainers = with maintainers; [ siraben ];
+    license = licenses.cecill-b;
+    platforms = platforms.unix;
+  };
+}
--- a/pkgs/development/coq-modules/paco/default.nix
+++ b/pkgs/development/coq-modules/paco/default.nix
@ -0,0 +1,32 @@
+{ lib, mkCoqDerivation, coq, version ? null }:
+
+with lib; mkCoqDerivation {
+  pname = "paco";
+  owner = "snu-sf";
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = range "8.12" "8.15"; out = "4.1.2"; }
+    { case = range "8.9" "8.13"; out = "4.1.1"; }
+    { case = range "8.6" "8.13"; out = "4.0.2"; }
+    { case = isEq "8.5";         out = "1.2.8"; }
+  ] null;
+  release."4.1.2".sha256 = "sha256:1l8mwakqp4wnppsldl8wp2j24h1jvadnvrsgf35xnvdyygypjp2v";
+  release."4.1.1".sha256 = "1qap8cyv649lr1s11r7h5jzdjd4hsna8kph15qy5fw24h5nx6byy";
+  release."4.0.2".sha256 = "1q96bsxclqx84xn5vkid501jkwlc1p6fhb8szrlrp82zglj58b0b";
+  release."1.2.8".sha256 = "05fskx5x1qgaf9qv626m38y5izichzzqc7g2rglzrkygbskrrwsb";
+  releaseRev = v: "v${v}";
+
+  preBuild = "cd src";
+
+  installPhase = ''
+    COQLIB=$out/lib/coq/${coq.coq-version}/
+    mkdir -p $COQLIB/user-contrib/Paco
+    cp -pR *.vo $COQLIB/user-contrib/Paco
+  '';
+
+  meta = {
+    homepage = "http://plv.mpi-sws.org/paco/";
+    description = "A Coq library implementing parameterized coinduction";
+    maintainers = with maintainers; [ jwiegley ptival ];
+  };
+}
--- a/pkgs/development/coq-modules/paramcoq/default.nix
+++ b/pkgs/development/coq-modules/paramcoq/default.nix
@ -0,0 +1,31 @@
+{ lib, mkCoqDerivation, coq, version ? null }:
+
+with lib; mkCoqDerivation {
+  pname = "paramcoq";
+  inherit version;
+  defaultVersion = with versions; switch coq.version [
+    { case = range "8.10" "8.15"; out = "1.1.3+coq${coq.coq-version}"; }
+    { case = range "8.7"  "8.13"; out = "1.1.2+coq${coq.coq-version}"; }
+  ] null;
+  displayVersion = { paramcoq = "..."; };
+  release."1.1.3+coq8.15".sha256 = "0sl7ihznwz05d2x2v78w1zd4q55c1sgy06vxasbcls4v2pkw53hl";
+  release."1.1.3+coq8.14".sha256 = "00zqq9dc2p5v0ib1jgizl25xkwxrs9mrlylvy0zvb96dpridjc71";
+  release."1.1.3+coq8.13".sha256 = "06ndly736k4pmdn4baqa7fblp6lx7a9pxm9gvz1vzd6ic51825wp";
+  release."1.1.3+coq8.12".sha256 = "sha256:10j23ws8ymqpxhapni75sxbzz0dl4n9sgasrx618i7s7b705y2rh";
+  release."1.1.3+coq8.11".sha256 = "sha256:1wbvcmkr7q106418bvvc2rj2d7s03wdhhxar0hicy1rr267w2bs6";
+  release."1.1.3+coq8.10".sha256 = "sha256:0kv3k3y2fck1qz83pqmihyh98swicnpx0n6fzkis1n2g39qjfz91";
+  release."1.1.2+coq8.13".sha256 = "02vnf8p04ynf3qk8myvjzsbga15395235mpdpj54pvxis3h5qq22";
+  release."1.1.2+coq8.12".sha256 = "0qd72r45if4h7c256qdfiimv75zyrs0w0xqij3m866jxaq591v4i";
+  release."1.1.2+coq8.11".sha256 = "09c6813988nvq4fpa45s33k70plnhxsblhm7cxxkg0i37mhvigsa";
+  release."1.1.2+coq8.10".sha256 = "1lq1mw15w4yky79qg3rm0mpzqi2ir51b6ak04ismrdr7ixky49y8";
+  release."1.1.2+coq8.9".sha256  = "1jjzgpff09xjn9kgp7w69r096jkj0x2ksng3pawrmhmn7clwivbk";
+  release."1.1.2+coq8.8".sha256  = "0rc4lshqvnfdsph98gnscvpmlirs9wx91qcvffggg73xw0p1g9s0";
+  release."1.1.2+coq8.7".sha256  = "09n0ky7ldb24by7yf5j3hv410h85x50ksilf7qacl7xglj4gy5hj";
+  releaseRev = v: "v${v}";
+  mlPlugin = true;
+  meta = {
+    description = "Coq plugin for parametricity";
+    license = licenses.mit;
+    maintainers = [ maintainers.vbgl ];
+  };
+}
--- a/pkgs/development/coq-modules/parsec/default.nix
+++ b/pkgs/development/coq-modules/parsec/default.nix
@ -0,0 +1,26 @@
+{ lib, mkCoqDerivation, coq, ceres, coq-ext-lib, version ? null }:
+
+with lib;
+mkCoqDerivation {
+
+  pname = "parsec";
+  repo = "coq-parsec";
+  owner = "liyishuai";
+
+  propagatedBuildInputs = [ ceres coq-ext-lib ];
+  releaseRev = (v: "v${v}");
+
+  inherit version;
+  defaultVersion = with versions; switch coq.version [
+    { case = range "8.12" "8.15"; out = "0.1.1"; }
+    { case = range "8.12" "8.13"; out = "0.1.0"; }
+  ] null;
+  release."0.1.1".sha256 = "sha256:1c0l18s68pzd4c8i3jimh2yz0pqm4g38pca4bm7fr18r8xmqf189";
+  release."0.1.0".sha256 = "sha256:01avfcqirz2b9wjzi9iywbhz9szybpnnj3672dgkfsimyg9jgnsr";
+
+  meta = {
+    description = "Library for serialization to S-expressions";
+    license = licenses.bsd3;
+    maintainers = with maintainers; [ Zimmi48 ];
+  };
+}
--- a/pkgs/development/coq-modules/pocklington/default.nix
+++ b/pkgs/development/coq-modules/pocklington/default.nix
@ -0,0 +1,22 @@
+{ lib, mkCoqDerivation, coq, version ? null }:
+with lib;
+
+mkCoqDerivation {
+  pname = "pocklington";
+  owner = "coq-community";
+
+  release."8.12.0".rev    = "v8.12.0";
+  release."8.12.0".sha256 = "sha256-0xBrw9+4g14niYdNqp0nx00fPJoSSnaDSDEaIVpPfjs=";
+
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = isGe "8.7"; out = "8.12.0"; }
+  ] null;
+
+  meta = {
+    description = "Pocklington's criterion for primality in Coq";
+    maintainers = with maintainers; [ siraben ];
+    license = licenses.mit;
+    platforms = platforms.unix;
+  };
+}
--- a/pkgs/development/coq-modules/reglang/default.nix
+++ b/pkgs/development/coq-modules/reglang/default.nix
@ -0,0 +1,25 @@
+{ lib, mkCoqDerivation, coq, ssreflect, version ? null }:
+with lib;
+
+mkCoqDerivation {
+  pname = "reglang";
+
+  releaseRev = v: "v${v}";
+
+  release."1.1.2".sha256 = "sha256-SEnMilLNxh6a3oiDNGLaBr8quQ/nO2T9Fwdf/1il2Yk=";
+
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = range "8.10" "8.15"; out = "1.1.2"; }
+  ] null;
+
+
+  propagatedBuildInputs = [ ssreflect ];
+
+  meta = {
+    description = "Regular Language Representations in Coq";
+    maintainers = with maintainers; [ siraben ];
+    license = licenses.cecill-b;
+    platforms = platforms.unix;
+  };
+}
--- a/pkgs/development/coq-modules/relation-algebra/default.nix
+++ b/pkgs/development/coq-modules/relation-algebra/default.nix
@ -0,0 +1,42 @@
+{ lib, mkCoqDerivation, coq, aac-tactics, mathcomp, version ? null }:
+with lib;
+
+mkCoqDerivation {
+  pname = "relation-algebra";
+  owner = "damien-pous";
+
+  releaseRev = v:
+    if versions.isGe "1.7.6" v
+    then "v.${v}"
+    else "v${v}";
+
+  release."1.7.7".sha256 = "sha256:1dff3id6nypl2alhk9rcifj3dab0j78dym05blc525lawsmc26l2";
+  release."1.7.6".sha256 = "sha256:02gsj06zcy9zgd0h1ibqspwfiwm36pkkgg9cz37k4bxzcapxcr6w";
+  release."1.7.5".sha256 = "sha256-XdO8agoJmNXPv8Ho+KTlLCB4oRlQsb0w06aM9M16ZBU=";
+  release."1.7.4".sha256 = "sha256-o+v2CIAa2+9tJ/V8DneDTf4k31KMHycgMBLaQ+A4ufM=";
+  release."1.7.3".sha256 = "sha256-4feSNfi7h4Yhwn5L+9KP9K1S7HCPvsvaVWwoQSTFvos=";
+  release."1.7.2".sha256 = "sha256-f4oNjXspNMEz3AvhIeYO3avbUa1AThoC9DbcHMb5A2o=";
+  release."1.7.1".sha256 = "sha256-WWVMcR6z8rT4wzZPb8SlaVWGe7NC8gScPqawd7bltQA=";
+
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = isEq "8.15"; out = "1.7.7"; }
+    { case = isEq "8.14"; out = "1.7.6"; }
+    { 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;
+
+  propagatedBuildInputs = [ aac-tactics mathcomp.ssreflect ];
+
+  meta = {
+    description = "Relation algebra library for Coq";
+    maintainers = with maintainers; [ siraben ];
+    license = licenses.gpl3Plus;
+    platforms = platforms.unix;
+  };
+}
--- a/pkgs/development/coq-modules/semantics/default.nix
+++ b/pkgs/development/coq-modules/semantics/default.nix
@ -0,0 +1,47 @@
+{ lib, mkCoqDerivation, coq, version ? null }:
+with lib;
+
+mkCoqDerivation rec {
+  pname = "semantics";
+  owner = "coq-community";
+  releaseRev = v: "v${v}";
+
+  release."8.14.0".sha256 = "sha256-TB12C3hX9XucbsXr+UL+8jM19NOFXASW/lcytwy6uVE=";
+  release."8.13.0".sha256 = "sha256-8bDr/Ovl6s8BFaRcHeS5H33/K/pYdeKfSN+krVuKulQ=";
+  release."8.11.1".sha256 = "sha256-jTPgcXSNn1G2mMDC7ocFcmqs8svB7Yo1emXP15iuxiU=";
+  release."8.9.0".sha256 = "sha256-UBsvzlDEZsZsVkbUI0GbFEhpxnnLCiaqlqDyWVC5I6s=";
+  release."8.8.0".sha256 = "sha256-k2nQyNw9KT3wY7bGy8KGILF44sLxkBYqdFpzFE9fgyw=";
+  release."8.7.0".sha256 = "sha256-k2nQyNw9KT3wY7bGy8KGILF44sLxkBYqdFpzFE9fgyw=";
+  release."8.6.0".sha256 = "sha256-GltkGQ3tJqUPAbdDkqqvKLLhMOap50XvGaCkjshiNdY=";
+
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { 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"; }
+    { case = "8.6"; out = "8.6.0"; }
+  ] null;
+
+  mlPlugin = true;
+  nativeBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]);
+  propagatedBuildInputs = (with coq.ocamlPackages; [ num ]);
+
+  postPatch = ''
+    for p in Make Makefile.coq.local
+    do
+      substituteInPlace $p --replace "-libs nums" "-use-ocamlfind -package num" || true
+    done
+  '';
+
+  meta = {
+    description = "A survey of programming language semantics styles in Coq";
+    longDescription = ''
+      A survey of semantics styles in Coq, from natural semantics through
+      structural operational, axiomatic, and denotational semantics, to
+      abstract interpretation
+    '';
+    maintainers = with maintainers; [ siraben ];
+    license = licenses.mit;
+  };
+}
--- a/pkgs/development/coq-modules/serapi/8.10.0+0.7.2.patch
+++ b/pkgs/development/coq-modules/serapi/8.10.0+0.7.2.patch
@ -0,0 +1,34 @@
+diff --git a/serapi/serapi_paths.ml b/serapi/serapi_paths.ml
+index 17cbb98..1fd85a0 100644
+--- a/serapi/serapi_paths.ml
+++ b/serapi/serapi_paths.ml
+@@ -23,10 +23,10 @@
+ let coq_loadpath_default ~implicit ~coq_path =
+   let open Mltop in
+   let mk_path prefix = coq_path ^ "/" ^ prefix in
+-  let mk_lp ~ml ~root ~dir ~implicit =
+  let mk_lp ~ml ~root ~dir ~implicit ~absolute =
+     { recursive = true;
+       path_spec = VoPath {
+-          unix_path = mk_path dir;
+          unix_path = if absolute then dir else mk_path dir;
+           coq_path  = root;
+           has_ml    = ml;
+           implicit;
+@@ -35,10 +35,12 @@ let coq_loadpath_default ~implicit ~coq_path =
+   (* in 8.8 we can use Libnames.default_* *)
+   let coq_root     = Names.DirPath.make [Libnames.coq_root] in
+   let default_root = Libnames.default_root_prefix in
+-  [mk_lp ~ml:AddRecML ~root:coq_root     ~implicit       ~dir:"plugins";
+-   mk_lp ~ml:AddNoML  ~root:coq_root     ~implicit       ~dir:"theories";
+-   mk_lp ~ml:AddRecML ~root:default_root ~implicit:false ~dir:"user-contrib";
+-  ]
+  [mk_lp ~ml:AddRecML ~root:coq_root     ~implicit       ~dir:"plugins" ~absolute:false;
+   mk_lp ~ml:AddNoML  ~root:coq_root     ~implicit       ~dir:"theories" ~absolute:false;
+   mk_lp ~ml:AddRecML ~root:default_root ~implicit:false ~dir:"user-contrib" ~absolute:false;
+  ] @
+  List.map (fun dir -> mk_lp ~ml:AddRecML ~root:default_root ~implicit:false ~dir ~absolute:true)
+    Envars.coqpath
+ 
+ (******************************************************************************)
+ (* Generate a module name given a file                                        *)
--- a/pkgs/development/coq-modules/serapi/8.11.0+0.11.1.patch
+++ b/pkgs/development/coq-modules/serapi/8.11.0+0.11.1.patch
@ -0,0 +1,33 @@
+diff --git a/serapi/serapi_paths.ml b/serapi/serapi_paths.ml
+index a9c5074..eed92e3 100644
+--- a/serapi/serapi_paths.ml
+++ b/serapi/serapi_paths.ml
+@@ -23,10 +23,10 @@
+ let coq_loadpath_default ~implicit ~coq_path =
+   let open Loadpath in
+   let mk_path prefix = coq_path ^ "/" ^ prefix in
+-  let mk_lp ~ml ~root ~dir ~implicit =
+  let mk_lp ~ml ~root ~dir ~implicit ~absolute =
+     { recursive = true;
+       path_spec = VoPath {
+-          unix_path = mk_path dir;
+          unix_path = if absolute then dir else mk_path dir;
+           coq_path  = root;
+           has_ml    = ml;
+           implicit;
+@@ -35,11 +35,11 @@ let coq_loadpath_default ~implicit ~coq_path =
+   (* in 8.8 we can use Libnames.default_* *)
+   let coq_root     = Names.DirPath.make [Libnames.coq_root] in
+   let default_root = Libnames.default_root_prefix in
+-  [mk_lp ~ml:AddRecML ~root:coq_root     ~implicit       ~dir:"plugins";
+-   mk_lp ~ml:AddNoML  ~root:coq_root     ~implicit       ~dir:"theories";
+-   mk_lp ~ml:AddRecML ~root:default_root ~implicit:false ~dir:"user-contrib";
+  [mk_lp ~ml:AddRecML ~root:coq_root     ~implicit       ~dir:"plugins" ~absolute:false;
+   mk_lp ~ml:AddNoML  ~root:coq_root     ~implicit       ~dir:"theories" ~absolute:false;
+   mk_lp ~ml:AddRecML ~root:default_root ~implicit:false ~dir:"user-contrib" ~absolute:false;
+   ] @
+-  List.map (fun dir -> mk_lp ~ml:AddRecML ~root:default_root ~implicit:false ~dir)
+  List.map (fun dir -> mk_lp ~ml:AddRecML ~root:default_root ~implicit:false ~dir ~absolute:true)
+     Envars.coqpath
+ 
+ (******************************************************************************)
--- a/pkgs/development/coq-modules/serapi/8.12.0+0.12.1.patch
+++ b/pkgs/development/coq-modules/serapi/8.12.0+0.12.1.patch
@ -0,0 +1,29 @@
+diff --git a/serapi/serapi_paths.ml b/serapi/serapi_paths.ml
+index b71fa60..0bec8c2 100644
+--- a/serapi/serapi_paths.ml
+++ b/serapi/serapi_paths.ml
+@@ -24,8 +24,8 @@ let coq_loadpath_default ~implicit ~coq_path =
+   let open Loadpath in
+   let mk_path prefix = coq_path ^ "/" ^ prefix in
+   (* let mk_ml = () in *)
+-  let mk_vo ~has_ml ~coq_path ~dir ~implicit =
+-    { unix_path = mk_path dir
+  let mk_vo ~has_ml ~coq_path ~dir ~implicit ~absolute =
+    { unix_path = if absolute then dir else mk_path dir
+     ; coq_path
+     ; has_ml
+     ; recursive = true
+@@ -40,10 +40,10 @@ let coq_loadpath_default ~implicit ~coq_path =
+     List.map fst plugins_dirs
+   in
+   ml_paths ,
+-  [ mk_vo ~has_ml:false ~coq_path:coq_root     ~implicit       ~dir:"theories"
+-  ; mk_vo ~has_ml:true  ~coq_path:default_root ~implicit:false ~dir:"user-contrib";
+  [ mk_vo ~has_ml:false ~coq_path:coq_root     ~implicit       ~dir:"theories" ~absolute:false
+  ; mk_vo ~has_ml:true  ~coq_path:default_root ~implicit:false ~dir:"user-contrib" ~absolute:false;
+   ] @
+-  List.map (fun dir -> mk_vo ~has_ml:true ~coq_path:default_root ~implicit:false ~dir)
+  List.map (fun dir -> mk_vo ~has_ml:true ~coq_path:default_root ~implicit:false ~dir ~absolute:true)
+     Envars.coqpath
+ 
+ (******************************************************************************)
--- a/pkgs/development/coq-modules/serapi/default.nix
+++ b/pkgs/development/coq-modules/serapi/default.nix
@ -0,0 +1,80 @@
+{ lib, fetchzip, mkCoqDerivation, coq, version ? null }:
+
+let
+  release = {
+    "8.15.0+0.15.0".sha256 = "1vh99ya2dq6a8xl2jrilgs0rpj4j227qx8zvzd2v5xylx0p4bbrp";
+    "8.14.0+0.14.0".sha256 = "1kh80yb791yl771qbqkvwhbhydfii23a7lql0jgifvllm2k8hd8d";
+    "8.13.0+0.13.0".sha256 = "0k69907xn4k61w4mkhwf8kh8drw9pijk9ynijsppihw98j8w38fy";
+    "8.12.0+0.12.1".sha256 = "048x3sgcq4h845hi6hm4j4dsfca8zfj70dm42w68n63qcm6xf9hn";
+    "8.11.0+0.11.1".sha256 = "1phmh99yqv71vlwklqgfxiq2vj99zrzxmryj2j4qvg5vav3y3y6c";
+    "8.10.0+0.7.2".sha256  = "1ljzm63hpd0ksvkyxcbh8rdf7p90vg91gb4h0zz0941v1zh40k8c";
+  };
+in
+
+(with lib; mkCoqDerivation rec {
+  pname = "serapi";
+  inherit version release;
+
+  defaultVersion =  with versions;
+    switch coq.version [
+      { case = isEq "8.15"; out = "8.15.0+0.15.0"; }
+      { case = isEq "8.14"; out = "8.14.0+0.14.0"; }
+      { case = isEq "8.13"; out = "8.13.0+0.13.0"; }
+      { case = isEq "8.12"; out = "8.12.0+0.12.1"; }
+      { case = isEq "8.11"; out = "8.11.0+0.11.1"; }
+      { case = isEq "8.10"; out = "8.10.0+0.7.2";  }
+    ] null;
+
+  useDune2 = true;
+
+  propagatedBuildInputs =
+    with coq.ocamlPackages; [
+      cmdliner
+      findlib # run time dependency of SerAPI
+      ppx_deriving
+      ppx_deriving_yojson
+      ppx_import
+      ppx_sexp_conv
+      sexplib
+      yojson
+      zarith # needed because of Coq
+    ];
+
+  installPhase = ''
+    runHook preInstall
+    dune install --prefix $out --libdir $OCAMLFIND_DESTDIR coq-serapi
+    runHook postInstall
+  '';
+
+  meta = with lib; {
+    homepage = "https://github.com/ejgallego/coq-serapi";
+    description = "SerAPI is a library for machine-to-machine interaction with the Coq proof assistant";
+    license = licenses.lgpl21Plus;
+    maintainers = [ maintainers.Zimmi48 ];
+  };
+}).overrideAttrs(o:
+  let inherit (o) version; in {
+  src = fetchzip {
+    url =
+        "https://github.com/ejgallego/coq-serapi/releases/download/${version}/coq-serapi-${
+          if version == "8.11.0+0.11.1" then version
+          else builtins.replaceStrings [ "+" ] [ "." ] version
+        }.tbz";
+    sha256 = release."${version}".sha256;
+  };
+
+  patches =
+    if version == "8.10.0+0.7.2"
+    then [
+      ./8.10.0+0.7.2.patch
+    ]
+    else if version == "8.11.0+0.11.1"
+    then [
+      ./8.11.0+0.11.1.patch
+    ]
+    else if version == "8.12.0+0.12.1" || version == "8.13.0+0.13.0"
+    then [
+      ./8.12.0+0.12.1.patch
+    ]
+    else [];
+})
--- a/pkgs/development/coq-modules/simple-io/default.nix
+++ b/pkgs/development/coq-modules/simple-io/default.nix
@ -0,0 +1,26 @@
+{ lib, mkCoqDerivation, coq, coq-ext-lib, version ? null }:
+
+with lib; mkCoqDerivation {
+  pname = "simple-io";
+  owner = "Lysxia";
+  repo = "coq-simple-io";
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = range "8.11" "8.15"; out = "1.7.0"; }
+    { case = range "8.7"  "8.13"; out = "1.3.0"; }
+  ] null;
+  release."1.7.0".sha256 = "sha256:1a1q9x2abx71hqvjdai3n12jxzd49mhf3nqqh3ya2ssl2lj609ci";
+  release."1.3.0".sha256 = "1yp7ca36jyl9kz35ghxig45x6cd0bny2bpmy058359p94wc617ax";
+  mlPlugin = true;
+  nativeBuildInputs = [ coq.ocamlPackages.cppo ];
+  propagatedBuildInputs = [ coq-ext-lib coq.ocamlPackages.ocamlbuild ];
+
+  doCheck = true;
+  checkTarget = "test";
+
+  meta = {
+    description = "Purely functional IO for Coq";
+    license = licenses.mit;
+    maintainers = [ maintainers.vbgl ];
+  };
+}
--- a/pkgs/development/coq-modules/smpl/default.nix
+++ b/pkgs/development/coq-modules/smpl/default.nix
@ -0,0 +1,32 @@
+{ lib, mkCoqDerivation, coq, version ? null }:
+with lib;
+
+mkCoqDerivation {
+  pname = "smpl";
+  owner = "uds-psl";
+
+  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"; }
+  ] null;
+
+  mlPlugin = true;
+
+  meta = {
+    description = "A Coq plugin providing an extensible tactic similar to first";
+    maintainers = with maintainers; [ siraben ];
+    license = licenses.mit;
+    platforms = platforms.unix;
+  };
+}
--- a/pkgs/development/coq-modules/smtcoq/default.nix
+++ b/pkgs/development/coq-modules/smtcoq/default.nix
@ -0,0 +1,28 @@
+{ lib, stdenv, mkCoqDerivation, coq, trakt, cvc4, veriT, version ? null }:
+with lib;
+
+mkCoqDerivation {
+  pname = "smtcoq";
+  owner = "smtcoq";
+
+  release."itp22".rev    = "1d60d37558d85a4bfd794220ec48849982bdc979";
+  release."itp22".sha256 = "sha256-CdPfgDfeJy8Q6ZlQeVCSR/x8ZlJ2kSEF6F5UnAespnQ=";
+
+  inherit version;
+  defaultVersion = with versions; switch coq.version [
+    { case = isEq "8.13"; out = "itp22"; }
+  ] null;
+
+  propagatedBuildInputs = [ trakt cvc4 ]
+    ++ lib.optionals (!stdenv.isDarwin) [ veriT ]
+    ++ (with coq.ocamlPackages; [ num zarith ]);
+  mlPlugin = true;
+  nativeBuildInputs = with coq.ocamlPackages; [ ocamlbuild ];
+
+  meta = {
+    description = "Communication between Coq and SAT/SMT solvers ";
+    maintainers = with maintainers; [ siraben ];
+    license = licenses.cecill-b;
+    platforms = platforms.unix;
+  };
+}
--- a/pkgs/development/coq-modules/stdpp/default.nix
+++ b/pkgs/development/coq-modules/stdpp/default.nix
@ -0,0 +1,31 @@
+{ lib, mkCoqDerivation, coq, version ? null }:
+
+with lib; mkCoqDerivation rec {
+  pname = "stdpp";
+  inherit version;
+  domain = "gitlab.mpi-sws.org";
+  owner = "iris";
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = range "8.13" "8.15"; out = "1.7.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.7.0".sha256 = "sha256:0447wbzm23f9rl8byqf6vglasfn6c1wy6cxrrwagqjwsh3i5lx8y";
+  release."1.6.0".sha256 = "1l1w6srzydjg0h3f4krrfgvz455h56shyy2lbcnwdbzjkahibl7v";
+  release."1.5.0".sha256 = "1ym0fy620imah89p8b6rii8clx2vmnwcrbwxl3630h24k42092nf";
+  release."1.4.0".sha256 = "1m6c7ibwc99jd4cv14v3r327spnfvdf3x2mnq51f9rz99rffk68r";
+  releaseRev = v: "coq-stdpp-${v}";
+
+  preBuild = ''
+    if [[ -f coq-lint.sh ]]
+    then patchShebangs coq-lint.sh
+    fi
+  '';
+
+  meta = {
+    description = "An extended “Standard Library” for Coq";
+    license = licenses.bsd3;
+    maintainers = [ maintainers.vbgl ];
+  };
+}
--- a/pkgs/development/coq-modules/tlc/default.nix
+++ b/pkgs/development/coq-modules/tlc/default.nix
@ -0,0 +1,31 @@
+{ lib, mkCoqDerivation, coq, version ? null }:
+
+with lib; (mkCoqDerivation {
+  pname = "tlc";
+  owner = "charguer";
+  inherit version;
+  displayVersion = { tlc = false; };
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = range "8.13" "8.15"; out = "20211215"; }
+    { case = range "8.12" "8.13"; out = "20210316"; }
+    { case = range "8.10" "8.12"; out = "20200328"; }
+    { case = range "8.6"  "8.12"; out = "20181116"; }
+  ] null;
+  release."20211215".sha256 = "sha256:0m4d4jhdcyq8p2gpz9j3nd6jqzmz2bjmbpc0q06b38b8i550mamp";
+  release."20210316".sha256 = "1hlavnx20lxpf2iydbbxqmim9p8wdwv4phzp9ypij93yivih0g4a";
+  release."20200328".sha256 = "16vzild9gni8zhgb3qhmka47f8zagdh03k6nssif7drpim8233lx";
+  release."20181116".sha256 = "032lrbkxqm9d3fhf6nv1kq2z0mqd3czv3ijlbsjwnfh12xck4vpl";
+
+  meta = {
+    homepage = "http://www.chargueraud.org/softs/tlc/";
+    description = "A non-constructive library for Coq";
+    license = licenses.free;
+    maintainers = [ maintainers.vbgl ];
+  };
+}).overrideAttrs (x:
+  if versionAtLeast x.version "20210316"
+  then {}
+  else {
+    installFlags = [ "CONTRIB=$(out)/lib/coq/${coq.coq-version}/user-contrib" ];
+  }
+)
--- a/pkgs/development/coq-modules/topology/default.nix
+++ b/pkgs/development/coq-modules/topology/default.nix
@ -0,0 +1,39 @@
+{ lib, mkCoqDerivation, coq, mathcomp, zorns-lemma, version ? null }:
+with lib;
+
+mkCoqDerivation rec {
+  pname = "topology";
+
+  releaseRev = v: "v${v}";
+
+  release."9.0.0".sha256 = "sha256:03lgy53xg9pmrdd3d8qb4087k5qjnk260655svp6d79x4p2lxr8c";
+  release."8.12.0".sha256 = "sha256-ypHmHwzwZ6MQPYwuS3QyZmVOEPUCSbO2lhVaA6TypgQ=";
+  release."8.10.0".sha256 = "sha256-mCLF3JYIiO3AEW9yvlcLeF7zN4SjW3LG+Y5vYB0l55A=";
+  release."8.9.0".sha256 = "sha256-ZJh1BM34iZOQ75zqLIA+KtBjO2y33y0UpAw/ydCWQYc=";
+  release."8.8.0".sha256 = "sha256-Yfm3UymEP1e+BKMNPhdRFLdFhynMirtQ8E0HXnRiqHU=";
+  release."8.7.0".sha256 = "sha256-qcZQKvMRs5wWIAny8ciF9TrmEQfKKO9fWhwIRL+s7VA=";
+  release."8.6.0".sha256 = "sha256-eu/dBEFo3y6vnXlJljUD4hds6+qgAPQVvsuspyGHcj8=";
+
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = isGe "8.10"; out = "9.0.0"; }
+    { case = "8.9"; out = "8.9.0"; }
+    { case = "8.8"; out = "8.8.0"; }
+    { case = "8.7"; out = "8.7.0"; }
+    { case = "8.6"; out = "8.6.0"; }
+  ] null;
+
+  propagatedBuildInputs = [ zorns-lemma ];
+
+  useDune2ifVersion = versions.isGe "9.0";
+
+  meta = {
+    description = "General topology in Coq";
+    longDescription = ''
+      This library develops some of the basic concepts and results of
+      general topology in Coq.
+    '';
+    maintainers = with maintainers; [ siraben ];
+    license = licenses.lgpl21Plus;
+  };
+}
--- a/pkgs/development/coq-modules/trakt/default.nix
+++ b/pkgs/development/coq-modules/trakt/default.nix
@ -0,0 +1,24 @@
+{ lib, mkCoqDerivation, coq, coq-elpi, version ? null }:
+with lib;
+
+mkCoqDerivation {
+  pname = "trakt";
+  owner = "ecranceMERCE";
+
+  release."1.0".rev    = "d1c9daba8fe0584b526047862dd27ddf836dbbf2";
+  release."1.0".sha256 = "sha256-Qhw5fWFYxUFO2kIWWz/og+4fuy9aYG27szfNk3IglhY=";
+
+  inherit version;
+  defaultVersion = with versions; switch [ coq.version ] [
+    { cases = [ (isGe "8.13") ]; out = "1.0"; }
+  ] null;
+
+  propagatedBuildInputs = [ coq-elpi ];
+
+  meta = {
+    description = "A generic goal preprocessing tool for proof automation tactics in Coq";
+    maintainers = with maintainers; [ siraben ];
+    license = licenses.cecill-b;
+    platforms = platforms.unix;
+  };
+}
--- a/pkgs/development/coq-modules/zorns-lemma/default.nix
+++ b/pkgs/development/coq-modules/zorns-lemma/default.nix
@ -0,0 +1,40 @@
+{ lib, mkCoqDerivation, coq, version ? null }:
+with lib;
+
+(mkCoqDerivation {
+  pname = "zorns-lemma";
+
+  releaseRev = v: "v${v}";
+
+  release."9.0.0".sha256 = "sha256:03lgy53xg9pmrdd3d8qb4087k5qjnk260655svp6d79x4p2lxr8c";
+  release."8.11.0".sha256 = "sha256-2Hf7YwRcFmP/DqwFtF1p78MCNV50qUWfMVQtZbwKd0k=";
+  release."8.10.0".sha256 = "sha256-qLPLK2ZLJQ4SmJX2ADqFiP4kgHuQFJTeNXkBbjiFS+4=";
+  release."8.9.0".sha256 = "sha256-lEh978cXehglFX9D92RVltEuvN8umfPo/hvmFZm2NGo=";
+  release."8.8.0".sha256 = "sha256-ikXGzABu8VW7O0xNtCNvIq29c+mlDUm4k/ygVcsgDOI=";
+  release."8.7.0".sha256 = "sha256-jozvkkKLFBllN6K4oeYD0lNG+MdnOuKrDUPDocHUG6c=";
+  release."8.6.0".sha256 = "sha256-jozvkkKLFBllN6K4oeYD0lNG+MdnOuKrDUPDocHUG6c=";
+  release."8.5.0".sha256 = "sha256-mH/v02ObMjbVPYx2H+Jhz+Xp0XRKN67iMAdA1VNFzso=";
+
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = isGe "8.10"; out = "9.0.0"; }
+    { case = "8.9"; out = "8.9.0"; }
+    { case = "8.8"; out = "8.8.0"; }
+    { case = "8.7"; out = "8.7.0"; }
+    { case = "8.6"; out = "8.6.0"; }
+    { case = "8.5"; out = "8.5.0"; }
+  ] null;
+
+  useDune2ifVersion = versions.isGe "9.0";
+
+  meta = {
+    description = "Development of basic set theory";
+    longDescription = ''
+      This Coq library develops some basic set theory.  The main
+      purpose the author had in writing it was as support for the
+      Topology library.
+    '';
+    maintainers = with maintainers; [ siraben ];
+    license = licenses.lgpl21Plus;
+  };
+}).overrideAttrs({version, ...}: if versions.isGe "9.0" version then { repo =  "topology"; } else {})