From ea51404f4e50c9a2692697f30dae6b2649f953f9 Mon Sep 17 00:00:00 2001
From: Sebastian Ertel <sebastian.ertel@gmail.com>
Date: Fri, 3 May 2024 11:32:09 +0200
Subject: coqPackages.ssprove: init at 0.2.0 (#306981)

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

(limited to 'pkgs')

diff --git a/pkgs/development/coq-modules/ssprove/default.nix b/pkgs/development/coq-modules/ssprove/default.nix
new file mode 100644
index 0000000000000..714872170c3b9
--- /dev/null
+++ b/pkgs/development/coq-modules/ssprove/default.nix
@@ -0,0 +1,48 @@
+{ lib, mkCoqDerivation, coq, version ? null
+, equations
+, mathcomp-ssreflect
+, mathcomp-analysis
+, extructures
+, deriving
+}:
+
+(mkCoqDerivation {
+  pname = "ssprove";
+  owner = "SSProve";
+
+  inherit version;
+  defaultVersion = with lib.versions; lib.switch [coq.coq-version mathcomp-ssreflect.version] [
+    { cases = [(range "8.18" "8.19") (range "2.1.0" "2.2.0")]; out = "0.2.0"; }
+    # This is the original dependency:
+    # { cases = ["8.17" "1.18.0"]; out = "0.1.0"; }
+    # But it is not loadable. The math-comp nixpkgs configuration
+    # will always only output version 1.18.0 for Coq 8.17.
+    # Hence, the Coq 8.17 and math-comp 1.17.0 must be explicitly set
+    # to load it.
+    # (This version is not on the math-comp CI and hence not checked.)
+    { cases = ["8.17" "1.17.0"]; out = "0.1.0"; }
+  ] null;
+
+  releaseRev = v: "v${v}";
+
+  release."0.2.0".sha256 = "sha256-GDkWH0LUsW165vAUoYC5of9ndr0MbfBtmrPhsJVXi3o=";
+  release."0.1.0".sha256 = "sha256-Yj+k+mBsudi3d6bRVlZLyM4UqQnzAX5tHvxtKoIuNTE=";
+
+  propagatedBuildInputs = [equations
+                           mathcomp-ssreflect
+                           mathcomp-analysis
+                           extructures
+                           deriving];
+
+  meta = with lib; {
+    description = "SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq";
+    license = licenses.mit;
+    maintainers = [ {
+      name = "Sebastian Ertel";
+      email = "sebastian.ertel@gmail.com";
+      github = "sertel";
+      githubId = 3703100;
+    } ];
+  };
+
+})
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index 1964f666a86ba..88538a7da7738 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -117,6 +117,7 @@ let
       simple-io = callPackage ../development/coq-modules/simple-io { };
       smpl = callPackage ../development/coq-modules/smpl { };
       smtcoq = callPackage ../development/coq-modules/smtcoq { };
+      ssprove = callPackage ../development/coq-modules/ssprove {};
       stdpp = callPackage ../development/coq-modules/stdpp { };
       StructTact = callPackage ../development/coq-modules/StructTact {};
       tlc = callPackage ../development/coq-modules/tlc {};
-- 
cgit 1.4.1