From 11985737dc144ba10f7a10d62d223b184d346234 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Thu, 1 Aug 2024 16:36:27 +0200
Subject: [PATCH] coqPackages.waterproof: init at 2.1.1+8.18

---
 .../coq-modules/waterproof/default.nix        | 24 +++++++++++++++++++
 pkgs/top-level/coq-packages.nix               |  1 +
 2 files changed, 25 insertions(+)
 create mode 100644 pkgs/development/coq-modules/waterproof/default.nix

diff --git a/pkgs/development/coq-modules/waterproof/default.nix b/pkgs/development/coq-modules/waterproof/default.nix
new file mode 100644
index 000000000000..7d9431c25c28
--- /dev/null
+++ b/pkgs/development/coq-modules/waterproof/default.nix
@@ -0,0 +1,24 @@
+{ lib, mkCoqDerivation, coq, version ? null }:
+
+mkCoqDerivation {
+  pname = "waterproof";
+  owner = "impermeable";
+  repo = "coq-waterproof";
+  inherit version;
+  defaultVersion = let inherit (lib.versions) range; in
+    lib.switch coq.coq-version [
+      { case = range "8.18" "8.18"; out = "2.1.1+8.18"; }
+    ] null;
+  release = {
+    "2.1.1+8.18".sha256  = "sha256-jYuQ9SPFRefNCUfn6+jEaJ4399EnU0gXPPkEDCpJYOI=";
+  };
+
+  mlPlugin = true;
+
+  useDune = true;
+
+  meta = {
+    description = "Coq proofs in a style that resembles non-mechanized mathematical proofs";
+    license = lib.licenses.lgpl3Plus;
+  };
+}
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index ecdbe8bd6eff..c6a6ce952f71 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -159,6 +159,7 @@ let
             paco = self.paco.override { version = "4.1.2"; };
           };
        }));
+      waterproof = callPackage ../development/coq-modules/waterproof {};
       zorns-lemma = callPackage ../development/coq-modules/zorns-lemma {};
       filterPackages = doesFilter: if doesFilter then filterCoqPackages self else self;
     };