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