[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

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

[Arnaud Daby-Seesaram via Guix-patches via]

[-- Attachment #1: Type: text/plain, Size: 2175 bytes --]

Hi Antero,

Thank you for your patches; I apologise for the response delay.

You will find a quick review below.

- Build: using your patch, both coq-iris and coq-actris can be
  successfully built (I only tried on a x86-64 machine with --rounds=3
  at the moment).

  However, I have a few questions:

  + I do not understand why COQTOP has to be specified in the
    #:make-flags.

  + Tests indeed fail if I switch #:tests? to #t.

    However, when I let the main build phase run the tests, they all
    seem to pass.  Do you experience the same result?
    If so, it could be worth it to (at least temporarily) allow tests in
    the main build phase (as is done in stdpp for example) and better
    understand where the issues come from.

  + Open question: would it be appropriate to split coq-iris across
    several outputs (main output for Iris, heap-lang, deprecated and
    unstable)?

  NB: I have not had the time to look at why there is a need to replace
      the install phase in coq-actris yet.

- Licenses: the licenses are correct.

- Home pages:
  + Iris: Ok.
  + Actris: you used a link to the GitLab repository.
    https://iris-project.org/actris/ might be more appropriate.

- Description fields:
  Descriptions are are usually phrased as "X is ...", where "X" is the
  name of the project.  Could you please rephrase the description in
  this style?

  Note: the Opam file of Iris reads "Iris is ..." too if you need a
  reference text.

- Documentation:
  It is very nice that you build and install iris.pdf.

  Do you think that adding a `native-search-paths' field to `coq-iris'
  (for variables "GUIX_TEXMF" and "BIBINPUTS") would be interesting?
  This way, `tex/iris.sty' and `tex/bib.bib' (maybe renamed into
  iris.bib) would be made available to TeX installations?


Sorry if writing my review as a list reads a bit cold (this is not my
intention); I just wanted to be as organised as possible.

Overall, thank you for you patches.  It would be nice to see
Iris-related stuff in Guix (and more generally more movement in the
OCaml/Coq worlds) :).

Best regards,

-- 
Arnaud

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 857 bytes --]