From a9352d446b34e76341ef748b375716ca4051baa2 Mon Sep 17 00:00:00 2001
From: Chandradeep Dey <codesigning@chandradeepdey.com>
Date: Tue, 6 Oct 2026 16:28:36 -0400
Subject: [PATCH] rocqPackages.actris: init at 4.5.0

Actris is a framework for session-protocol reasoning in Iris.
Version 4.5.0 is released in the rocq-prover opam repository as
rocq-actris, and builds against Iris 4.5.0.

Assisted-by: Claude Code (Claude Opus 5.5)
---
 .../rocq-modules/actris/default.nix           | 35 +++++++++++++++++++
 pkgs/top-level/coq-packages.nix               |  1 +
 pkgs/top-level/rocq-packages.nix              |  1 +
 3 files changed, 37 insertions(+)
 create mode 100644 pkgs/development/rocq-modules/actris/default.nix

diff --git a/pkgs/development/rocq-modules/actris/default.nix b/pkgs/development/rocq-modules/actris/default.nix
new file mode 100644
index 000000000000..a8558d35d51e
--- /dev/null
+++ b/pkgs/development/rocq-modules/actris/default.nix
@@ -0,0 +1,35 @@
+{
+  lib,
+  mkRocqDerivation,
+  iris,
+  version ? null,
+}:
+
+mkRocqDerivation {
+  pname = "actris";
+  # MPI's gitlab is unfortunately under siege of various LLM scrappers
+  # and had to establish some strong rate limiting, a mirror is put on github
+  # domain = "gitlab.mpi-sws.org";
+  # owner = "iris";
+  owner = "rocq-iris";
+  inherit version;
+  defaultVersion =
+    let
+      case = case: out: { inherit case out; };
+    in
+    with lib.versions;
+    lib.switch iris.version [
+      (case (isEq "4.5.0") "4.5.0")
+    ] null;
+  release."4.5.0".hash = "sha256-Kp3YDN2C2QNIDHfg9AJGfOjQ/9sM2MHRICO8iPgYdBw=";
+  releaseRev = v: "actris-${v}";
+
+  propagatedBuildInputs = [ iris ];
+
+  meta = {
+    description = "Framework for session protocol reasoning in Iris";
+    homepage = "https://iris-project.org/actris";
+    license = lib.licenses.bsd3;
+    maintainers = with lib.maintainers; [ chandradeepdey ];
+  };
+}
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index 4657ec7e7a5c..d0e9e2f4db52 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -70,6 +70,7 @@ let
       contribs = lib.recurseIntoAttrs (callPackage ../development/rocq-modules/contribs { });
 
       aac-tactics = callPackage ../development/rocq-modules/aac-tactics { };
+      actris = callPackage ../development/rocq-modules/actris { };
       addition-chains = callPackage ../development/rocq-modules/addition-chains { };
       async-test = callPackage ../development/rocq-modules/async-test { };
       atbr = callPackage ../development/rocq-modules/atbr { };
diff --git a/pkgs/top-level/rocq-packages.nix b/pkgs/top-level/rocq-packages.nix
index 78af819bd3a0..035d83a3123c 100644
--- a/pkgs/top-level/rocq-packages.nix
+++ b/pkgs/top-level/rocq-packages.nix
@@ -69,6 +69,7 @@ let
       contribs = lib.recurseIntoAttrs (callPackage ../development/rocq-modules/contribs { });
 
       aac-tactics = callPackage ../development/rocq-modules/aac-tactics { };
+      actris = callPackage ../development/rocq-modules/actris { };
       addition-chains = callPackage ../development/rocq-modules/addition-chains { };
       async-test = callPackage ../development/rocq-modules/async-test { };
       atbr = callPackage ../development/rocq-modules/atbr { };