coqPackages.stalmarck: init at 8.20.0

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"

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 {};