* [bug#73236] [PATCH 0/2] gnu: Add coq-actris.
@ 2024-09-13 20:48 Antero Mejr via Guix-patches via
[not found] ` <handler.73236.B.172626053231570.ack@debbugs.gnu.org>
0 siblings, 1 reply; 3+ messages in thread
From: Antero Mejr via Guix-patches via @ 2024-09-13 20:48 UTC (permalink / raw)
To: 73236
This patchset adds the Coq verification library Actris, and its
dependency coq-iris.
^ permalink raw reply [flat|nested] 3+ messages in thread
* [bug#73236] [PATCH 1/2] gnu: Add coq-iris.
[not found] ` <handler.73236.B.172626053231570.ack@debbugs.gnu.org>
@ 2024-09-13 20:51 ` Antero Mejr via Guix-patches via
2024-09-13 20:52 ` [bug#73236] [PATCH 2/2] gnu: Add coq-actris Antero Mejr via Guix-patches via
1 sibling, 0 replies; 3+ messages in thread
From: Antero Mejr via Guix-patches via @ 2024-09-13 20:51 UTC (permalink / raw)
To: 73236; +Cc: pukkamustard, julien
* 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
^ permalink raw reply related [flat|nested] 3+ messages in thread
* [bug#73236] [PATCH 2/2] gnu: Add coq-actris.
[not found] ` <handler.73236.B.172626053231570.ack@debbugs.gnu.org>
2024-09-13 20:51 ` [bug#73236] [PATCH 1/2] gnu: Add coq-iris Antero Mejr via Guix-patches via
@ 2024-09-13 20:52 ` Antero Mejr via Guix-patches via
1 sibling, 0 replies; 3+ messages in thread
From: Antero Mejr via Guix-patches via @ 2024-09-13 20:52 UTC (permalink / raw)
To: 73236; +Cc: pukkamustard, julien
* 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
^ permalink raw reply related [flat|nested] 3+ messages in thread
end of thread, other threads:[~2024-09-13 20:54 UTC | newest]
Thread overview: 3+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2024-09-13 20:48 [bug#73236] [PATCH 0/2] gnu: Add coq-actris Antero Mejr via Guix-patches via
[not found] ` <handler.73236.B.172626053231570.ack@debbugs.gnu.org>
2024-09-13 20:51 ` [bug#73236] [PATCH 1/2] gnu: Add coq-iris Antero Mejr via Guix-patches via
2024-09-13 20:52 ` [bug#73236] [PATCH 2/2] gnu: Add coq-actris Antero Mejr via Guix-patches via
Code repositories for project(s) associated with this external index
https://git.savannah.gnu.org/cgit/guix.git
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.