From a69fe54c499fed6e94f9741314002f55588a98c8 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Wed, 24 Jul 2024 15:22:31 +0200
Subject: [PATCH] coqPackages.stalmarck: init at 8.20.0

---
 .../coq-modules/stalmarck/default.nix         | 37 +++++++++++++++++++
 pkgs/top-level/coq-packages.nix               |  2 +
 2 files changed, 39 insertions(+)
 create mode 100644 pkgs/development/coq-modules/stalmarck/default.nix

diff --git a/pkgs/development/coq-modules/stalmarck/default.nix b/pkgs/development/coq-modules/stalmarck/default.nix
new file mode 100644
index 0000000000000..88ea437937268
--- /dev/null
+++ b/pkgs/development/coq-modules/stalmarck/default.nix
@@ -0,0 +1,37 @@
+{ lib, mkCoqDerivation, coq, version ? null }:
+
+let
+  repo = "stalmarck";
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
+    { case = isEq "8.20"; out = "8.20.0"; }
+  ] null;
+  release = {
+    "8.20.0".sha256 = "sha256-jITxQT1jLyZvWCGPnmK8i3IrwsZwMPOV0aBe9r22TIQ=";
+  };
+  releaseRev = v: "v${v}";
+
+  packages = [ "stalmarck" "stalmarck-tactic" ];
+
+  stalmarck_ = package: let
+    pname = package;
+    istac = package == "stalmarck-tactic";
+    propagatedBuildInputs =
+      lib.optional istac (stalmarck_ "stalmarck");
+    description =
+      if istac then
+        "Coq tactic and verified tool for proving tautologies using Stålmarck's algorithm"
+      else
+        "A two-level approach to prove tautologies using Stålmarck's algorithm in Coq.";
+    in mkCoqDerivation {
+      inherit version pname defaultVersion release releaseRev repo
+        propagatedBuildInputs;
+
+      mlPlugin = istac;
+      useDune = istac;
+
+      meta = { inherit description; license = lib.licenses.lgpl21Plus; };
+
+      passthru = lib.genAttrs packages stalmarck_;
+    };
+in
+stalmarck_ "stalmarck-tactic"
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index 78f5cd2bb187f..accb9cc009859 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -121,6 +121,8 @@ let
       smpl = callPackage ../development/coq-modules/smpl { };
       smtcoq = callPackage ../development/coq-modules/smtcoq { };
       ssprove = callPackage ../development/coq-modules/ssprove {};
+      stalmarck-tactic = callPackage ../development/coq-modules/stalmarck {};
+      stalmarck = self.stalmarck-tactic.stalmarck;
       stdpp = callPackage ../development/coq-modules/stdpp { };
       StructTact = callPackage ../development/coq-modules/StructTact {};
       tlc = callPackage ../development/coq-modules/tlc {};