From 629830c8ffc7d1b34533a6ebebde0eaec0c5c941 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Fri, 19 Jul 2024 13:38:54 +0200
Subject: [PATCH] Add coqPackages.stdlib

---
 .../coq-modules/ExtLib/default.nix            |  4 +-
 .../coq-modules/InfSeqExt/default.nix         |  3 +
 .../coq-modules/MenhirLib/default.nix         |  2 +
 .../coq-modules/StructTact/default.nix        |  3 +
 .../coq-modules/aac-tactics/default.nix       |  3 +
 pkgs/development/coq-modules/atbr/default.nix |  3 +
 pkgs/development/coq-modules/bbv/default.nix  |  3 +
 .../coq-modules/bignums/default.nix           |  3 +
 .../development/coq-modules/ceres/default.nix |  3 +
 .../coq-modules/coinduction/default.nix       |  3 +
 .../coq-modules/coq-elpi/default.nix          |  2 +
 .../coq-modules/coq-hammer/tactics.nix        |  3 +
 .../coq-modules/equations/default.nix         |  3 +
 .../development/coq-modules/flocq/default.nix |  3 +
 .../coq-modules/itauto/default.nix            |  3 +
 .../coq-modules/mathcomp/default.nix          |  4 +-
 pkgs/development/coq-modules/paco/default.nix |  3 +
 .../coq-modules/rewriter/default.nix          |  3 +
 .../coq-modules/smtcoq/default.nix            |  2 +
 .../coq-modules/stalmarck/default.nix         |  3 +-
 .../coq-modules/stdlib/default.nix            | 59 +++++++++++++++++++
 .../development/coq-modules/stdpp/default.nix |  3 +
 pkgs/development/coq-modules/tlc/default.nix  |  3 +
 .../coq-modules/waterproof/default.nix        |  3 +
 pkgs/top-level/coq-packages.nix               |  1 +
 25 files changed, 124 insertions(+), 4 deletions(-)
 create mode 100644 pkgs/development/coq-modules/stdlib/default.nix

diff --git a/pkgs/development/coq-modules/ExtLib/default.nix b/pkgs/development/coq-modules/ExtLib/default.nix
index 7d81235799e3..4eb989a50ef4 100644
--- a/pkgs/development/coq-modules/ExtLib/default.nix
+++ b/pkgs/development/coq-modules/ExtLib/default.nix
@@ -1,4 +1,4 @@
-{ lib, mkCoqDerivation, coq, version ? null }:
+{ lib, mkCoqDerivation, coq, stdlib, version ? null }:
 
 mkCoqDerivation rec {
   pname = "coq-ext-lib";
@@ -33,6 +33,8 @@ mkCoqDerivation rec {
   release."0.9.4".sha256  = "1y66pamgsdxlq2w1338lj626ln70cwj7k53hxcp933g8fdsa4hp0";
   releaseRev = v: "v${v}";
 
+  propagatedBuildInputs = [ stdlib ];
+
   meta = {
     description = "Collection of theories and plugins that may be useful in other Coq developments";
     maintainers = with lib.maintainers; [ jwiegley ptival ];
diff --git a/pkgs/development/coq-modules/InfSeqExt/default.nix b/pkgs/development/coq-modules/InfSeqExt/default.nix
index d36a723deabf..479205b0245a 100644
--- a/pkgs/development/coq-modules/InfSeqExt/default.nix
+++ b/pkgs/development/coq-modules/InfSeqExt/default.nix
@@ -2,6 +2,7 @@
   lib,
   mkCoqDerivation,
   coq,
+  stdlib,
   version ? null,
 }:
 
@@ -25,4 +26,6 @@ mkCoqDerivation {
   release."20230107".sha256 = "sha256-YMBzVIsLkIC+w2TeyHrKe29eWLIxrH3wIMZqhik8p9I=";
   release."20200131".rev = "203d4c20211d6b17741f1fdca46dbc091f5e961a";
   release."20200131".sha256 = "0xylkdmb2dqnnqinf3pigz4mf4zmczcbpjnn59g5g76m7f2cqxl0";
+
+  propagatedBuildInputs = [ stdlib ];
 }
diff --git a/pkgs/development/coq-modules/MenhirLib/default.nix b/pkgs/development/coq-modules/MenhirLib/default.nix
index 5b680c73da44..ecdbab974a5f 100644
--- a/pkgs/development/coq-modules/MenhirLib/default.nix
+++ b/pkgs/development/coq-modules/MenhirLib/default.nix
@@ -2,6 +2,7 @@
   lib,
   mkCoqDerivation,
   coq,
+  stdlib,
   version ? null,
 }:
 let
@@ -32,6 +33,7 @@ let
       "20211230".sha256 = "sha256-+ntl4ykkqJWEeJJzt6fO5r0X1J+4in2LJIj1N8R175w="; # coq 8.7 - 8.18
       "20200624".sha256 = "sha256-8lMqwmOsqxU/45Xr+GeyU2aIjrClVdv3VamCCkF76jY="; # coq 8.7 - 8.13
     };
+    propagatedBuildInputs = [ stdlib ];
     preBuild = "cd coq-menhirlib/src";
     meta = with lib; {
       homepage = "https://gitlab.inria.fr/fpottier/menhir/-/tree/master/coq-menhirlib";
diff --git a/pkgs/development/coq-modules/StructTact/default.nix b/pkgs/development/coq-modules/StructTact/default.nix
index 8e982d19f609..63a450726e4c 100644
--- a/pkgs/development/coq-modules/StructTact/default.nix
+++ b/pkgs/development/coq-modules/StructTact/default.nix
@@ -2,6 +2,7 @@
   lib,
   mkCoqDerivation,
   coq,
+  stdlib,
   version ? null,
 }:
 
@@ -31,4 +32,6 @@ mkCoqDerivation {
   release."20210328".sha256 = "sha256:1y5r1zm3hli10ah6lnj7n8hxad6rb6rgldd0g7m2fjibzvwqzhdg";
   release."20181102".rev = "82a85b7ec07e71fa6b30cfc05f6a7bfb09ef2510";
   release."20181102".sha256 = "08zry20flgj7qq37xk32kzmg4fg6d4wi9m7pf9aph8fd3j2a0b5v";
+
+  propagatedBuildInputs = [ stdlib ];
 }
diff --git a/pkgs/development/coq-modules/aac-tactics/default.nix b/pkgs/development/coq-modules/aac-tactics/default.nix
index a5cbfa49d938..db2c56c7d98a 100644
--- a/pkgs/development/coq-modules/aac-tactics/default.nix
+++ b/pkgs/development/coq-modules/aac-tactics/default.nix
@@ -2,6 +2,7 @@
   lib,
   mkCoqDerivation,
   coq,
+  stdlib,
   version ? null,
 }:
 
@@ -97,6 +98,8 @@ mkCoqDerivation {
 
   mlPlugin = true;
 
+  propagatedBuildInputs = [ stdlib ];
+
   meta = with lib; {
     description = "Coq plugin providing tactics for rewriting universally quantified equations";
     longDescription = ''
diff --git a/pkgs/development/coq-modules/atbr/default.nix b/pkgs/development/coq-modules/atbr/default.nix
index 7310e4b45702..3e5598b81dbb 100644
--- a/pkgs/development/coq-modules/atbr/default.nix
+++ b/pkgs/development/coq-modules/atbr/default.nix
@@ -2,6 +2,7 @@
   lib,
   mkCoqDerivation,
   coq,
+  stdlib,
   version ? null,
 }:
 
@@ -23,6 +24,8 @@ mkCoqDerivation {
   };
   releaseRev = v: "v${v}";
 
+  propagatedBuildInputs = [ stdlib ];
+
   mlPlugin = true;
 
   meta = {
diff --git a/pkgs/development/coq-modules/bbv/default.nix b/pkgs/development/coq-modules/bbv/default.nix
index 44d0b0b40cee..6218d73f8ff8 100644
--- a/pkgs/development/coq-modules/bbv/default.nix
+++ b/pkgs/development/coq-modules/bbv/default.nix
@@ -2,6 +2,7 @@
   lib,
   mkCoqDerivation,
   coq,
+  stdlib,
   version ? null,
 }:
 
@@ -24,6 +25,8 @@ mkCoqDerivation {
   };
   releaseRev = v: "v${v}";
 
+  propagatedBuildInputs = [ stdlib ];
+
   meta = {
     description = "An implementation of bitvectors in Coq.";
     license = lib.licenses.mit;
diff --git a/pkgs/development/coq-modules/bignums/default.nix b/pkgs/development/coq-modules/bignums/default.nix
index 384ae1d80dae..acd6b8e04303 100644
--- a/pkgs/development/coq-modules/bignums/default.nix
+++ b/pkgs/development/coq-modules/bignums/default.nix
@@ -2,6 +2,7 @@
   lib,
   mkCoqDerivation,
   coq,
+  stdlib,
   version ? null,
 }:
 
@@ -47,6 +48,8 @@ mkCoqDerivation {
 
   mlPlugin = true;
 
+  propagatedBuildInputs = [ stdlib ];
+
   meta = {
     license = lib.licenses.lgpl2;
   };
diff --git a/pkgs/development/coq-modules/ceres/default.nix b/pkgs/development/coq-modules/ceres/default.nix
index 86907967f038..b141d2b48e2a 100644
--- a/pkgs/development/coq-modules/ceres/default.nix
+++ b/pkgs/development/coq-modules/ceres/default.nix
@@ -2,6 +2,7 @@
   lib,
   mkCoqDerivation,
   coq,
+  stdlib,
   version ? null,
 }:
 
@@ -29,6 +30,8 @@ mkCoqDerivation {
 
   useDuneifVersion = lib.versions.isGe "0.4.1";
 
+  propagatedBuildInputs = [ stdlib ];
+
   meta = with lib; {
     description = "Library for serialization to S-expressions";
     license = licenses.mit;
diff --git a/pkgs/development/coq-modules/coinduction/default.nix b/pkgs/development/coq-modules/coinduction/default.nix
index c9792d1e960f..c24e060a1c62 100644
--- a/pkgs/development/coq-modules/coinduction/default.nix
+++ b/pkgs/development/coq-modules/coinduction/default.nix
@@ -2,6 +2,7 @@
   lib,
   mkCoqDerivation,
   coq,
+  stdlib,
   version ? null,
 }:
 
@@ -24,6 +25,8 @@ mkCoqDerivation {
   };
   releaseRev = v: "v${v}";
 
+  propagatedBuildInputs = [ stdlib ];
+
   mlPlugin = true;
 
   meta = {
diff --git a/pkgs/development/coq-modules/coq-elpi/default.nix b/pkgs/development/coq-modules/coq-elpi/default.nix
index 4765e8fbb1de..5a6146de50b1 100644
--- a/pkgs/development/coq-modules/coq-elpi/default.nix
+++ b/pkgs/development/coq-modules/coq-elpi/default.nix
@@ -3,6 +3,7 @@
   mkCoqDerivation,
   which,
   coq,
+  stdlib,
   version ? null,
 }:
 
@@ -163,6 +164,7 @@ in
   propagatedBuildInputs = [
     coq.ocamlPackages.findlib
     elpi
+    stdlib
   ];
 
   meta = {
diff --git a/pkgs/development/coq-modules/coq-hammer/tactics.nix b/pkgs/development/coq-modules/coq-hammer/tactics.nix
index c2f7e40f1a23..893c8eb81b1a 100644
--- a/pkgs/development/coq-modules/coq-hammer/tactics.nix
+++ b/pkgs/development/coq-modules/coq-hammer/tactics.nix
@@ -2,6 +2,7 @@
   lib,
   mkCoqDerivation,
   coq,
+  stdlib,
   version ? null,
 }:
 
@@ -61,6 +62,8 @@ mkCoqDerivation {
       ;
   };
 
+  propagatedBuildInputs = [ stdlib ];
+
   mlPlugin = true;
 
   buildFlags = [ "tactics" ];
diff --git a/pkgs/development/coq-modules/equations/default.nix b/pkgs/development/coq-modules/equations/default.nix
index 309b44559f26..ca413d532f6b 100644
--- a/pkgs/development/coq-modules/equations/default.nix
+++ b/pkgs/development/coq-modules/equations/default.nix
@@ -2,6 +2,7 @@
   lib,
   mkCoqDerivation,
   coq,
+  stdlib,
   version ? null,
 }:
 
@@ -119,6 +120,8 @@
 
   mlPlugin = true;
 
+  propagatedBuildInputs = [ stdlib ];
+
   meta = with lib; {
     homepage = "https://mattam82.github.io/Coq-Equations/";
     description = "Plugin for Coq to add dependent pattern-matching";
diff --git a/pkgs/development/coq-modules/flocq/default.nix b/pkgs/development/coq-modules/flocq/default.nix
index 80dfdd597bf3..9cbf093b7273 100644
--- a/pkgs/development/coq-modules/flocq/default.nix
+++ b/pkgs/development/coq-modules/flocq/default.nix
@@ -4,6 +4,7 @@
   autoconf,
   mkCoqDerivation,
   coq,
+  stdlib,
   version ? null,
 }:
 
@@ -58,6 +59,8 @@ mkCoqDerivation {
   mlPlugin = true;
   useMelquiondRemake.logpath = "Flocq";
 
+  propagatedBuildInputs = [ stdlib ];
+
   meta = with lib; {
     description = "Floating-point formalization for the Coq system";
     license = licenses.lgpl3;
diff --git a/pkgs/development/coq-modules/itauto/default.nix b/pkgs/development/coq-modules/itauto/default.nix
index 238c89d1fd5a..22f3eb2d9f21 100644
--- a/pkgs/development/coq-modules/itauto/default.nix
+++ b/pkgs/development/coq-modules/itauto/default.nix
@@ -3,6 +3,7 @@
   callPackage,
   mkCoqDerivation,
   coq,
+  stdlib,
   version ? null,
 }:
 
@@ -63,6 +64,8 @@
 
   passthru.tests.suite = callPackage ./test.nix { };
 
+  propagatedBuildInputs = [ stdlib ];
+
   meta = with lib; {
     description = "Reflexive SAT solver parameterised by a leaf tactic and Nelson-Oppen support";
     maintainers = with maintainers; [ siraben ];
diff --git a/pkgs/development/coq-modules/mathcomp/default.nix b/pkgs/development/coq-modules/mathcomp/default.nix
index af4313ae2198..2cb068ba11cc 100644
--- a/pkgs/development/coq-modules/mathcomp/default.nix
+++ b/pkgs/development/coq-modules/mathcomp/default.nix
@@ -12,7 +12,7 @@
 
 { lib, ncurses, graphviz, lua, fetchzip,
   mkCoqDerivation, withDoc ? false, single ? false,
-  coq, hierarchy-builder, version ? null }@args:
+  coq, hierarchy-builder, stdlib, version ? null }@args:
 
 let
   repo  = "math-comp";
@@ -78,7 +78,7 @@ let
         mlPlugin = lib.versions.isLe "8.6" coq.coq-version;
         nativeBuildInputs = lib.optionals withDoc [ graphviz lua ];
         buildInputs = [ ncurses ];
-        propagatedBuildInputs = mathcomp-deps;
+        propagatedBuildInputs = [ stdlib ] ++ mathcomp-deps;
 
         buildFlags = lib.optional withDoc "doc";
 
diff --git a/pkgs/development/coq-modules/paco/default.nix b/pkgs/development/coq-modules/paco/default.nix
index 2881e7bab817..7f704a267969 100644
--- a/pkgs/development/coq-modules/paco/default.nix
+++ b/pkgs/development/coq-modules/paco/default.nix
@@ -2,6 +2,7 @@
   lib,
   mkCoqDerivation,
   coq,
+  stdlib,
   version ? null,
 }:
 
@@ -40,6 +41,8 @@ mkCoqDerivation {
   release."1.2.8".sha256 = "05fskx5x1qgaf9qv626m38y5izichzzqc7g2rglzrkygbskrrwsb";
   releaseRev = v: "v${v}";
 
+  propagatedBuildInputs = [ stdlib ];
+
   preBuild = "cd src";
 
   installPhase = ''
diff --git a/pkgs/development/coq-modules/rewriter/default.nix b/pkgs/development/coq-modules/rewriter/default.nix
index 15644c4dcee0..d7c4ff330e1f 100644
--- a/pkgs/development/coq-modules/rewriter/default.nix
+++ b/pkgs/development/coq-modules/rewriter/default.nix
@@ -2,6 +2,7 @@
   lib,
   mkCoqDerivation,
   coq,
+  stdlib,
   version ? null,
 }:
 
@@ -24,6 +25,8 @@ mkCoqDerivation {
   };
   releaseRev = v: "v${v}";
 
+  propagatedBuildInputs = [ stdlib ];
+
   mlPlugin = true;
 
   meta = {
diff --git a/pkgs/development/coq-modules/smtcoq/default.nix b/pkgs/development/coq-modules/smtcoq/default.nix
index 050a0bc1984b..a459fa19938c 100644
--- a/pkgs/development/coq-modules/smtcoq/default.nix
+++ b/pkgs/development/coq-modules/smtcoq/default.nix
@@ -7,6 +7,7 @@
   zchaff,
   fetchurl,
   cvc5,
+  stdlib,
   version ? null,
 }:
 
@@ -80,6 +81,7 @@ mkCoqDerivation {
       cvc5
       veriT'
       zchaff
+      stdlib
     ]
     ++ (with coq.ocamlPackages; [
       findlib
diff --git a/pkgs/development/coq-modules/stalmarck/default.nix b/pkgs/development/coq-modules/stalmarck/default.nix
index 70863c963359..10693a88ed0f 100644
--- a/pkgs/development/coq-modules/stalmarck/default.nix
+++ b/pkgs/development/coq-modules/stalmarck/default.nix
@@ -2,6 +2,7 @@
   lib,
   mkCoqDerivation,
   coq,
+  stdlib,
   version ? null,
 }:
 
@@ -30,7 +31,7 @@ let
     let
       pname = package;
       istac = package == "stalmarck-tactic";
-      propagatedBuildInputs = lib.optional istac (stalmarck_ "stalmarck");
+      propagatedBuildInputs = if istac then [ (stalmarck_ "stalmarck") ] else [ stdlib ];
       description =
         if istac then
           "Coq tactic and verified tool for proving tautologies using Stålmarck's algorithm"
diff --git a/pkgs/development/coq-modules/stdlib/default.nix b/pkgs/development/coq-modules/stdlib/default.nix
new file mode 100644
index 000000000000..86db7159031e
--- /dev/null
+++ b/pkgs/development/coq-modules/stdlib/default.nix
@@ -0,0 +1,59 @@
+{
+  coq,
+  mkCoqDerivation,
+  lib,
+  version ? null,
+}@args:
+(mkCoqDerivation {
+
+  pname = "stdlib";
+  repo = "coq";
+  owner = "coq";
+  opam-name = "coq-stdlib";
+
+  inherit version;
+  defaultVersion =
+    with lib.versions;
+    lib.switch
+      [ coq.version ]
+      [
+        {
+          cases = [ (isLt "8.21") ];
+          out = "8.20";
+        }
+      ]
+      null;
+  releaseRev = v: "v${v}";
+
+  release."8.20".sha256 = "sha256-AcoS4edUYCfJME1wx8UbuSQRF3jmxhArcZyPIoXcfu0=";
+
+  useDune = true;
+
+  configurePhase = ''
+    echo "no configure phase"
+  ''; # don't run Coq's configure
+
+  preBuild = ''
+    echo "(dirs stdlib)" > dune
+  '';
+
+  meta = {
+    description = "Coq Standard Library";
+    license = lib.licenses.lgpl21Only;
+  };
+
+}).overrideAttrs
+  (
+    o:
+    # stdlib is already included in Coq <= 8.20
+    lib.optionalAttrs
+      (coq.version != null && coq.version != "dev" && lib.versions.isLt "8.21" coq.version)
+      {
+        buildPhase = ''
+          echo building nothing
+        '';
+        installPhase = ''
+          touch $out
+        '';
+      }
+  )
diff --git a/pkgs/development/coq-modules/stdpp/default.nix b/pkgs/development/coq-modules/stdpp/default.nix
index 930d5ae87fe1..750388750b6b 100644
--- a/pkgs/development/coq-modules/stdpp/default.nix
+++ b/pkgs/development/coq-modules/stdpp/default.nix
@@ -2,6 +2,7 @@
   lib,
   mkCoqDerivation,
   coq,
+  stdlib,
   version ? null,
 }:
 
@@ -52,6 +53,8 @@ mkCoqDerivation rec {
   release."1.4.0".sha256 = "1m6c7ibwc99jd4cv14v3r327spnfvdf3x2mnq51f9rz99rffk68r";
   releaseRev = v: "coq-stdpp-${v}";
 
+  propagatedBuildInputs = [ stdlib ];
+
   preBuild = ''
     if [[ -f coq-lint.sh ]]
     then patchShebangs coq-lint.sh
diff --git a/pkgs/development/coq-modules/tlc/default.nix b/pkgs/development/coq-modules/tlc/default.nix
index ffc71f93a606..2aeca7509eb6 100644
--- a/pkgs/development/coq-modules/tlc/default.nix
+++ b/pkgs/development/coq-modules/tlc/default.nix
@@ -2,6 +2,7 @@
   lib,
   mkCoqDerivation,
   coq,
+  stdlib,
   version ? null,
 }:
 
@@ -37,6 +38,8 @@
   release."20200328".sha256 = "16vzild9gni8zhgb3qhmka47f8zagdh03k6nssif7drpim8233lx";
   release."20181116".sha256 = "032lrbkxqm9d3fhf6nv1kq2z0mqd3czv3ijlbsjwnfh12xck4vpl";
 
+  propagatedBuildInputs = [ stdlib ];
+
   meta = with lib; {
     homepage = "http://www.chargueraud.org/softs/tlc/";
     description = "Non-constructive library for Coq";
diff --git a/pkgs/development/coq-modules/waterproof/default.nix b/pkgs/development/coq-modules/waterproof/default.nix
index 61612f3cb105..313dd441e799 100644
--- a/pkgs/development/coq-modules/waterproof/default.nix
+++ b/pkgs/development/coq-modules/waterproof/default.nix
@@ -2,6 +2,7 @@
   lib,
   mkCoqDerivation,
   coq,
+  stdlib,
   version ? null,
 }:
 
@@ -24,6 +25,8 @@ mkCoqDerivation {
     "2.1.1+8.18".sha256 = "sha256-jYuQ9SPFRefNCUfn6+jEaJ4399EnU0gXPPkEDCpJYOI=";
   };
 
+  propagatedBuildInputs = [ stdlib ];
+
   mlPlugin = true;
 
   useDune = true;
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index b65e1e42bf91..63cf771268b7 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -150,6 +150,7 @@ let
       ssprove = callPackage ../development/coq-modules/ssprove {};
       stalmarck-tactic = callPackage ../development/coq-modules/stalmarck {};
       stalmarck = self.stalmarck-tactic.stalmarck;
+      stdlib = callPackage ../development/coq-modules/stdlib {};
       stdpp = callPackage ../development/coq-modules/stdpp { };
       StructTact = callPackage ../development/coq-modules/StructTact {};
       tlc = callPackage ../development/coq-modules/tlc {};