diff mbox series

[bug#73236,2/2] gnu: Add coq-actris.

Message ID 874j6j2s4j.fsf_-_@antr.me
State New
Headers show
Series gnu: Add coq-actris. | expand

Commit Message

Antero Mejr Sept. 13, 2024, 8:52 p.m. UTC 
* gnu/packages/coq.scm (coq-actris): New variable.

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

Patch

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))))