(address . guix-patches@gnu.org)
87ed5n2sbi.fsf@antr.me
This patchset adds the Coq verification library Actris, and its
dependency coq-iris.
[PATCH 0/2] gnu: Add coq-actris.
- Open
Details
- 2 participants
- Arnaud Daby-Seesaram
- Antero Mejr
- Owner
- unassigned
- Submitted by
- Antero Mejr
- Severity
- normal
A
A
[PATCH 1/2] gnu: Add coq-iris.
(address . 73236@debbugs.gnu.org)
87a5gb2s6p.fsf_-_@antr.me
* gnu/packages/coq.scm (coq-iris): New variable.
Change-Id: I3841ab402fe82149996e1413f9ab3a475f4859d9
---
gnu/packages/coq.scm | 94 ++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 94 insertions(+)
Toggle diff (113 lines)
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
A
[PATCH 2/2] gnu: Add coq-actris.
(address . 73236@debbugs.gnu.org)
874j6j2s4j.fsf_-_@antr.me
* gnu/packages/coq.scm (coq-actris): New variable.
Change-Id: Ied7bff06ee88271400e145844139ded2f3c80108
---
gnu/packages/coq.scm | 37 +++++++++++++++++++++++++++++++++++++
1 file changed, 37 insertions(+)
Toggle diff (47 lines)
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
A
Re: [bug#73236] [PATCH 0/2] gnu: Add coq-actris.
(address . 73236@debbugs.gnu.org)
87ldyxzcyl.fsf@nanein.fr
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
-----BEGIN PGP SIGNATURE-----
iQJEBAEBCgAuFiEEMgqfJ4U0fby1t860ojLKXoMTiAwFAmcGdKMQHGRzLWFjQG5h
bmVpbi5mcgAKCRCiMspegxOIDDulD/9kyPD8eewzWm4Y3bR1Pv6IVPSI78D7CqkN
MvVa2fV+Vp50+ICK5q66iqpvDnaHjxOUEs8NYY8wxDs5bo1ypbmTqCBE6kusiTAT
09MasEQjb3G4Cy6s/hC48+4V5yAhbkOjUGsY3oGgbOXMkPdXlaaTqSZ9bbacVorV
Io31GziAb7GCo4iXKYIHIV3q+lbcvrRXGfeYPiWeEQ6vYFkrblw5UoQU2y46fGjW
SXfTBPVNaeXjgR1xKcZ99XGez98PFeJh8jENAI9pUlnQE9RgzCFW+A6STPwfSkwY
SiDomUCN852h/7pLsYZ+8ghIOFLsKaqlOK5rQA2ZaJ9sARd0DuVIqZIeKllGlO+T
bYoRJxFBKA6oGX7ronXTHwSN2Gtl7AarcR+cIG+i8DhWLJ1gI3i3xdFq3dNOHASF
n5ktJ5y7O4AUSFALWZvBHl8p4461s8ODVQ1yluhy/Esk1Dwu0jLTIGBtMP4syc//
z9raZFl9PdxMe+3S0ok6QEkKwQool9qbN04NteuXb47wCiOiCpFtV99nHXJP5IQM
q7tBZPOOXCI5kR7cZ/NvWj4l/8ybocVutsqucETqr5hSHJ+K2sVKFVACKXtbaOjw
YxUhZDlELZSWPODrOsm49rNq/tT/2xodTtq+Z0xnJXTPB28+ROo6rV/qTw5m7SRd
YqQhtsDWaw==
=J9Av
-----END PGP SIGNATURE-----
?