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

Please note: This is a static page, with minimal formatting, updated once a day.
Click here to see this page with the latest information and nicer formatting.

Package: guix-patches; Reported by: Antero Mejr <mail@HIDDEN>; Keywords: patch; dated Fri, 13 Sep 2024 20:49:01 UTC; Maintainer for guix-patches is guix-patches@HIDDEN.

Message received at 73236 <at> debbugs.gnu.org:


Received: (at 73236) by debbugs.gnu.org; 9 Oct 2024 12:19:14 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Wed Oct 09 08:19:14 2024
Received: from localhost ([127.0.0.1]:55897 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1syVer-0003ow-So
	for submit <at> debbugs.gnu.org; Wed, 09 Oct 2024 08:19:14 -0400
Received: from nanein.fr ([185.230.78.41]:42784)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <ds-ac@HIDDEN>) id 1syVeo-0003oe-Ls
 for 73236 <at> debbugs.gnu.org; Wed, 09 Oct 2024 08:19:11 -0400
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=nanein.fr; s=mail;
 t=1728476334; bh=qm/hH/ol/rwWHfzEXzqfDYmorfODcj3w1DqVTmxJIb8=;
 h=From:To:Cc:Subject:In-Reply-To:References:Date:From;
 b=m35eGemNS2+oS/T47oKRZ3vpnFbYun/iBf5F7WnJs6VBwP8Ki0102IhDBPh8/Fmhk
 IQ/Gdj75b60j3Wy0sqDbSGYRr1a5fcTd9xGngk9ig4sYi9DVDQwODymGlbho1OBUK2
 ukmXh6m/Yr7/oRn33wJeR6PZzg+wavMNReo98Uym0dd7vtbqgLR9pM1XhkWHsFAmsr
 3YNeCvJQACy60QKZbhAZpeo7GOqTaSAMtEb9JuTZX9micoo4bo4cYJ1Rm3sB+HVgJM
 6+AQ30El/1C94h9glRpZnUHrdtcnC9BjNjYKSbFTafaAm5LRWB18L5l2sNLj++T9Py
 6K60SZHwBe7Jfq2bHC4eX8vCj9qpOJl5rPbGl7B6zUuM3X+Q8Fjj8gJ95OKFSOHgWf
 kyRK5tVFNqAlRy+xQTAdoD/L7LRE14NctwFcXbvaXXL/8neubu6oNxLRxbQ1Oplb+g
 L8S8MHdAo9S7FNSud9ch3buXlB2NETBDuB+gx0xnXb0MXzBkEPhauvsN7NDYJhbTTa
 omMpZAZ8Sg0OCzdqXlmXbDaHCYstt1YNLPtQPyt1aqXsW70uWLazs9wM4nJ3WdrQBh
 Fk/ubZAZmHl4hUffScOlY7jNm80r5Ui3hRqVLaKp0tmrLdDMGo+6z/PVIQ+dJ55Jju
 4VUenSeRuEDloZSVZB1qZdlE=
Received: from cochea (eduroam09.au.dk [185.45.22.146])
 (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)
 key-exchange ECDHE (prime256v1) server-signature ECDSA (prime256v1)
 server-digest SHA256) (No client certificate requested)
 by nanein.fr (Postfix) with ESMTPSA id 11841140215;
 Wed,  9 Oct 2024 14:18:54 +0200 (CEST)
From: Arnaud Daby-Seesaram <ds-ac@HIDDEN>
To: 73236 <at> debbugs.gnu.org
Subject: Re: [bug#73236] [PATCH 0/2] gnu: Add coq-actris.
In-Reply-To: <87ed5n2sbi.fsf@HIDDEN> (Antero Mejr via Guix-patches via's
 message of "Fri, 13 Sep 2024 20:48:33 +0000")
References: <87ed5n2sbi.fsf@HIDDEN>
Date: Wed, 09 Oct 2024 14:18:42 +0200
Message-ID: <87ldyxzcyl.fsf@HIDDEN>
MIME-Version: 1.0
Content-Type: multipart/signed; boundary="=-=-=";
 micalg=pgp-sha512; protocol="application/pgp-signature"
X-Spam-Score: 0.0 (/)
X-Debbugs-Envelope-To: 73236
Cc: Antero Mejr <mail@HIDDEN>, pukkamustard@HIDDEN, julien@HIDDEN
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -1.0 (-)

--=-=-=
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: quoted-printable

Hi Antero,

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

You will find a quick review below.

=2D Build: using your patch, both coq-iris and coq-actris can be
  successfully built (I only tried on a x86-64 machine with --rounds=3D3
  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.

=2D Licenses: the licenses are correct.

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

=2D 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.

=2D 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=C2=A0just 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,

=2D-=20
Arnaud

--=-=-=
Content-Type: application/pgp-signature; name="signature.asc"

-----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-----
--=-=-=--




Information forwarded to guix-patches@HIDDEN:
bug#73236; Package guix-patches. Full text available.

Message received at 73236 <at> debbugs.gnu.org:


Received: (at 73236) by debbugs.gnu.org; 13 Sep 2024 20:53:07 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Fri Sep 13 16:53:07 2024
Received: from localhost ([127.0.0.1]:44333 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1spDHv-0008TO-Bu
	for submit <at> debbugs.gnu.org; Fri, 13 Sep 2024 16:53:07 -0400
Received: from smtp.forwardemail.net ([207.246.76.47]:20585)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <SRS0=0bc9=QM=antr.me=mail@HIDDEN>)
 id 1spDHt-0008Sn-AO
 for 73236 <at> debbugs.gnu.org; Fri, 13 Sep 2024 16:53:05 -0400
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=antr.me;
 h=Content-Type: MIME-Version: Message-ID: Date: References: In-Reply-To:
 Subject: Cc: To: From; q=dns/txt; s=fe-d5cf982890; t=1726260767;
 bh=Tymug9I413kd/K47sbJMAPPR9GpKTG0udTRTH4uNQpE=;
 b=UK5tDPPF4vzsrN84qW2NWQL/J36apvyR+7VB/4CP7i1p/FDUcF9htIFlc83JfgkbokIZ6+Kn5
 SpLwAu7adGWPDhVOKDIBToEJ3so0R+gw7DzrobdpX7PS/bkhm+62WW36Q4J/k6DoJL4UB1nCsH0
 kuyCrykNyyPBar7wdk/Jt8Q=
From: Antero Mejr <mail@HIDDEN>
To: 73236 <at> debbugs.gnu.org
Subject: [PATCH 2/2] gnu: Add coq-actris.
In-Reply-To: <handler.73236.B.172626053231570.ack <at> debbugs.gnu.org> (GNU bug
 Tracking System's message of "Fri, 13 Sep 2024 20:49:02 +0000")
References: <87ed5n2sbi.fsf@HIDDEN>
 <handler.73236.B.172626053231570.ack <at> debbugs.gnu.org>
Date: Fri, 13 Sep 2024 20:52:44 +0000
Message-ID: <874j6j2s4j.fsf_-_@HIDDEN>
MIME-Version: 1.0
Content-Type: text/plain
X-Report-Abuse-To: abuse@HIDDEN
X-Report-Abuse: abuse@HIDDEN
X-Complaints-To: abuse@HIDDEN
X-ForwardEmail-Version: 0.4.40
X-ForwardEmail-Sender: rfc822; mail@HIDDEN, smtp.forwardemail.net,
 207.246.76.47
X-ForwardEmail-ID: 66e4a61e6c57d9a68975c6df
X-Spam-Score: -0.0 (/)
X-Debbugs-Envelope-To: 73236
Cc: pukkamustard@HIDDEN, julien@HIDDEN
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -1.0 (-)


* 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





Information forwarded to guix-patches@HIDDEN:
bug#73236; Package guix-patches. Full text available.

Message received at 73236 <at> debbugs.gnu.org:


Received: (at 73236) by debbugs.gnu.org; 13 Sep 2024 20:51:51 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Fri Sep 13 16:51:51 2024
Received: from localhost ([127.0.0.1]:44329 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1spDGg-0008Qs-Nw
	for submit <at> debbugs.gnu.org; Fri, 13 Sep 2024 16:51:51 -0400
Received: from smtp.forwardemail.net ([207.246.76.47]:26057)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <SRS0=0bc9=QM=antr.me=mail@HIDDEN>)
 id 1spDGd-0008QZ-Hj
 for 73236 <at> debbugs.gnu.org; Fri, 13 Sep 2024 16:51:48 -0400
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=antr.me;
 h=Content-Type: MIME-Version: Message-ID: Date: References: In-Reply-To:
 Subject: Cc: To: From; q=dns/txt; s=fe-d5cf982890; t=1726260689;
 bh=5LC5/des+518xYcfmHnOLoA72L1c4HQ7DAuv9kytD1w=;
 b=pRI8X8olj0LZInfPJHShSP6PItJ08Hhl5aXoEp3CtSxWcoUcMUt6dsTeKmZybn8KdvV7ubjXm
 oN5Q6IiWZTUmMUpBhtX/id+Udfyz1vjXrtlsg+yg6Yipyo8u1SDDfF4kkYrEy4sdbNZIaFYN/En
 BG4JHWyr9iY4+8zMWFh0CKM=
From: Antero Mejr <mail@HIDDEN>
To: 73236 <at> debbugs.gnu.org
Subject: [PATCH 1/2] gnu: Add coq-iris.
In-Reply-To: <handler.73236.B.172626053231570.ack <at> debbugs.gnu.org> (GNU bug
 Tracking System's message of "Fri, 13 Sep 2024 20:49:02 +0000")
References: <87ed5n2sbi.fsf@HIDDEN>
 <handler.73236.B.172626053231570.ack <at> debbugs.gnu.org>
Date: Fri, 13 Sep 2024 20:51:26 +0000
Message-ID: <87a5gb2s6p.fsf_-_@HIDDEN>
User-Agent: Gnus/5.13 (Gnus v5.13)
MIME-Version: 1.0
Content-Type: text/plain
X-Report-Abuse-To: abuse@HIDDEN
X-Report-Abuse: abuse@HIDDEN
X-Complaints-To: abuse@HIDDEN
X-ForwardEmail-Version: 0.4.40
X-ForwardEmail-Sender: rfc822; mail@HIDDEN, smtp.forwardemail.net,
 207.246.76.47
X-ForwardEmail-ID: 66e4a5cf6c57d9a68975c649
X-Spam-Score: -0.0 (/)
X-Debbugs-Envelope-To: 73236
Cc: pukkamustard@HIDDEN, julien@HIDDEN
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -1.0 (-)


* 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





Information forwarded to guix-patches@HIDDEN:
bug#73236; Package guix-patches. Full text available.

Message received at submit <at> debbugs.gnu.org:


Received: (at submit) by debbugs.gnu.org; 13 Sep 2024 20:48:52 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Fri Sep 13 16:48:52 2024
Received: from localhost ([127.0.0.1]:44324 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1spDDo-0008D7-7E
	for submit <at> debbugs.gnu.org; Fri, 13 Sep 2024 16:48:52 -0400
Received: from lists.gnu.org ([209.51.188.17]:51044)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <SRS0=0bc9=QM=antr.me=mail@HIDDEN>)
 id 1spDDm-0008Cx-40
 for submit <at> debbugs.gnu.org; Fri, 13 Sep 2024 16:48:50 -0400
Received: from eggs.gnu.org ([2001:470:142:3::10])
 by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
 (Exim 4.90_1)
 (envelope-from <SRS0=0bc9=QM=antr.me=mail@HIDDEN>)
 id 1spDDc-0003RH-6J
 for guix-patches@HIDDEN; Fri, 13 Sep 2024 16:48:40 -0400
Received: from smtp.forwardemail.net ([149.28.215.223])
 by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128)
 (Exim 4.90_1)
 (envelope-from <SRS0=0bc9=QM=antr.me=mail@HIDDEN>)
 id 1spDDa-000369-Mk
 for guix-patches@HIDDEN; Fri, 13 Sep 2024 16:48:39 -0400
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=antr.me;
 h=Content-Type: MIME-Version: Message-ID: Date: Subject: To: From;
 q=dns/txt; s=fe-d5cf982890; t=1726260515;
 bh=0FMtVPqALx1c3GLgtVErL5zyVkGDaw+trhIsTfDTiHM=;
 b=OUl7ilYxSyr6kZeW133gz+yPqdSkEDxJeMuSheVJc0azXST/lOZjKz21ATIPenR0oClXPhvtG
 C8oDL2ZEslsPpfmtah5UpadyDhRIQpq6k7aZVsgMR8NafpQySbLWxaqzAuxpIwVb6uliTdhMtPU
 8XqT69nJLii4olh8KIDkeY0=
From: Antero Mejr <mail@HIDDEN>
To: guix-patches@HIDDEN
Subject: [PATCH 0/2] gnu: Add coq-actris.
Date: Fri, 13 Sep 2024 20:48:33 +0000
Message-ID: <87ed5n2sbi.fsf@HIDDEN>
User-Agent: Gnus/5.13 (Gnus v5.13)
MIME-Version: 1.0
Content-Type: text/plain
X-Report-Abuse-To: abuse@HIDDEN
X-Report-Abuse: abuse@HIDDEN
X-Complaints-To: abuse@HIDDEN
X-ForwardEmail-Version: 0.4.40
X-ForwardEmail-Sender: rfc822; mail@HIDDEN, smtp.forwardemail.net,
 149.28.215.223
X-ForwardEmail-ID: 66e4a5226c57d9a68975c597
Received-SPF: pass client-ip=149.28.215.223;
 envelope-from=SRS0=0bc9=QM=antr.me=mail@HIDDEN;
 helo=smtp.forwardemail.net
X-Spam_score_int: -20
X-Spam_score: -2.1
X-Spam_bar: --
X-Spam_report: (-2.1 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1,
 DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, SPF_HELO_PASS=-0.001,
 SPF_PASS=-0.001 autolearn=ham autolearn_force=no
X-Spam_action: no action
X-Spam-Score: -1.4 (-)
X-Debbugs-Envelope-To: submit
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -2.4 (--)

This patchset adds the Coq verification library Actris, and its
dependency coq-iris.




Acknowledgement sent to Antero Mejr <mail@HIDDEN>:
New bug report received and forwarded. Copy sent to guix-patches@HIDDEN. Full text available.
Report forwarded to guix-patches@HIDDEN:
bug#73236; Package guix-patches. Full text available.
Please note: This is a static page, with minimal formatting, updated once a day.
Click here to see this page with the latest information and nicer formatting.
Last modified: Sun, 12 Jan 2025 05:45:02 UTC

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