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----- --=-=-=--
guix-patches@HIDDEN
:bug#73236
; Package guix-patches
.
Full text available.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
guix-patches@HIDDEN
:bug#73236
; Package guix-patches
.
Full text available.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
guix-patches@HIDDEN
:bug#73236
; Package guix-patches
.
Full text available.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.
Antero Mejr <mail@HIDDEN>
:guix-patches@HIDDEN
.
Full text available.guix-patches@HIDDEN
:bug#73236
; Package guix-patches
.
Full text available.
GNU bug tracking system
Copyright (C) 1999 Darren O. Benham,
1997 nCipher Corporation Ltd,
1994-97 Ian Jackson.