GNU bug report logs - #73236
[PATCH 0/2] gnu: Add coq-actris.

Previous Next

Full log

Message #11 received at 73236 <at> debbugs.gnu.org (full text, mbox):

From: Antero Mejr <mail <at> antr.me>
To: 73236 <at> debbugs.gnu.org
Cc: pukkamustard <at> posteo.net, julien <at> lepiller.eu
Subject: [PATCH 2/2] gnu: Add coq-actris.
Date: Fri, 13 Sep 2024 20:52:44 +0000

* gnu/packages/coq.scm (coq-actris): New variable.

Change-Id: Ied7bff06ee88271400e145844139ded2f3c80108
---
 gnu/packages/coq.scm | 37 +++++++++++++++++++++++++++++++++++++
 1 file changed, 37 insertions(+)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index bd80cc4a34..1640e68b03 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -871,3 +871,40 @@ (define-public coq-iris
 reasoning about safety of concurrent programs, as the logic in logical
 relations, and to reason about type-systems, data-abstraction, etc.")
     (license license:bsd-3)))
+
+(define-public coq-actris
+  (let ((commit "18f784adb884ac14edd3eb19610d0b3fd62f4985") ;no tags
+        (revision "0"))
+    (package
+      (name "coq-actris")
+      (version (git-version "2.0" revision commit)) ;2.0 has subprotocols
+      (source (origin
+                (method git-fetch)
+                (uri (git-reference
+                      (url "https://gitlab.mpi-sws.org/iris/actris.git/")
+                      (commit commit)))
+                (file-name (git-file-name name version))
+                (sha256
+                 (base32
+                  "0d6xjccnk6jw530mzvs8gya3q3cck9jc8a9mb267d1dhypvdxc40"))))
+      (build-system gnu-build-system)
+      (arguments
+       (list #:parallel-build? #f ; non-deterministic failures
+             #:tests? #f ; no tests
+             #:make-flags #~(list (string-append "COQLIBINSTALL=" #$output
+                                                 "/lib/coq/user-contrib")
+                                  "NO_TEST=1"
+                                  "COQTOP=coqtop -Q theories actris")
+             #:phases #~(modify-phases %standard-phases
+                          (delete 'configure)
+                          (replace 'install
+                            (lambda* (#:key make-flags #:allow-other-keys)
+                              (apply invoke "make" "-f" "Makefile.coq"
+                                     "install" make-flags))))))
+      (propagated-inputs (list coq coq-iris))
+      (home-page "https://gitlab.mpi-sws.org/iris/actris")
+      (synopsis "Coq library for session types in separation logic")
+      (description
+       "This package provides a Coq library for proving functional correctness
+of programs that use message-passing concurrency.")
+      (license license:bsd-3))))
-- 
2.46.0

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.