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

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

[Antero Mejr via Guix-patches via]

This patchset adds the Coq verification library Actris, and its
dependency coq-iris.

[bug#73236] [PATCH 1/2] gnu: Add coq-iris.

[Antero Mejr via Guix-patches via]

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

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

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 31d1e8d51d..bd80cc4a34 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -42,6 +42,7 @@ (define-module (gnu packages coq)
   #:use-module (gnu packages perl)
   #:use-module (gnu packages python)
   #:use-module (gnu packages rsync)
+  #:use-module (gnu packages tex)
   #:use-module (gnu packages texinfo)
   #:use-module (guix build-system dune)
   #:use-module (guix build-system gnu)
@@ -777,3 +778,96 @@ (define-public coq-mathcomp-bigenough
 purposes as @code{bigenough} will be subsumed by the near tactics.  The
 formalization is based on the Mathematical Components library.")
     (license license:cecill-b)))
+
+(define-public coq-iris
+  (package
+    (name "coq-iris")
+    (version "4.2.0")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://gitlab.mpi-sws.org/iris/iris.git/")
+                    (commit (string-append "iris-" version))))
+              (file-name (git-file-name name version))
+              (sha256
+               (base32
+                "1wr1jigzgl4fajl5jv4lanmb8nk4k6wdakakmxhfp5drxwhqgs0y"))))
+    (build-system gnu-build-system)
+    (arguments
+     (list #:parallel-build? #f ; non-deterministic failures
+           #:tests? #f ; 3 proof failures, appears formatting-related
+           #:test-target "test"
+           #:make-flags #~(list (string-append "COQLIBINSTALL=" #$output
+                                               "/lib/coq/user-contrib")
+                                ;; Coq interleaves tests into the build.
+                                ;; Work around this in the check phase.
+                                "NO_TEST=1"
+                                ;; Load mappings from _CoqProject into coqtop
+                                ;; TODO: can this be automated?
+                                "COQTOP=coqtop -Q iris/prelude iris.prelude \
+-Q iris/algebra iris.algebra \
+-Q iris/si_logic iris.si_logic \
+-Q iris/bi iris.bi \
+-Q iris/proofmode iris.proofmode \
+-Q iris/base_logic iris.base_logic \
+-Q iris/program_logic iris.program_logic \
+-Q iris_heap_lang iris.heap_lang \
+-Q iris_unstable iris.unstable \
+-Q iris_deprecated iris.deprecated")
+           #:phases #~(modify-phases %standard-phases
+                        (delete 'configure)
+                        (add-after 'build 'build-doc
+                          (lambda _
+                            (with-directory-excursion "tex"
+                              (invoke "make"))))
+                        (replace 'check
+                          (lambda* (#:key tests? test-target parallel-build?
+                                    make-flags #:allow-other-keys)
+                            (when tests?
+                              (apply invoke "make" "-f" "Makefile.coq.local"
+                                     "-j" (number->string
+                                           (if parallel-build?
+                                               (parallel-job-count)
+                                               1))
+                                     test-target make-flags))))
+                        (add-after 'install 'install-doc
+                          (lambda _
+                            (install-file
+                             "tex/iris.pdf"
+                             (string-append #$output
+                                            "/share/doc/iris/iris.pdf")))))))
+    (native-inputs (list (texlive-updmap.cfg
+                          (list texlive-amsfonts
+                                texlive-amsmath
+                                texlive-babel
+                                texlive-biber
+                                texlive-biblatex
+                                texlive-csquotes
+                                texlive-dashbox
+                                texlive-enumitem
+                                texlive-faktor
+                                texlive-geometry
+                                texlive-hyperref
+                                texlive-ifmtarg
+                                texlive-latexmk
+                                texlive-marvosym
+                                texlive-mathpartir
+                                texlive-mathtools
+                                texlive-microtype
+                                texlive-pgf
+                                texlive-scalerel
+                                texlive-semantic
+                                texlive-stmaryrd
+                                texlive-tabbing
+                                texlive-tensor
+                                texlive-xcolor
+                                texlive-xifthen))))
+    (propagated-inputs (list coq coq-stdpp))
+    (home-page "https://iris-project.org/")
+    (synopsis "Concurrent separation logic library for Coq")
+    (description
+     "This package provides a higher-order concurrent separation logic
+library, implemented and verified in the Coq proof assistant.  It is used for
+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)))

base-commit: 0e0d9bc91f20ac6dda439ab09330f0163eb9bf42
-- 
2.46.0

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

[Antero Mejr via Guix-patches via]

* 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