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)
This commit is contained in:
Chandradeep Dey
2026-10-06 16:28:36 -04:00
parent 80d7c6c6bf
commit a9352d446b
3 changed files with 37 additions and 0 deletions

View File

@@ -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 ];
};
}

View File

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

View File

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