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

Previous Next

Full log

Message #8 received at 73236 <at> debbugs.gnu.org (full text, mbox):

From: Antero Mejr <mail <at> antr.me>
To: 73236 <at> debbugs.gnu.org
Cc: pukkamustard <at> posteo.net, julien <at> lepiller.eu
Subject: [PATCH 1/2] gnu: Add coq-iris.
Date: Fri, 13 Sep 2024 20:51:26 +0000

* 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

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.