GNU bug report logs - #57540
[PATCH] Add ocaml-elpi (a dependency of coq-mathcomp-analysis)

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: Garek Dyszel <garekdyszel@HIDDEN>; Keywords: patch; dated Fri, 2 Sep 2022 07:46:01 UTC; Maintainer for guix-patches is guix-patches@HIDDEN.

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


Received: (at 57540) by debbugs.gnu.org; 24 Sep 2022 13:05:31 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Sat Sep 24 09:05:31 2022
Received: from localhost ([127.0.0.1]:42654 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1oc4qZ-0001O4-L8
	for submit <at> debbugs.gnu.org; Sat, 24 Sep 2022 09:05:31 -0400
Received: from eggs.gnu.org ([209.51.188.92]:35576)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <ludo@HIDDEN>) id 1oc4qV-0001Np-Tl
 for 57540 <at> debbugs.gnu.org; Sat, 24 Sep 2022 09:05:29 -0400
Received: from fencepost.gnu.org ([2001:470:142:3::e]:57928)
 by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
 (Exim 4.90_1) (envelope-from <ludo@HIDDEN>)
 id 1oc4qP-0006R2-B2; Sat, 24 Sep 2022 09:05:21 -0400
DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=gnu.org;
 s=fencepost-gnu-org; h=MIME-Version:In-Reply-To:Date:References:Subject:To:
 From; bh=plcAdgZ7CwOAkz74verKnPG+VWaBP2awvPg4dJMarO8=; b=O72WCtNJh8EMeRGeaLvr
 e2UVnValxsV4s+aoqvxMqCTMBGYPZ/jVVYVm4tnFIvnvfz1M5oom8rcfOwXDeksWqBEcHqnwnI//B
 n5TLnk+ua+Ipjf30d7vWpMHNVFfC/c/nayo2nlVfmLlAguj7h9bIgwgLTd/lX5ouuupkWUw+X7zuI
 DNrgiJSjASdBI6F8AMQunBDJW9kfegCqQAGAGKAKmj+HtDkhhWk6mkeVwb9qQ1IsVqeP3wtvEmrO6
 Bkfk/gzay8uEobMow5Y8LTZyNhAMAF3MqzXG7lWbdLzyuVMm16XKYINvvR3mgc65kvX8XCB0DzNSN
 oxD73MiV8xGpew==;
Received: from 91-160-117-201.subs.proxad.net ([91.160.117.201]:55467
 helo=ribbon)
 by fencepost.gnu.org with esmtpsa (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
 (Exim 4.90_1) (envelope-from <ludo@HIDDEN>)
 id 1oc4qO-0006vN-0J; Sat, 24 Sep 2022 09:05:20 -0400
From: =?utf-8?Q?Ludovic_Court=C3=A8s?= <ludo@HIDDEN>
To: Julien Lepiller <julien@HIDDEN>
Subject: Re: bug#57540: [PATCH] Add ocaml-elpi (a dependency of
 coq-mathcomp-analysis)
References: <79d544f7d8ba64b631a6f0f1d2ef0b08@HIDDEN>
 <20220903204035.22e3b372@HIDDEN>
Date: Sat, 24 Sep 2022 15:05:18 +0200
In-Reply-To: <20220903204035.22e3b372@HIDDEN> (Julien Lepiller's
 message of "Sat, 3 Sep 2022 20:40:35 +0200")
Message-ID: <87tu4wapo1.fsf_-_@HIDDEN>
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/28.1 (gnu/linux)
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: quoted-printable
X-Spam-Score: -2.3 (--)
X-Debbugs-Envelope-To: 57540
Cc: Garek Dyszel <garekdyszel@HIDDEN>, 57540 <at> debbugs.gnu.org
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: -3.3 (---)

Hi Julien,

Julien Lepiller <julien@HIDDEN> skribis:

> thanks for the patches! As I understand it, these patches introduce 8
> new packages, but I count only 7 (with this one which didn't make it as
> a part of the series). Could you split the last patch, so each new
> package has its own patch?

Could you take a look at v2 of this patch series?

  https://issues.guix.gnu.org/57540

TIA!

Ludo=E2=80=99.




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

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


Received: (at 57540) by debbugs.gnu.org; 7 Sep 2022 18:35:06 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Wed Sep 07 14:35:06 2022
Received: from localhost ([127.0.0.1]:56275 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1oVztC-00083x-7f
	for submit <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:35:06 -0400
Received: from knopi.disroot.org ([178.21.23.139]:32924)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <garekdyszel@HIDDEN>) id 1oVztA-00083M-P5
 for 57540 <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:35:05 -0400
Received: from localhost (localhost [127.0.0.1])
 by disroot.org (Postfix) with ESMTP id 3CC6340121
 for <57540 <at> debbugs.gnu.org>; Wed,  7 Sep 2022 20:35:04 +0200 (CEST)
X-Virus-Scanned: SPAM Filter at disroot.org
Received: from knopi.disroot.org ([127.0.0.1])
 by localhost (disroot.org [127.0.0.1]) (amavisd-new, port 10024)
 with ESMTP id 9gu3jbYuCeZu for <57540 <at> debbugs.gnu.org>;
 Wed,  7 Sep 2022 20:35:02 +0200 (CEST)
From: Garek Dyszel <garekdyszel@HIDDEN>
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=disroot.org; s=mail;
 t=1662575697; bh=g9vGwd9z/ETUQ9QKviACR0QH0Rz3kAjBdyhcTQ51ca0=;
 h=From:To:Subject:Date;
 b=ED9O/1swzQ+MwbkHggXC3Q4RiaL/nvOeyoxC4qQfJEWrJPFcXy1FyHO5NGROHc+t5
 w+3vswpRDM6wduFktLDp+KmebT7yJEcRXBZXQSFeYpoisWwOJeahNXvr3RJ85Uta9E
 eT9iPj+nJ0UbzL8pmfJs4gGWICr27S5SNh9yAkmB/rww08sKWd7LSkcegf/GXt/R/M
 /YwsQZcxD58Xby9Dd1gYxuqXIFgxlcWL5Kw5TUMoU+rFsjHniWQsBFYxUM8nVJ1ssk
 k+Va9mX2d7mh4danj1Pd3L6lBJ9mMArZ5BkZNLMAdEuXwlJdnNPvEkm2TbRoR3hikS
 /1KRMknEa/8bA==
To: 57540 <at> debbugs.gnu.org
Subject: [RFC PATCH v2 19/19] gnu: Add python-jsonschema-4.15.*
 gnu/packages/python-xyz.scm (python-jsonschema-4.15): New variable.
Date: Wed, 07 Sep 2022 14:34:55 -0400
Message-ID: <8735d3vxrk.fsf@HIDDEN>
Mime-Version: 1.0
Content-Type: text/plain
X-Spam-Score: -0.0 (/)
X-Debbugs-Envelope-To: 57540
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/python-xyz.scm (python-jsonschema-4.15): New variable.
---
 gnu/packages/python-xyz.scm | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)

diff --git a/gnu/packages/python-xyz.scm b/gnu/packages/python-xyz.scm
index 0e67adc95f..fd470652bc 100644
--- a/gnu/packages/python-xyz.scm
+++ b/gnu/packages/python-xyz.scm
@@ -3661,6 +3661,37 @@ (define-public python-jsonschema-next
            python-pyrsistent
            python-typing-extensions))))
 
+(define-public python-jsonschema-4.15
+  (package
+    (inherit python-jsonschema)
+    (name "python-jsonschema-4.15")
+    (version "4.15.0")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://github.com/python-jsonschema/jsonschema")
+                    (commit (string-append "v" version))))
+              (file-name (git-file-name name version))
+              (sha256
+               (base32
+                "1yv01id6l0s1dq6khal9jvxh9dqivy394z04y6yr5lv8cimwcx2x"))))
+    (native-inputs (list python-pypa-build
+                         python-twisted
+                         python-hatchling
+                         python-pathspec
+                         python-pluggy-1.0
+                         python-editables
+                         python-hatch-vcs
+                         python-setuptools-scm-7
+                         python-hatch-fancy-pypi-readme))
+    (propagated-inputs (list python-attrs python-importlib-metadata
+                             python-pyrsistent python-typing-extensions
+                             python-hatch-vcs))
+    (arguments
+     (substitute-keyword-arguments
+         (package-arguments python-jsonschema-next)))
+    (home-page "https://github.com/python-jsonschema/jsonschema")))
+
 (define-public python-schema
   (package
     (name "python-schema")
-- 
2.37.2






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

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


Received: (at 57540) by debbugs.gnu.org; 7 Sep 2022 18:35:03 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Wed Sep 07 14:35:03 2022
Received: from localhost ([127.0.0.1]:56265 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1oVzt8-00082r-Mq
	for submit <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:35:03 -0400
Received: from knopi.disroot.org ([178.21.23.139]:60036)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <garekdyszel@HIDDEN>) id 1oVzt6-00082S-CP
 for 57540 <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:35:00 -0400
Received: from localhost (localhost [127.0.0.1])
 by disroot.org (Postfix) with ESMTP id B671640122
 for <57540 <at> debbugs.gnu.org>; Wed,  7 Sep 2022 20:34:59 +0200 (CEST)
X-Virus-Scanned: SPAM Filter at disroot.org
Received: from knopi.disroot.org ([127.0.0.1])
 by localhost (disroot.org [127.0.0.1]) (amavisd-new, port 10024)
 with ESMTP id DeafAPK9giHU for <57540 <at> debbugs.gnu.org>;
 Wed,  7 Sep 2022 20:34:58 +0200 (CEST)
From: Garek Dyszel <garekdyszel@HIDDEN>
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=disroot.org; s=mail;
 t=1662575692; bh=BWKRHB92GdCjU7/e0hRzydKCWqahqYhmTbsVVNgtGw4=;
 h=From:To:Subject:Date;
 b=WggLOA7izDvpLeivq1gA6EITKPSKO8A6ccwvMvHf/d21I+COltUY7LG9ngSXexsG1
 Z8scItE6cvQLu7U8KBF6EukgYX6xgXk+q1sk7hxiPvozCGb5U/UvYmUzYNZ1+Y3Tlp
 YB7upTMtIIVNOcwXk0LefysDo3nLRLE/cqbmHRar4Q6SaUnNtiikG5DjOMdsaP63S9
 C20Gooew1185aPYKFEQIc/hHxJxD3jNQHDlPmhqFFfmDpGHvKY7JNSFRyDjtDY9LOX
 fK52c7Gy3CvttNzEcn8quNYl2K5IZ2KUNui72uvyLNpDu2El6O1YW79ctJfKCUZw4X
 o6a9LQJsbnmRA==
To: 57540 <at> debbugs.gnu.org
Subject: [RFC PATCH v2 18/19] gnu: Add python-setuptools-scm-7.*
 gnu/packages/python.xyz.scm (python-setuptools-scm-7): New variable.
Date: Wed, 07 Sep 2022 14:34:49 -0400
Message-ID: <874jxjvxrq.fsf@HIDDEN>
Mime-Version: 1.0
Content-Type: text/plain
X-Spam-Score: -0.0 (/)
X-Debbugs-Envelope-To: 57540
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/python.xyz.scm (python-setuptools-scm-7): New variable.
---
 gnu/packages/python-xyz.scm | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)

diff --git a/gnu/packages/python-xyz.scm b/gnu/packages/python-xyz.scm
index 7febf50286..0e67adc95f 100644
--- a/gnu/packages/python-xyz.scm
+++ b/gnu/packages/python-xyz.scm
@@ -20859,6 +20859,38 @@ (define-public python-setuptools-scm-git-archive
 belong to tagged versions.")
     (license license:expat)))
 
+(define-public python-setuptools-scm-7
+  ;; The version tags are inaccurate. Use the bare commit.
+  (let ((commit "c4d37004ab0a16c2cacdc58ef06b36956db02a9f")
+        (revision "1"))
+    (package
+      (name "python-setuptools-scm")
+      (version (git-version "7.0.5" revision commit))
+      (source (origin
+                ;; Won't build with git. Fails with error:
+                ;; "ERROR Backend subproccess exited when trying to invoke
+                ;; get_requires_for_build_wheel"
+                ;;
+                ;; The PyPi version has no such issue.
+                (method url-fetch)
+                (uri (pypi-uri "setuptools_scm" version))
+                (sha256
+                 (base32
+                  "0i28zghzdzzkm9w8rrjwphggkfs58nh6xnqsjhmqjvqxfypi67h3"))))
+      (build-system python-build-system)
+      (propagated-inputs (list python-importlib-metadata python-packaging
+                               python-tomli python-typing-extensions))
+      (native-inputs (list python
+                           python-pypa-build
+                           python-pytest
+                           python-virtualenv
+                           git-minimal
+                           mercurial))
+      (home-page "https://github.com/pypa/setuptools_scm/")
+      (synopsis "The blessed package to manage your versions by scm tags")
+      (description "The blessed package to manage your versions by scm tags.")
+      (license license:expat))))
+
 (define-public python-setuptools-git
   (package
     (name "python-setuptools-git")
-- 
2.37.2






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

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


Received: (at 57540) by debbugs.gnu.org; 7 Sep 2022 18:34:59 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Wed Sep 07 14:34:59 2022
Received: from localhost ([127.0.0.1]:56261 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1oVzt5-00082L-Ab
	for submit <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:34:59 -0400
Received: from knopi.disroot.org ([178.21.23.139]:59208)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <garekdyszel@HIDDEN>) id 1oVzt3-00082D-AK
 for 57540 <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:34:57 -0400
Received: from localhost (localhost [127.0.0.1])
 by disroot.org (Postfix) with ESMTP id AF97149FD6
 for <57540 <at> debbugs.gnu.org>; Wed,  7 Sep 2022 20:34:56 +0200 (CEST)
X-Virus-Scanned: SPAM Filter at disroot.org
Received: from knopi.disroot.org ([127.0.0.1])
 by localhost (disroot.org [127.0.0.1]) (amavisd-new, port 10024)
 with ESMTP id btY7u-U1kctN for <57540 <at> debbugs.gnu.org>;
 Wed,  7 Sep 2022 20:34:55 +0200 (CEST)
From: Garek Dyszel <garekdyszel@HIDDEN>
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=disroot.org; s=mail;
 t=1662575687; bh=OBlatGYCybQ3KdpAtBcmJWPWG4m2xCmIQgbQQc01lYs=;
 h=From:To:Subject:Date;
 b=fys9ccMGQHNYLsmakK8bzTxjUVSOg8quHZ6+8LrCGyP3L4wC10Vj/Zz/aDVp/euFl
 4IJW4HAC1YdM1T8sZtmiXQVgpclXb42ncEHcHNV3urzeu680Ft3TidX9zktT+nzzmD
 qG5FjspPzzFvW1tCPumUFZQ5WywzuMyk50U7hCvyU/vmZKIqQjB0c8wl5rHBi8yOOv
 diI8nn/kEEpK4EOl0oLVawBUkTbKyrJ8zDtSSrxBBCZEcb9rx28Ad5kAYB16SQk6Cf
 PcMvwkoEnozVfKriFVfdSjFyQFfoizCThwRITj1SChbA9dcfW4jNcZU2pEb2AEBhM9
 NubIY9UYrSduw==
To: 57540 <at> debbugs.gnu.org
Subject: [RFC PATCH v2 17/19] gnu: Add python-pluggy-1.0.*
 gnu/packages/python-xyz.scm (python-pluggy-1.0): New variable.
Date: Wed, 07 Sep 2022 14:34:44 -0400
Message-ID: <875yhzvxrv.fsf@HIDDEN>
Mime-Version: 1.0
Content-Type: text/plain
X-Spam-Score: -0.0 (/)
X-Debbugs-Envelope-To: 57540
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/python-xyz.scm (python-pluggy-1.0): New variable.
---
 gnu/packages/python-xyz.scm | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/gnu/packages/python-xyz.scm b/gnu/packages/python-xyz.scm
index 1651f00054..7febf50286 100644
--- a/gnu/packages/python-xyz.scm
+++ b/gnu/packages/python-xyz.scm
@@ -14585,6 +14585,26 @@ (define-public python-pluggy
    (home-page "https://pypi.org/project/pluggy/")
    (license license:expat)))
 
+(define-public python-pluggy-1.0
+  (package
+    (inherit python-pluggy)
+    (name "python-pluggy")
+    (version "1.0.0")
+    (source (origin
+              ;; Won't build from github tarballs, throws error:
+              ;; "LookupError: setuptools-scm was unable to detect
+              ;; version for
+              ;; '/tmp/guix-build-python-pluggy-1.0-1.0.0.drv-0/source'."
+              ;;
+              ;; The PyPi version does not throw this error.
+              (method url-fetch)
+              (uri (pypi-uri "pluggy" version))
+              (sha256
+               (base32
+                "0n8iadlas2z1b4h0fc73b043c7iwfvx9rgvqm1azjmffmhxkf922"))))
+    (inputs (list python python-pypa-build python-wheel))
+    (native-inputs (list python-pytest python-setuptools-scm))))
+
 (define-public python-plumbum
   (package
     (name "python-plumbum")
-- 
2.37.2






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

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


Received: (at 57540) by debbugs.gnu.org; 7 Sep 2022 18:34:48 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Wed Sep 07 14:34:48 2022
Received: from localhost ([127.0.0.1]:56255 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1oVzst-00081j-Kj
	for submit <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:34:47 -0400
Received: from knopi.disroot.org ([178.21.23.139]:56432)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <garekdyszel@HIDDEN>) id 1oVzss-00081c-2I
 for 57540 <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:34:46 -0400
Received: from localhost (localhost [127.0.0.1])
 by disroot.org (Postfix) with ESMTP id 906DB49FDD
 for <57540 <at> debbugs.gnu.org>; Wed,  7 Sep 2022 20:34:45 +0200 (CEST)
X-Virus-Scanned: SPAM Filter at disroot.org
Received: from knopi.disroot.org ([127.0.0.1])
 by localhost (disroot.org [127.0.0.1]) (amavisd-new, port 10024)
 with UTF8SMTP id v3yQ8zMFCLk4 for <57540 <at> debbugs.gnu.org>;
 Wed,  7 Sep 2022 20:34:44 +0200 (CEST)
From: Garek Dyszel <garekdyszel@HIDDEN>
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=disroot.org; s=mail;
 t=1662575682; bh=qmcPxoBO+OBS1rmPFD2kj+zFqmaRZA0AcMWdywJSAuM=;
 h=From:To:Subject:Date;
 b=iJvI4ZTMI5W670bGgY/vSo/QouCx/QonkP1jgsE4/jbTiVPA6TfxKEDb5gi3lZ6Hs
 KJn0vjwk2Uar9ZeSNIPhGiOFK/UxoRk6X+R+gf+6v10FCgn7v0souGlrKyfZ62O21R
 Fm+Jh6PrbL40U86kF62DBRfj3eUCHNFye09J0cRN3J8CRhH7UCJQczeVtNJPSsxbf2
 xb8cOPuisSxeFmBXaBjDMNNwLA58YzKmWmQJAJrzfAirHniZx3NR6R9ONQW94OGI4/
 uIZBkVfwF+nalaxRIrRcfPa/iMdAujpHSOV1xCmp+TzE9GlaGmprdOqxHGJeNlHMEF
 H4BWp6j6FrmXA==
To: 57540 <at> debbugs.gnu.org
Subject: [RFC PATCH v2 16/19] gnu: Add python-editables.*
 gnu/packages/python-build.scm (python-editables): New variable.
Date: Wed, 07 Sep 2022 14:34:39 -0400
Message-ID: <877d2fvxs0.fsf@HIDDEN>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: quoted-printable
X-Spam-Score: -0.0 (/)
X-Debbugs-Envelope-To: 57540
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/python-build.scm (python-editables): New variable.
---
 gnu/packages/python-build.scm | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/gnu/packages/python-build.scm b/gnu/packages/python-build.scm
index e7023aca0c..d7f93543f4 100644
--- a/gnu/packages/python-build.scm
+++ b/gnu/packages/python-build.scm
@@ -7,6 +7,7 @@
 ;;; Copyright =C2=A9 2018, 2021, 2022 Maxim Cournoyer <maxim.cournoyer@gma=
il.com>
 ;;; Copyright =C2=A9 2021 Tobias Geerinckx-Rice <me@HIDDEN>
 ;;; Copyright =C2=A9 2021, 2022 Ricardo Wurmus <rekado@HIDDEN>
+;;; Copyright =C2=A9 2022 Garek Dyszel <garekdyszel@HIDDEN>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -474,3 +475,22 @@ (define-public python-setuptools-scm
 @dfn{software configuration management} (SCM) metadata instead of declaring
 them as the version argument or in a SCM managed file.")
     (license license:expat)))
+
+(define-public python-editables
+  (package
+    (name "python-editables")
+    (version "0.3")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://github.com/pfmoore/editables")
+                    (commit version)))
+              (file-name (git-file-name name version))
+              (sha256
+               (base32
+                "1gbfkgzmrmbd4ycshm09fr2wd4f1n9gq7s567jgkavhfkn7s2pn1"))))
+    (build-system python-build-system)
+    (home-page "https://github.com/pfmoore/editables")
+    (synopsis "Editable installations")
+    (description "Editable installations")
+    (license license:expat)))
--=20
2.37.2






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

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


Received: (at 57540) by debbugs.gnu.org; 7 Sep 2022 18:34:44 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Wed Sep 07 14:34:44 2022
Received: from localhost ([127.0.0.1]:56252 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1oVzsq-00081S-8d
	for submit <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:34:44 -0400
Received: from knopi.disroot.org ([178.21.23.139]:55938)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <garekdyszel@HIDDEN>) id 1oVzsn-00081K-P2
 for 57540 <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:34:42 -0400
Received: from localhost (localhost [127.0.0.1])
 by disroot.org (Postfix) with ESMTP id 365C240143
 for <57540 <at> debbugs.gnu.org>; Wed,  7 Sep 2022 20:34:41 +0200 (CEST)
X-Virus-Scanned: SPAM Filter at disroot.org
Received: from knopi.disroot.org ([127.0.0.1])
 by localhost (disroot.org [127.0.0.1]) (amavisd-new, port 10024)
 with ESMTP id N4j_vLrocnqI for <57540 <at> debbugs.gnu.org>;
 Wed,  7 Sep 2022 20:34:40 +0200 (CEST)
From: Garek Dyszel <garekdyszel@HIDDEN>
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=disroot.org; s=mail;
 t=1662575677; bh=lacvLdrihcFOXthMNaYMMylINg+0ZqM+R9qlLgnnYbE=;
 h=From:To:Subject:Date;
 b=AmEsDtEavI1UWaRYmU8NBe7hpHsxky0sCRbCdpOVo8CtEAvzYkiX8Eci+pFt8XSHz
 N2+Lv8bEhamlHHlFSQ0SlRFp1bf5vZvPAxlGM9281+eeXeSVp0V/Isa7GZJfxoy2Qs
 u2hsyICbXx8/oTcpzjHVhWZ51OOt4IDHjNhD8NQjw3odou0Av2vBJrK9WUV26/7oSK
 zKkN6J3Xmc7DdfHYylgIL7SHb2PsgqrjVu0zXlmSgEd1j0FL4dKEXH5M8xc36mdcr0
 +1C2mEXRjpdwOS7OJ8SNeqMWGFdKHS9LMRR/n1ELpr3+npanq8d4nN8CaW4IYH5uSg
 3Hfd63Jd8tBGw==
To: 57540 <at> debbugs.gnu.org
Subject: [RFC PATCH v2 15/19] gnu: Add python-pytest-icdiff.*
 gnu/packages/python-check.scm (python-pytest-icdiff): New variable.
Date: Wed, 07 Sep 2022 14:34:34 -0400
Message-ID: <878rmvvxs5.fsf@HIDDEN>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: quoted-printable
X-Spam-Score: -0.0 (/)
X-Debbugs-Envelope-To: 57540
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/python-check.scm (python-pytest-icdiff): New variable.
---
 gnu/packages/python-check.scm | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/gnu/packages/python-check.scm b/gnu/packages/python-check.scm
index 5ee1d41f34..6199b1e147 100644
--- a/gnu/packages/python-check.scm
+++ b/gnu/packages/python-check.scm
@@ -16,6 +16,7 @@
 ;;; Copyright =C2=A9 2022 Malte Frank Gerdes <malte.f.gerdes@HIDDEN>
 ;;; Copyright =C2=A9 2022 Felix Gruber <felgru@HIDDEN>
 ;;; Copyright =C2=A9 2022 Tomasz Jeneralczyk <tj@HIDDEN>
+;;; Copyright =C2=A9 2022 Garek Dyszel <garekdyszel@HIDDEN>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -2468,3 +2469,24 @@ (define-public python-xvfbwrapper
 physical display.  Only a network layer is necessary.  Xvfb is useful for
 running acceptance tests on headless servers.")
     (license license:expat)))
+
+(define-public python-pytest-icdiff
+  (package
+    (name "python-pytest-icdiff")
+    (version "0.6")
+    (source (origin
+              ;; Tests fail in git version, but not in the PyPi version.
+              ;; The PyPi version is also more up-to-date.
+              (method url-fetch)
+              (uri (pypi-uri "pytest-icdiff" version))
+              (sha256
+               (base32
+                "1b8vzn2hvv6x25w1s446q1rfsbdik617lzpal3qb94x8a12yzwg8"))))
+    (build-system python-build-system)
+    (propagated-inputs (list python python-pypa-build python-icdiff
+                             python-pprintpp))
+    (native-inputs (list python-pytest))
+    (home-page "https://github.com/hjwp/pytest-icdiff")
+    (synopsis "Use icdiff for better error messages in pytest assertions")
+    (description "Use icdiff for better error messages in pytest assertion=
s.")
+    (license (license:non-copyleft "LICENSE"))))
--=20
2.37.2






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

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


Received: (at 57540) by debbugs.gnu.org; 7 Sep 2022 18:34:41 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Wed Sep 07 14:34:41 2022
Received: from localhost ([127.0.0.1]:56249 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1oVzsm-00081C-VI
	for submit <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:34:41 -0400
Received: from knopi.disroot.org ([178.21.23.139]:55618)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <garekdyszel@HIDDEN>) id 1oVzsk-000814-Vi
 for 57540 <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:34:39 -0400
Received: from localhost (localhost [127.0.0.1])
 by disroot.org (Postfix) with ESMTP id 6809440123
 for <57540 <at> debbugs.gnu.org>; Wed,  7 Sep 2022 20:34:38 +0200 (CEST)
X-Virus-Scanned: SPAM Filter at disroot.org
Received: from knopi.disroot.org ([127.0.0.1])
 by localhost (disroot.org [127.0.0.1]) (amavisd-new, port 10024)
 with ESMTP id UL4nB2Od0dom for <57540 <at> debbugs.gnu.org>;
 Wed,  7 Sep 2022 20:34:37 +0200 (CEST)
From: Garek Dyszel <garekdyszel@HIDDEN>
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=disroot.org; s=mail;
 t=1662575672; bh=sdklI/rCJ+MG5pSUKtXHb0EpdH75q9qT9fwiv25+zpA=;
 h=From:To:Subject:Date;
 b=MWeM8JUC2CjUkG2UdHvoQAAbzxn77afu/7aaugYMg1JnE2GYbQ426H7ctx2IoedrM
 Y7TO6libCQl6zo6b/GDAk4OM96bpJWiddUhg9RpW2TJj/Sd9VHDEToworCip6uL6rg
 jwl8FLVM1+RslleCaE47SbH81lqcJQ7WPFdqeSeHJn4vqMD8ykp5idp57Z6n+MiDK9
 yX9wNZeGtWKutfruVoWdeMLf2O85YWX55h9V0y6tnp78MYBcdGxI2WseFz9xVrpzIW
 EOKUSDestjGAMHW8sptZgI4ZXuXIjdvNUeallOwt+6ubGyZj0Q2pTQMh4ZlYt+EJFc
 kHIqk2HhRjNog==
To: 57540 <at> debbugs.gnu.org
Subject: [RFC PATCH v2 14/19] gnu: Add python-icdiff.*
 gnu/packages/python-xyz.scm (python-icdiff): New variable.
Date: Wed, 07 Sep 2022 14:34:29 -0400
Message-ID: <87a67bvxsa.fsf@HIDDEN>
Mime-Version: 1.0
Content-Type: text/plain
X-Spam-Score: -0.0 (/)
X-Debbugs-Envelope-To: 57540
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/python-xyz.scm (python-icdiff): New variable.
---
 gnu/packages/python-xyz.scm | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/gnu/packages/python-xyz.scm b/gnu/packages/python-xyz.scm
index 90bf269341..1651f00054 100644
--- a/gnu/packages/python-xyz.scm
+++ b/gnu/packages/python-xyz.scm
@@ -31021,3 +31021,23 @@ (define-public python-pprintpp
       (description
        "This package provides a drop-in replacement for pprint that's actually pretty.")
       (license license:bsd-3))))
+
+(define-public python-icdiff
+  (package
+    (name "python-icdiff")
+    (version "2.0.5")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://github.com/jeffkaufman/icdiff")
+                    (commit (string-append "release-" version))))
+              (file-name (git-file-name name version))
+              (sha256
+               (base32
+                "14gr9j2h7sfw47pwfzspm4zinywhqmzm4a0qz5c2k9wbixz120a4"))))
+    (build-system python-build-system)
+    (home-page "https://www.jefftk.com/icdiff")
+    (synopsis "Improved colored diff")
+    (description "Improved colored diff.")
+    ;; Python Software Foundation License version 2
+    (license license:psfl)))
-- 
2.37.2






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

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


Received: (at 57540) by debbugs.gnu.org; 7 Sep 2022 18:34:31 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Wed Sep 07 14:34:30 2022
Received: from localhost ([127.0.0.1]:56246 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1oVzsc-00080p-JV
	for submit <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:34:30 -0400
Received: from knopi.disroot.org ([178.21.23.139]:53662)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <garekdyszel@HIDDEN>) id 1oVzsa-00080h-LO
 for 57540 <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:34:29 -0400
Received: from localhost (localhost [127.0.0.1])
 by disroot.org (Postfix) with ESMTP id 17DB749FB4
 for <57540 <at> debbugs.gnu.org>; Wed,  7 Sep 2022 20:34:28 +0200 (CEST)
X-Virus-Scanned: SPAM Filter at disroot.org
Received: from knopi.disroot.org ([127.0.0.1])
 by localhost (disroot.org [127.0.0.1]) (amavisd-new, port 10024)
 with ESMTP id CR8qYAAhDT21 for <57540 <at> debbugs.gnu.org>;
 Wed,  7 Sep 2022 20:34:26 +0200 (CEST)
From: Garek Dyszel <garekdyszel@HIDDEN>
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=disroot.org; s=mail;
 t=1662575662; bh=HprV3rasm0f+1iGUNKmDbme0tqHirvVG4rrHmDH3HIc=;
 h=From:To:Subject:Date;
 b=GVfmnt7IPjUgihJupcraPBRIt52gqMau+AO7wIYRC9502h1hXPIbMM3m0jVqJliDo
 NoKmyjxrOXrUhExBTygP2SOZg48cflBzH9F3aP7Ge4TaMnguKKX5jgAzb7HOTtLgcZ
 PrpctSc4dsfoz89HZ4iOo4xYVw2xCQ/I2gw+UQ7usEUvE3hGDwZ6wMAj6JqSCFf369
 +jW/OGbCoM74Z53VCdVGzIpJYBP9ijQDq0rIT63r957jxeEfWTSydIwrM+26N0zsYk
 jmpSmBlrGnpblNvv/5EnkziBeJ85W+ee8FlsIGwXGlpYKyF41RMrmLP/HSs8HK4ODN
 zhNFHtDPoQBTg==
To: 57540 <at> debbugs.gnu.org
Subject: [RFC PATCH v2 13/19] gnu: Add python-pprintpp.*
 gnu/packages/python-xyz.scm (python-pprintpp): New variable.
Date: Wed, 07 Sep 2022 14:34:19 -0400
Message-ID: <87bkrrvxsk.fsf@HIDDEN>
Mime-Version: 1.0
Content-Type: text/plain
X-Spam-Score: -0.0 (/)
X-Debbugs-Envelope-To: 57540
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/python-xyz.scm (python-pprintpp): New variable.
---
 gnu/packages/python-xyz.scm | 58 +++++++++++++++++++++++++++++++++++++
 1 file changed, 58 insertions(+)

diff --git a/gnu/packages/python-xyz.scm b/gnu/packages/python-xyz.scm
index 2c358b8c58..90bf269341 100644
--- a/gnu/packages/python-xyz.scm
+++ b/gnu/packages/python-xyz.scm
@@ -30963,3 +30963,61 @@ (define-public python-hatch-fancy-pypi-readme
     (description "Fancy PyPI READMEs with Hatch")
     ;; MIT License
     (license license:expat)))
+
+(define-public python-pprintpp
+  ;; Git version tags are inaccurate for this package, too; use the
+  ;; bare commit.
+  (let ((commit "7ede6da1f3062bbfb32ee04353d675a5bff185e0")
+        (revision "1"))
+    (package
+      (name "python-pprintpp")
+      (version (git-version "0.3.0" revision commit))
+      (source (origin
+                (method git-fetch)
+                (uri (git-reference
+                      (url "https://github.com/wolever/pprintpp")
+                      (commit commit)))
+                (file-name (git-file-name name version))
+                (sha256
+                 (base32
+                  "0nk935m3ig8sc32laqbh698vwpk037yw27gd3nvwwzdv42jal2li"))))
+      (inputs (list python python-pypa-build python-hypothesis python-wheel
+                    python-parameterized))
+      (native-inputs (list python-pytest python-nose))
+      (build-system python-build-system)
+      (arguments
+       ;; Copied directly from the build process for
+       ;; python-jsonschema-next.
+       (substitute-keyword-arguments (package-arguments python-jsonschema)
+         ((#:phases phases)
+          #~(modify-phases #$phases
+              (replace 'build
+                (lambda _
+                  (setenv "SOURCE_DATE_EPOCH" "315532800")
+                  (invoke "python"
+                          "-m"
+                          "build"
+                          "--wheel"
+                          "--no-isolation"
+                          ".")))
+              (replace 'install
+                (lambda* (#:key outputs #:allow-other-keys)
+                  (let ((whl (car (find-files "dist" "\\.whl$"))))
+                    (invoke "pip"
+                            "--no-cache-dir"
+                            "--no-input"
+                            "install"
+                            "--no-deps"
+                            "--prefix"
+                            #$output
+                            whl))))
+              (replace 'check
+                (lambda* (#:key tests? #:allow-other-keys)
+                  (when tests?
+                    (invoke "python" "test.py"))))))))
+
+      (home-page "https://github.com/wolever/pprintpp")
+      (synopsis "Drop-in replacement for pprint that's actually pretty")
+      (description
+       "This package provides a drop-in replacement for pprint that's actually pretty.")
+      (license license:bsd-3))))
-- 
2.37.2






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

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


Received: (at 57540) by debbugs.gnu.org; 7 Sep 2022 18:34:20 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Wed Sep 07 14:34:20 2022
Received: from localhost ([127.0.0.1]:56243 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1oVzsS-00080S-41
	for submit <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:34:20 -0400
Received: from knopi.disroot.org ([178.21.23.139]:52044)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <garekdyszel@HIDDEN>) id 1oVzsQ-00080J-Kb
 for 57540 <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:34:19 -0400
Received: from localhost (localhost [127.0.0.1])
 by disroot.org (Postfix) with ESMTP id 13D3949FCF
 for <57540 <at> debbugs.gnu.org>; Wed,  7 Sep 2022 20:34:18 +0200 (CEST)
X-Virus-Scanned: SPAM Filter at disroot.org
Received: from knopi.disroot.org ([127.0.0.1])
 by localhost (disroot.org [127.0.0.1]) (amavisd-new, port 10024)
 with ESMTP id 2e0g15u2BZg0 for <57540 <at> debbugs.gnu.org>;
 Wed,  7 Sep 2022 20:34:16 +0200 (CEST)
From: Garek Dyszel <garekdyszel@HIDDEN>
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=disroot.org; s=mail;
 t=1662575656; bh=GDJ8A0HgDX8SVDTjn/Y4ZhFYTfapRbQqFcb9Q8phFT0=;
 h=From:To:Subject:Date;
 b=UTlXnzpqlqv2p06gRYl0nba1+c3hQsfnWBMBzmlcU4x1Jlp6Ad0C84sF2O6+vreB2
 7JgQvLj/UJnVCEl0KJG9kJdJKTxSy7tsTD+l6cKdQWqre9+zQzJfei2sOzZl9h48zW
 HNDM5ANGqJBiVB8/mJsCG7rOdsfihGplQdsTuoOrsX+BsIS670stc/wvQdaKqlkj1V
 3i1lYYNgrJXLoNY7R8pOa6vavCk54cTrZ1p57NsCoem1kNUTpGQBG6dy5uU+OUv/3V
 3r1vaGQoDkOzTbQcsF5HflD/o+FtGtWJKLNHJwhlH3L5mqUqKHv5yvPCUbRF4Gibim
 z40BoEsnSD4sg==
To: 57540 <at> debbugs.gnu.org
Subject: [RFC PATCH v2 12/19] gnu: Add python-hatch-fancy-pypi-readme.*
 gnu/packages/python-xyz.scm (python-hatch-fancy-pypi-readme): New
 variable.
Date: Wed, 07 Sep 2022 14:34:13 -0400
Message-ID: <87czc7vxsq.fsf@HIDDEN>
Mime-Version: 1.0
Content-Type: text/plain
X-Spam-Score: -0.0 (/)
X-Debbugs-Envelope-To: 57540
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/python-xyz.scm (python-hatch-fancy-pypi-readme): New variable.
---
 gnu/packages/python-xyz.scm | 66 +++++++++++++++++++++++++++++++++++++
 1 file changed, 66 insertions(+)

diff --git a/gnu/packages/python-xyz.scm b/gnu/packages/python-xyz.scm
index b5b319cfde..2c358b8c58 100644
--- a/gnu/packages/python-xyz.scm
+++ b/gnu/packages/python-xyz.scm
@@ -30897,3 +30897,69 @@ (define-public python-hatch-vcs
       (description "Hatch plugin for versioning with your preferred VCS")
       ;; MIT License
       (license license:expat))))
+
+(define-public python-hatch-fancy-pypi-readme
+  (package
+    (name "python-hatch-fancy-pypi-readme")
+    (version "22.3.0")
+    (source (origin
+              (method url-fetch)
+              (uri (pypi-uri "hatch_fancy_pypi_readme" version))
+              (sha256
+               (base32
+                "1ykfz1sbz58xbjw5k9xpmn5r6ji16w8vag47j8f969bqy3w52ikx"))))
+    (build-system python-build-system)
+    (propagated-inputs (list python-hatchling python-tomli
+                             python-typing-extensions))
+    (native-inputs (list python
+                         python-pypa-build
+                         python-pathspec
+                         python-pluggy-1.0
+                         python-editables
+                         python-hatchling
+                         python-wheel
+                         python-pytest
+                         python-pytest-icdiff))
+    (arguments
+     `(#:phases (modify-phases %standard-phases
+                  (add-before 'build 'disable-broken-tests
+                    (lambda _
+                      ;; Skip the tests for "building". Guix already does this,
+                      ;; so we don't need to test it for any Guix package.
+                      (chdir "tests")
+                      (invoke "sed" "-i"
+                       "11ipytest.skip('No need to test building,                        guix does this already', allow_module_level=True)"
+                       "test_end_to_end.py")
+                      (chdir "../")))
+                  ;; XXX: PEP 517 manual build/install procedures copied from
+                  ;; python-isort.
+                  (replace 'build
+                    (lambda _
+                      ;; ZIP does not support timestamps before 1980.
+                      (setenv "SOURCE_DATE_EPOCH" "315532800")
+                      (invoke "python"
+                              "-m"
+                              "build"
+                              "--wheel"
+                              "--no-isolation"
+                              ".")))
+                  (replace 'install
+                    (lambda* (#:key outputs #:allow-other-keys)
+                      (let ((whl (car (find-files "dist" "\\.whl$"))))
+                        (invoke "pip"
+                                "--no-cache-dir"
+                                "--no-input"
+                                "install"
+                                "--no-deps"
+                                "--prefix"
+                                (assoc-ref %outputs "out")
+                                whl))))
+                  (replace 'check
+                    (lambda* (#:key tests? #:allow-other-keys)
+                      (when tests?
+                        (invoke "pytest" "-vv")))))))
+    (home-page "https://github.com/hynek/hatch-fancy-pypi-readme")
+    (synopsis "Fancy PyPI READMEs with Hatch")
+    (description "Fancy PyPI READMEs with Hatch")
+    ;; MIT License
+    (license license:expat)))
-- 
2.37.2






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

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


Received: (at 57540) by debbugs.gnu.org; 7 Sep 2022 18:34:17 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Wed Sep 07 14:34:17 2022
Received: from localhost ([127.0.0.1]:56240 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1oVzsO-00080B-PC
	for submit <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:34:17 -0400
Received: from knopi.disroot.org ([178.21.23.139]:51288)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <garekdyszel@HIDDEN>) id 1oVzsM-000802-F6
 for 57540 <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:34:14 -0400
Received: from localhost (localhost [127.0.0.1])
 by disroot.org (Postfix) with ESMTP id F170749FB1
 for <57540 <at> debbugs.gnu.org>; Wed,  7 Sep 2022 20:34:13 +0200 (CEST)
X-Virus-Scanned: SPAM Filter at disroot.org
Received: from knopi.disroot.org ([127.0.0.1])
 by localhost (disroot.org [127.0.0.1]) (amavisd-new, port 10024)
 with ESMTP id dhT_3oWiKtoc for <57540 <at> debbugs.gnu.org>;
 Wed,  7 Sep 2022 20:34:12 +0200 (CEST)
From: Garek Dyszel <garekdyszel@HIDDEN>
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=disroot.org; s=mail;
 t=1662575651; bh=7mH9haXQTE1A2E0nljjfrT8XE4r5qbehk0N38qG1914=;
 h=From:To:Subject:Date;
 b=bq9J7iKI9Si39+pujnTIyoPlWWF6mhNRdeHqNBhobkvyUce4QPNf2vhRnODcy13ov
 R9udAPw0kkd+IFmbuFLLvYlYjFZGTNP19JU3xdixqdsHuIsns/UgdoH1rttAzL/KWm
 z2TuibMEDBnjxLRCGZ8p7IZujM96ZOed41n76pMmoUBRXO2b1HSh7VQNoYoj3RwoUG
 qO2V1xAC5Y2hPNMTTrWAn/vcmtKk/lLrbebh4wSD3bTGia0Nw9gzVoVPaJ6uEfykCs
 Fod8yn40Rm2B9sLzDUE+g6zy6tf0/4sF4C5VCCmLYtZn3Q0h8Btv9mY6lHLBiHitRW
 dzrHn1x3mZbOQ==
To: 57540 <at> debbugs.gnu.org
Subject: [RFC PATCH v2 11/19] gnu: Add python-hatch-vcs.*
 gnu/packages/python-xyz.scm (python-hatch-vcs): New variable.
Date: Wed, 07 Sep 2022 14:34:08 -0400
Message-ID: <87edwnvxsv.fsf@HIDDEN>
Mime-Version: 1.0
Content-Type: text/plain
X-Spam-Score: -0.0 (/)
X-Debbugs-Envelope-To: 57540
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/python-xyz.scm (python-hatch-vcs): New variable.
---
 gnu/packages/python-xyz.scm | 62 +++++++++++++++++++++++++++++++++++++
 1 file changed, 62 insertions(+)

diff --git a/gnu/packages/python-xyz.scm b/gnu/packages/python-xyz.scm
index 8dd8d902a5..b5b319cfde 100644
--- a/gnu/packages/python-xyz.scm
+++ b/gnu/packages/python-xyz.scm
@@ -30835,3 +30835,65 @@ (define-public python-hatchling
     (description "Modern, extensible Python project management")
     ;; MIT License
     (license license:expat)))
+
+(define-public python-hatch-vcs
+  ;; Tags are not accurate; just use the commit itself.
+  (let ((commit "367daedb23ba906f3e0714c64392fdd6ffa69ab2")
+        (revision "1"))
+    (package
+      (name "python-hatch-vcs")
+      (version (git-version "0.2.0" revision commit))
+      (source (origin
+                (method git-fetch)
+                (uri (git-reference
+                      (url "https://github.com/ofek/hatch-vcs")
+                      (commit commit)))
+                (file-name (git-file-name name version))
+                (sha256
+                 (base32
+                  "0nlnv32jqiz8ikc013h5simmiqqg0qa7pm0qcbd8yiqq1p43iw05"))))
+      (build-system python-build-system)
+      (inputs (list python
+                    python-pypa-build
+                    python-pathspec
+                    python-pluggy-1.0
+                    python-editables
+                    git))
+      ;; python-setuptools-scm-6.4 minimum
+      (propagated-inputs (list python-hatchling))
+      (native-inputs (list python-pytest python-setuptools-scm-7))
+      (arguments
+       ;; Copied directly from the build process for
+       ;; python-jsonschema-next.
+       (substitute-keyword-arguments (package-arguments python-jsonschema)
+         ((#:phases phases)
+          #~(modify-phases #$phases
+              (replace 'build
+                (lambda _
+                  (setenv "SOURCE_DATE_EPOCH" "315532800")
+                  (invoke "python"
+                          "-m"
+                          "build"
+                          "--wheel"
+                          "--no-isolation"
+                          ".")))
+              (replace 'install
+                (lambda* (#:key outputs #:allow-other-keys)
+                  (let ((whl (car (find-files "dist" "\\.whl$"))))
+                    (invoke "pip"
+                            "--no-cache-dir"
+                            "--no-input"
+                            "install"
+                            "--no-deps"
+                            "--prefix"
+                            #$output
+                            whl))))
+              (replace 'check
+                (lambda* (#:key tests? #:allow-other-keys)
+                  (when tests?
+                    (invoke "pytest" "-vvv"))))))))
+      (home-page "https://ofek.dev/projects/hatch/")
+      (synopsis "Hatch plugin for versioning with your preferred VCS")
+      (description "Hatch plugin for versioning with your preferred VCS")
+      ;; MIT License
+      (license license:expat))))
-- 
2.37.2






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

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


Received: (at 57540) by debbugs.gnu.org; 7 Sep 2022 18:34:07 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Wed Sep 07 14:34:07 2022
Received: from localhost ([127.0.0.1]:56237 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1oVzsF-0007zo-CC
	for submit <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:34:07 -0400
Received: from knopi.disroot.org ([178.21.23.139]:49864)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <garekdyszel@HIDDEN>) id 1oVzsE-0007zh-54
 for 57540 <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:34:06 -0400
Received: from localhost (localhost [127.0.0.1])
 by disroot.org (Postfix) with ESMTP id 927E040143
 for <57540 <at> debbugs.gnu.org>; Wed,  7 Sep 2022 20:34:05 +0200 (CEST)
X-Virus-Scanned: SPAM Filter at disroot.org
Received: from knopi.disroot.org ([127.0.0.1])
 by localhost (disroot.org [127.0.0.1]) (amavisd-new, port 10024)
 with ESMTP id QTWkB2VGviY2 for <57540 <at> debbugs.gnu.org>;
 Wed,  7 Sep 2022 20:34:04 +0200 (CEST)
From: Garek Dyszel <garekdyszel@HIDDEN>
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=disroot.org; s=mail;
 t=1662575644; bh=Evy0AxQhHJgf8kXgl2AsfFAJqWrr0lQA/T+KV2AbKZg=;
 h=From:To:Subject:Date;
 b=cyMCzjBdK/kOhvfbcPlG1495swQoGSBj7VXabZrQ8NDqBuCY3ECv4/p98JG+tBIkV
 wygfZGgt1/3LQhG4KJ/3xqZeXKIdzn1Y99DhDYI1KBbhu2ycdgXa0g3vIymkIGsILQ
 vS0rTnS91mOVmqyPQOXz09y81iKI1r5j6Ojdrp0ykTCVDWJWFLDUYf8+jWT3XN3Xum
 ZSHCQPDIw061oa2wwxU7DQ5Zwu7HTPsTVcL3z7+Imzx+ljKQiISJT8HPC28IzgNAzJ
 ZaMcVOLVLITzLOU0iamgR3eKf9i1SbaADQzc/5ioMuVTsfmv9CBBV0riBm9moYRZk/
 daO9+dj3r5Wbw==
To: 57540 <at> debbugs.gnu.org
Subject: [RFC PATCH v2 10/19] gnu: Add python-hatchling.*
 gnu/packages/python-xyz.scm (python-hatchling): New variable.
Date: Wed, 07 Sep 2022 14:34:01 -0400
Message-ID: <87fsh3vxt2.fsf@HIDDEN>
Mime-Version: 1.0
Content-Type: text/plain
X-Spam-Score: -0.0 (/)
X-Debbugs-Envelope-To: 57540
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/python-xyz.scm (python-hatchling): New variable.
---
 gnu/packages/python-xyz.scm | 64 +++++++++++++++++++++++++++++++++++++
 1 file changed, 64 insertions(+)

diff --git a/gnu/packages/python-xyz.scm b/gnu/packages/python-xyz.scm
index cc5b85c3a1..8dd8d902a5 100644
--- a/gnu/packages/python-xyz.scm
+++ b/gnu/packages/python-xyz.scm
@@ -30771,3 +30771,67 @@ (define-public python-version
        "This package provides a simple utility for checking the python version.")
       ;; MIT License
       (license license:expat))))
+
+(define-public python-hatchling
+  (package
+    (name "python-hatchling")
+    (version "1.8.1")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://github.com/pypa/hatch")
+                    (commit (string-append "hatchling-v" version))))
+              (file-name (git-file-name name version))
+              (sha256
+               (base32
+                "1q25kqw71g8mjwfjz9ph0iigdqa26zzxgmqm0v0bp0z1j8rcl237"))))
+    ;; python-pypa-build needed for bootstrapping.
+    ;; Otherwise we get a circular reference:
+    ;; python-hatchling trying to build itself, without
+    ;; first having hatchling installed.
+    (inputs (list python
+                  python-pypa-build
+                  python-editables
+                  python-importlib-metadata
+                  python-version
+                  python-packaging-next
+                  python-pathspec
+                  python-pluggy-1.0 ; TODO: Not detected by pytest?
+                  python-tomli
+                  python-platformdirs))
+    (build-system python-build-system)
+    (arguments
+     `(#:phases (modify-phases %standard-phases
+                  ;; Copied directly from the build process for
+                  ;; python-jsonschema-next.
+                  (replace 'build
+                    (lambda _
+                      (chdir "backend")
+                      ;; ZIP does not support timestamps before 1980.
+                      (setenv "SOURCE_DATE_EPOCH" "315532800")
+                      (invoke "python"
+                              "-m"
+                              "build"
+                              "--wheel"
+                              "--no-isolation"
+                              ".")))
+                  (replace 'install
+                    (lambda* (#:key outputs #:allow-other-keys)
+                      (let ((whl (car (find-files "dist" "\\.whl$"))))
+                        (invoke "pip"
+                                "--no-cache-dir"
+                                "--no-input"
+                                "install"
+                                "--no-deps"
+                                "--prefix"
+                                (assoc-ref %outputs "out")
+                                whl))))
+                  (replace 'check
+                    (lambda* (#:key tests? #:allow-other-keys)
+                      (when tests?
+                        (invoke "pytest" "-vv")))))))
+    (home-page "https://ofek.dev/projects/hatch/")
+    (synopsis "Modern, extensible Python project management")
+    (description "Modern, extensible Python project management")
+    ;; MIT License
+    (license license:expat)))
-- 
2.37.2






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

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


Received: (at 57540) by debbugs.gnu.org; 7 Sep 2022 18:34:03 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Wed Sep 07 14:34:03 2022
Received: from localhost ([127.0.0.1]:56228 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1oVzsA-0007yg-To
	for submit <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:34:03 -0400
Received: from knopi.disroot.org ([178.21.23.139]:48850)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <garekdyszel@HIDDEN>) id 1oVzs9-0007yD-2T
 for 57540 <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:34:01 -0400
Received: from localhost (localhost [127.0.0.1])
 by disroot.org (Postfix) with ESMTP id 6BD0349FB4
 for <57540 <at> debbugs.gnu.org>; Wed,  7 Sep 2022 20:34:00 +0200 (CEST)
X-Virus-Scanned: SPAM Filter at disroot.org
Received: from knopi.disroot.org ([127.0.0.1])
 by localhost (disroot.org [127.0.0.1]) (amavisd-new, port 10024)
 with ESMTP id jt_RDiw9C1QE for <57540 <at> debbugs.gnu.org>;
 Wed,  7 Sep 2022 20:33:59 +0200 (CEST)
From: Garek Dyszel <garekdyszel@HIDDEN>
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=disroot.org; s=mail;
 t=1662575639; bh=pzaUAEihUq+vt9h8uT4b4A0W5/wyGE16DMIfROJK6Lk=;
 h=From:To:Subject:Date;
 b=fPuCdE6TMpyIV2HZrvDqUwXKlfwu5A4o8sbQbhgdhJ2IvgnAdNZyYyxajuHbhtrRc
 TYn9W/AHezOq8mjkVhBGQpvz6PkUyCnsibrrbg8RQMorYBRDswkT27Z1jYhWkvEYA0
 rsEnYJbUDjPo0HodgkuKQUXKF9rGUEzv/AGB+C0OcGgpsNSR7rfj2c4FGvM6t0A9Ib
 z3+RWyR8CZjtIzT4lMNaV/bnNW5R9lhXDc06mkOrzDgo/4KubIY+Sb/QRUXR98XgLU
 yVE8rGi1tyLgz/pxi9fWk8QhZxtVjFnWEGXSTbT2PeY0RHsojdPz9vcklrXjIiEIRh
 wI2ZpHaRxastw==
To: 57540 <at> debbugs.gnu.org
Subject: [RFC PATCH v2 09/19] gnu: Add python-version.*
 gnu/packages/python-xyz.scm (python-version): New variable.
Date: Wed, 07 Sep 2022 14:33:55 -0400
Message-ID: <87h71jvxt8.fsf@HIDDEN>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: quoted-printable
X-Spam-Score: -0.0 (/)
X-Debbugs-Envelope-To: 57540
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/python-xyz.scm (python-version): New variable.
---
 gnu/packages/python-xyz.scm | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

diff --git a/gnu/packages/python-xyz.scm b/gnu/packages/python-xyz.scm
index a73f07ece3..cc5b85c3a1 100644
--- a/gnu/packages/python-xyz.scm
+++ b/gnu/packages/python-xyz.scm
@@ -128,6 +128,7 @@
 ;;; Copyright =C2=A9 2022 Marek Fel=C5=A1=C3=B6ci <marek@HIDDEN>
 ;;; Copyright =C2=A9 2022 Hilton Chain <hako@HIDDEN>
 ;;; Copyright =C2=A9 2022 Tomasz Jeneralczyk <tj@HIDDEN>
+;;; Copyright =C2=A9 2022 Garek Dyszel <garekdyszel@HIDDEN>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -30746,3 +30747,27 @@ (define-public python-lief
      "@code{python-lief} is a cross platform library which can parse, modi=
fy
 and abstract ELF, PE and MachO formats.")
     (license license:asl2.0)))
+
+(define-public python-version
+  ;; No version tags available in the git repo; just using bare commit ins=
tead.
+  (let ((commit "5232eea250ab72cc5cb72b0b75efb35d2192b906")
+        (revision "1"))
+    (package
+      (name "python-python-version")
+      (version (git-version "0.0.2" revision commit))
+      (source (origin
+                (method git-fetch)
+                (uri (git-reference
+                      (url "https://gitlab.com/halfak/python_version")
+                      (commit commit)))
+                (file-name (git-file-name name version))
+                (sha256
+                 (base32
+                  "0w210559ypdynlj9yn40m9awzkaknwrf682i99hswl7h66sdgh0h"))=
))
+      (build-system python-build-system)
+      (home-page "https://gitlab.com/halfak/python_version")
+      (synopsis "Provides a simple utility for checking the python version=
")
+      (description
+       "This package provides a simple utility for checking the python ver=
sion.")
+      ;; MIT License
+      (license license:expat))))
--=20
2.37.2






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

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


Received: (at 57540) by debbugs.gnu.org; 7 Sep 2022 18:33:58 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Wed Sep 07 14:33:57 2022
Received: from localhost ([127.0.0.1]:56223 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1oVzs5-0007y3-9i
	for submit <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:33:57 -0400
Received: from knopi.disroot.org ([178.21.23.139]:48328)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <garekdyszel@HIDDEN>) id 1oVzs3-0007xv-TW
 for 57540 <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:33:56 -0400
Received: from localhost (localhost [127.0.0.1])
 by disroot.org (Postfix) with ESMTP id 4246140121
 for <57540 <at> debbugs.gnu.org>; Wed,  7 Sep 2022 20:33:55 +0200 (CEST)
X-Virus-Scanned: SPAM Filter at disroot.org
Received: from knopi.disroot.org ([127.0.0.1])
 by localhost (disroot.org [127.0.0.1]) (amavisd-new, port 10024)
 with ESMTP id fcLFxkWMD1VF for <57540 <at> debbugs.gnu.org>;
 Wed,  7 Sep 2022 20:33:53 +0200 (CEST)
From: Garek Dyszel <garekdyszel@HIDDEN>
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=disroot.org; s=mail;
 t=1662575633; bh=yGgZnp5IMdYK/UCQp/JZeOcggsUc6UUGx418O6fjyQ0=;
 h=From:To:Subject:Date;
 b=LfA/9D0i9KwTulektjQ4bXO2C5uP+jH0s4b7Jl6x5wy9knHMWTuzaVDdmZxpiqquq
 oySS4Wd7DGKSQnw9rvR9R4hltWwHX8zfkR+pLr8QMup8ngCh7r0jasd1jy+OwID2j2
 TtZhFZQnjZ03Fnx4JYabrtGKag+Csf/k2ICTk8U91H/BzOtL9Kst8tH8se0WDKyUQF
 G8jM3sAXmx4BvdzzxZAAnl1fOb/iqK3FI3jOWH1wAfPRV2qC1jCxpfTvj9+ypeu57o
 PkIDzpRA5onmbXe4s+45TxVDAYkE2Hb2DHnI4LHNxrRm9yegoTNhtCPgjeia+w5QqD
 iLlXhdScXC52Q==
To: 57540 <at> debbugs.gnu.org
Subject: [RFC PATCH v2 08/19] gnu: Add coq-mathcomp-analysis.*
 gnu/packages/coq.scm (coq-mathcomp-analysis): New variable.
Date: Wed, 07 Sep 2022 14:33:50 -0400
Message-ID: <87illzvxtd.fsf@HIDDEN>
Mime-Version: 1.0
Content-Type: text/plain
X-Spam-Score: -0.0 (/)
X-Debbugs-Envelope-To: 57540
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-mathcomp-analysis): New variable.
---
 gnu/packages/coq.scm | 66 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 66 insertions(+)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 78ef5473fd..036134b8ff 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -923,3 +923,69 @@ (define-public coq-mathcomp-bigenough
 near tactics.  The formalization is based on the Mathematical
 Components library.")
     (license license:cecill-b)))
+
+(define-public coq-mathcomp-analysis
+  (package
+    (name "coq-mathcomp-analysis")
+    (version "0.5.4")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://github.com/math-comp/analysis")
+                    (commit version)))
+              (file-name (git-file-name name version))
+              (sha256
+               (base32
+                "1l1yaxbmqr4li8x7g51q98a6v383dnf94lw1b74ccpwqz9qybz9m"))))
+    (build-system gnu-build-system)
+    (arguments
+     `( ;No rule to make target 'check'. Stop.
+       ;; Makefile.common has no references to tests.
+       ;; There are also no references to tests found after
+       ;; running the following commands in the top
+       ;; directory of the cloned repo:
+       ;; find -type d | grep -i test
+       ;; rg test # where rg is ripgrep
+       ;; Checking the git log, we find: "Add test suite for
+       ;; joins and several fixes".
+       ;;
+       ;; If tests are included, this quote suggests that they
+       ;; would be part of the source files themselves,
+       ;; and the tests would be run as part of the build
+       ;; process.
+       #:tests? #f
+       #:make-flags ,#~(list (string-append "COQBIN="
+                                            #$(this-package-input "coq-core")
+                                            "/bin/")
+                             (string-append "COQBININSTALL="
+                                            (assoc-ref %outputs "out") "/bin/")
+                             (string-append "DESTDIR="
+                                            (assoc-ref %outputs "out"))
+                             (string-append "COQMF_COQLIB="
+                                            (assoc-ref %outputs "out")
+                                            "/lib/ocaml/site-lib/coq")
+                             (string-append "COQLIBINSTALL="
+                                            (assoc-ref %outputs "out")
+                                            "/lib/coq/user-contrib"))
+       #:phases (modify-phases %standard-phases
+                  (delete 'configure)
+                  (replace 'build
+                    (lambda* (#:key make-flags #:allow-other-keys)
+                      (apply invoke "make" "build" make-flags))))))
+    (inputs (list coq
+                  coq-stdlib
+                  coq-mathcomp
+                  coq-mathcomp-finmap
+                  coq-mathcomp-hierarchy-builder
+                  coq-elpi
+                  coq-mathcomp-bigenough
+                  coq-core
+                  which
+                  python))
+    (synopsis "Real analysis for the Coq proof assistant")
+    (description
+     "This repository contains an experimental library for
+real analysis for the Coq proof-assistant, using the Mathematical
+Components library.")
+    (home-page "https://math-comp.github.io/")
+    (license license:cecill-c)))
-- 
2.37.2






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

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


Received: (at 57540) by debbugs.gnu.org; 7 Sep 2022 18:33:52 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Wed Sep 07 14:33:52 2022
Received: from localhost ([127.0.0.1]:56220 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1oVzrz-0007xj-Of
	for submit <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:33:52 -0400
Received: from knopi.disroot.org ([178.21.23.139]:47594)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <garekdyszel@HIDDEN>) id 1oVzry-0007xc-HF
 for 57540 <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:33:50 -0400
Received: from localhost (localhost [127.0.0.1])
 by disroot.org (Postfix) with ESMTP id DB26D40122
 for <57540 <at> debbugs.gnu.org>; Wed,  7 Sep 2022 20:33:49 +0200 (CEST)
X-Virus-Scanned: SPAM Filter at disroot.org
Received: from knopi.disroot.org ([127.0.0.1])
 by localhost (disroot.org [127.0.0.1]) (amavisd-new, port 10024)
 with ESMTP id U2qHALa171Jq for <57540 <at> debbugs.gnu.org>;
 Wed,  7 Sep 2022 20:33:48 +0200 (CEST)
From: Garek Dyszel <garekdyszel@HIDDEN>
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=disroot.org; s=mail;
 t=1662575628; bh=0Vm8pVtRoQ7OvMmNYDZPCZPZIjKfMA57lgPd2pijQHY=;
 h=From:To:Subject:Date;
 b=CnOmtGDsZCxOnn3EmJUUs2zTTF8scvXeNJ24oc6y+xhaNLt6beHac/9HFTdLRIkcC
 VKCtpO50ltiuq08J/Px4UzOUj8w4ptKrYbaFomsCd9+LFFictZ9v/bGQ0vM+NtV1IR
 iGC8CRumbJZ/QapO7UIIXSfYT7WWWNP7TjUAqkT9NTyLuw+6oPWWOP676p7H1Y6C+C
 Pq4ZT8JoRDuGl1fmla+8hpNxTm4nVe/YKYEM9qvbhPhEYiVSvRUvgYObb7qGrXUw49
 f9MoQAK04FCjDDoZKgGWU1GMPTTuq/sUdSpBtXJZj8iWL5zLLLziAmzLKZ+nWL4Ot1
 BOvHvmwAHWeWg==
To: 57540 <at> debbugs.gnu.org
Subject: [RFC PATCH v2 07/19] gnu: Add coq-mathcomp-bigenough.*
 gnu/packages/coq.scm (coq-mathcomp-bigenough): New variable.
Date: Wed, 07 Sep 2022 14:33:46 -0400
Message-ID: <87k06fvxth.fsf@HIDDEN>
Mime-Version: 1.0
Content-Type: text/plain
X-Spam-Score: -0.0 (/)
X-Debbugs-Envelope-To: 57540
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-mathcomp-bigenough): New variable.
---
 gnu/packages/coq.scm | 50 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 50 insertions(+)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index d123860172..78ef5473fd 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -873,3 +873,53 @@ (define-public coq-mathcomp-finmap
 subsume notations for finite sets.")
     (home-page "https://math-comp.github.io/")
     (license license:cecill-b)))
+
+(define-public coq-mathcomp-bigenough
+  ;; On the homepage, it is mentioned that coq-mathcomp-bigenough
+  ;; is going to be obsolete sometime in the near future.
+  ;; This package was included because of the following error,
+  ;; encountered while building coq-mathcomp-analysis:
+  ;; "Warning: in file theories/altreals/realseq.v, library
+  ;; mathcomp.bigenough.bigenough is required and has not been
+  ;; found in the loadpath!"
+  (package
+    (name "coq-mathcomp-bigenough")
+    (version "1.0.1")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://github.com/math-comp/bigenough")
+                    (commit version)
+                    (recursive? #t)))
+              (file-name (git-file-name name version))
+              (sha256
+               (base32
+                "02f4dv4rz72liciwxb2k7acwx6lgqz4381mqyq5854p3nbyn06aw"))))
+    (build-system gnu-build-system)
+    (arguments
+     `( ;"No rule to make target 'test'. Stop."
+       ;; No references to tests in Makefile.common.
+       ;; It doesn't appear as though tests will be included
+       ;; by the packaged project in the future.
+       #:tests? #f
+       #:make-flags ,#~(list (string-append "COQBIN="
+                                            #$(this-package-input "coq-core")
+                                            "/bin/")
+                             (string-append "COQMF_COQLIB="
+                                            (assoc-ref %outputs "out")
+                                            "/lib/ocaml/site-lib/coq")
+                             (string-append "COQLIBINSTALL="
+                                            (assoc-ref %outputs "out")
+                                            "/lib/coq/user-contrib"))
+       #:phases (modify-phases %standard-phases
+                  (delete 'configure))))
+    (propagated-inputs (list coq coq-core coq-mathcomp which))
+    (home-page "https://math-comp.github.io/")
+    (synopsis "Small library to do epsilon - N reasoning")
+    (description
+     "The package contains a package to reasoning with big enough
+objects (mostly natural numbers).  This package is essentially for
+backward compatibility purposes as @code{bigenough} will be subsumed by the
+near tactics.  The formalization is based on the Mathematical
+Components library.")
+    (license license:cecill-b)))
-- 
2.37.2






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

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


Received: (at 57540) by debbugs.gnu.org; 7 Sep 2022 18:33:47 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Wed Sep 07 14:33:47 2022
Received: from localhost ([127.0.0.1]:56217 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1oVzrv-0007xR-Bk
	for submit <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:33:47 -0400
Received: from knopi.disroot.org ([178.21.23.139]:46568)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <garekdyszel@HIDDEN>) id 1oVzrt-0007xJ-7F
 for 57540 <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:33:45 -0400
Received: from localhost (localhost [127.0.0.1])
 by disroot.org (Postfix) with ESMTP id B404940121
 for <57540 <at> debbugs.gnu.org>; Wed,  7 Sep 2022 20:33:44 +0200 (CEST)
X-Virus-Scanned: SPAM Filter at disroot.org
Received: from knopi.disroot.org ([127.0.0.1])
 by localhost (disroot.org [127.0.0.1]) (amavisd-new, port 10024)
 with ESMTP id tuy710Qqmd9D for <57540 <at> debbugs.gnu.org>;
 Wed,  7 Sep 2022 20:33:43 +0200 (CEST)
From: Garek Dyszel <garekdyszel@HIDDEN>
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=disroot.org; s=mail;
 t=1662575622; bh=gm9Nb/AAXlbwoDBozzMU/WFgaJrw/iO9WN8NyqauYYQ=;
 h=From:To:Subject:Date;
 b=YxtYRr/v24NAT81YJylnsc65RUa8znRy4xmxVBtSD2EpLJPjiW4ja8ELEdw6kw0qw
 WoA8eT9FRh1sVSyJJAwerB4TNlPnwylsyHTn+PBWwFeO3ZWobmsatIQS5HW8EWjall
 hHYBFsS+EDIMaBeVntbVXQj86viGZcEUTnTZRwSWjADlxKREXirmrAGuF9Pecb36bL
 fo9Ob6qn7cR6Mj6xoEO8fQMA7Dni4+fN1wLlXajEFR+76eUJfthHVGb2WQmSBUTCdj
 voHsNDPF4057tCPQ07Qp6TTO1zXeF5DjInGYfKKBadE2+Tfa5dbrA0O0bJKEmyqZHk
 GwAsZMSny0VYg==
To: 57540 <at> debbugs.gnu.org
Subject: [RFC PATCH v2 06/19] gnu: Add coq-mathcomp-finmap.*
 gnu/packages/coq.scm (coq-mathcomp-finmap): New variable.
Date: Wed, 07 Sep 2022 14:33:39 -0400
Message-ID: <87leqvvxto.fsf@HIDDEN>
Mime-Version: 1.0
Content-Type: text/plain
X-Spam-Score: -0.0 (/)
X-Debbugs-Envelope-To: 57540
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-mathcomp-finmap): New variable.
---
 gnu/packages/coq.scm | 37 +++++++++++++++++++++++++++++++++++++
 1 file changed, 37 insertions(+)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 24f9492175..d123860172 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -836,3 +836,40 @@ (define-public coq-mathcomp-hierarchy-builder
     (home-page "https://math-comp.github.io/")
     ;; MIT license
     (license license:expat)))
+
+(define-public coq-mathcomp-finmap
+  (package
+    (name "coq-mathcomp-finmap")
+    (version "1.5.2")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://github.com/math-comp/finmap")
+                    (commit version)
+                    (recursive? #t)))
+              (file-name (git-file-name name version))
+              (sha256
+               (base32
+                "1k72wpp15xa5ag358jl8a71gschng0bgbaqjx0l5a0in6x5adafh"))))
+    (build-system gnu-build-system)
+    (arguments
+     `( ;"No rule to make target 'check'."
+       ;; No tests supplied in Makefile.common.
+       ;; The project doesn't appear to have plans to include tests in
+       ;; the future.
+       #:tests? #f
+       #:make-flags (list (string-append "COQLIBINSTALL="
+                                         (assoc-ref %outputs "out")
+                                         "/lib/coq/user-contrib"))
+       #:phases (modify-phases %standard-phases
+                  (delete 'configure))))
+    (inputs (list coq coq-stdlib coq-mathcomp which))
+    (synopsis "Finite sets and finite types for coq-mathcomp")
+    (description
+     "This library is an extension of coq-mathcomp which supports finite sets
+and finite maps on choicetypes (rather than finite types).  This includes
+support for functions with finite support and multisets.  The library also
+contains a generic order and set libary, which will eventually be used to
+subsume notations for finite sets.")
+    (home-page "https://math-comp.github.io/")
+    (license license:cecill-b)))
-- 
2.37.2






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

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


Received: (at 57540) by debbugs.gnu.org; 7 Sep 2022 18:33:41 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Wed Sep 07 14:33:41 2022
Received: from localhost ([127.0.0.1]:56214 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1oVzro-0007x8-TU
	for submit <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:33:41 -0400
Received: from knopi.disroot.org ([178.21.23.139]:45682)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <garekdyszel@HIDDEN>) id 1oVzrn-0007x1-6S
 for 57540 <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:33:39 -0400
Received: from localhost (localhost [127.0.0.1])
 by disroot.org (Postfix) with ESMTP id 888E140122
 for <57540 <at> debbugs.gnu.org>; Wed,  7 Sep 2022 20:33:38 +0200 (CEST)
X-Virus-Scanned: SPAM Filter at disroot.org
Received: from knopi.disroot.org ([127.0.0.1])
 by localhost (disroot.org [127.0.0.1]) (amavisd-new, port 10024)
 with UTF8SMTP id qII2mgx_VAvT for <57540 <at> debbugs.gnu.org>;
 Wed,  7 Sep 2022 20:33:37 +0200 (CEST)
From: Garek Dyszel <garekdyszel@HIDDEN>
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=disroot.org; s=mail;
 t=1662575617; bh=b9xVwYzyCN2zILZQoRrrNUpKqr6BjQsMcfh8YqVCi+I=;
 h=From:To:Subject:Date;
 b=c3Dwt0CzomVFNZdrgTwFPeCSe1ws9bOyK02fOSJgutj8OumMMjfOUxznTdxFKEyDR
 og3/KyjlrEQiqv3HP8/eRZ68dDVjigaoQGEbufo/FhRJWXb42jsxdi5SrWwyJRlo5o
 bcWQ6/pHvNQ4EPAmgTDTUPpSsPsfGTentdxfR+PZdA5+LofmA+Xn/jOLiuan55Dvvu
 qTVlf0407190/yxEg3O2lrpGytIJ4DaEdhOjXgu64v4JO0qQqz0JEb3PyeYR4RDSsO
 PK4X1oo8/iWbBFM10rtt23HQDono/kkSymdgDrjim/D74WbDyyI/gN1wTbBIz4ul53
 f4iEThxAff1Bw==
To: 57540 <at> debbugs.gnu.org
Subject: [RFC PATCH v2 05/19] gnu: Add coq-mathcomp-hierarchy-builder.*
 gnu/packages/coq.scm (coq-mathcomp-hierarchy-builder): New variable.
Date: Wed, 07 Sep 2022 14:33:34 -0400
Message-ID: <87mtbbvxtt.fsf@HIDDEN>
Mime-Version: 1.0
Content-Type: text/plain
X-Spam-Score: -0.0 (/)
X-Debbugs-Envelope-To: 57540
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-mathcomp-hierarchy-builder): New variable.
---
 gnu/packages/coq.scm | 72 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 72 insertions(+)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 5ae5392db4..24f9492175 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -764,3 +764,75 @@ (define-public coq-elpi
 the @code{->} notation.  Finally it provides a way to define new
 vernacular commands and new tactics.")
     (license license:lgpl2.1)))
+
+(define-public coq-mathcomp-hierarchy-builder
+  (package
+    (name "coq-mathcomp-hierarchy-builder")
+    ;; For more information on which version works with Coq 8.15,
+    ;; see the relevant issue:
+    ;; https://github.com/math-comp/hierarchy-builder/issues/297
+    ;; Here we use
+    ;; coq-elpi 1.14.0 + ocaml-elpi 1.15.2 +
+    ;; coq-mathcomp-hierarchy-builder 1.3.0 (Coq 8.15)
+    (version "1.3.0")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://github.com/math-comp/hierarchy-builder")
+                    (commit (string-append "v" version))
+                    (recursive? #t)))
+              (file-name (git-file-name name version))
+              (sha256
+               (base32
+                "17k7rlxdx43qda6i1yafpgc64na8br285cb0mbxy5wryafcdrkrc"))))
+    (build-system gnu-build-system)
+    (arguments
+     `(#:test-target "test-suite"
+       #:make-flags ,#~(list (string-append "COQBIN="
+                                            #$(this-package-input "coq-core")
+                                            "/bin/")
+                             (string-append "COQBININSTALL="
+                                            (assoc-ref %outputs "out") "/bin/")
+                             (string-append "DESTDIR="
+                                            (assoc-ref %outputs "out"))
+                             (string-append "ELPIDIR="
+                                            #$(this-package-input "ocaml-elpi")
+                                            "/lib/ocaml/site-lib/elpi")
+                             (string-append "COQMF_COQLIB="
+                                            (assoc-ref %outputs "out")
+                                            "/lib/ocaml/site-lib/coq")
+                             (string-append "COQLIBINSTALL="
+                                            (assoc-ref %outputs "out")
+                                            "/lib/coq/user-contrib"))
+       #:phases (modify-phases %standard-phases
+                  (delete 'configure)
+                  (replace 'build
+                    (lambda* (#:key make-flags #:allow-other-keys)
+                      (apply invoke "make" "build" make-flags))))))
+    (inputs (list coq
+                  coq-core
+                  coq-mathcomp
+                  which
+                  ocaml
+                  coq-elpi
+                  ocaml-elpi))
+    (synopsis "Hierarchy structures for the Coq proof assistant")
+    (description
+     "Hierarchy Builder (HB) provides high level commands to declare a
+hierarchy of algebraic structure (or interfaces if you prefer the
+glossary of computer science) for the Coq system.
+
+Given a structure one can develop its theory, and that theory becomes
+automatically applicable to all the examples of the structure.  One can
+also declare alternative interfaces, for convenience or backward
+compatibility, and provide glue code linking these interfaces to the
+structures part of the hierarchy.
+
+HB commands compile down to Coq modules, sections, records, coercions,
+canonical structure instances and notations following the packed
+classes discipline which is at the core of the Mathematical Components
+library.  All that complexity is hidden behind a few concepts and a few
+declarative Coq commands.")
+    (home-page "https://math-comp.github.io/")
+    ;; MIT license
+    (license license:expat)))
-- 
2.37.2






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

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


Received: (at 57540) by debbugs.gnu.org; 7 Sep 2022 18:33:37 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Wed Sep 07 14:33:36 2022
Received: from localhost ([127.0.0.1]:56211 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1oVzrk-0007wq-BL
	for submit <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:33:36 -0400
Received: from knopi.disroot.org ([178.21.23.139]:44916)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <garekdyszel@HIDDEN>) id 1oVzri-0007wj-Mt
 for 57540 <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:33:35 -0400
Received: from localhost (localhost [127.0.0.1])
 by disroot.org (Postfix) with ESMTP id 2519E40143
 for <57540 <at> debbugs.gnu.org>; Wed,  7 Sep 2022 20:33:34 +0200 (CEST)
X-Virus-Scanned: SPAM Filter at disroot.org
Received: from knopi.disroot.org ([127.0.0.1])
 by localhost (disroot.org [127.0.0.1]) (amavisd-new, port 10024)
 with ESMTP id pFg9SNe1mnNz for <57540 <at> debbugs.gnu.org>;
 Wed,  7 Sep 2022 20:33:32 +0200 (CEST)
From: Garek Dyszel <garekdyszel@HIDDEN>
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=disroot.org; s=mail;
 t=1662575611; bh=9hdvu8SoSfKBRc8s0Z7w+m5qGLkLMKWU7xm0RjbJafk=;
 h=From:To:Subject:Date;
 b=ht9Lbiho5hvF3cN59EYFrssx2kS4DgPRWX4vsVjZKeg58dDgI1B+eIwblKt24qW1/
 Tn/1Ae/oClc8AmXuLuriVzoyIGnIqvtw+vrVJXXuf22JHvFojPJ1JaJbPXSe2RBfsl
 Zad3xu06q/qENTnHHZ2a1snDLuUXcHnjPoTrKsoHUzGxeA7tTU3jd89R74r8hQn3O7
 GTerRi1mopOYw2ANG+USzI8/2d2G8PN6s4ZwAisDKSkWwf+gcRQ/rd4nHBfF5sVG0K
 DxgrC2Q3Z8L25+ewxPPXjLH4mrU2whdRUQj2OuD9cqICsPFWpr1o+KteGHfkoSWSau
 2ibjdm29Oq8Kw==
To: 57540 <at> debbugs.gnu.org
Subject: [RFC PATCH v2 04/19] gnu: Add coq-elpi.* gnu/packages/coq.scm
 (coq-elpi): New variable.
Date: Wed, 07 Sep 2022 14:33:27 -0400
Message-ID: <87o7vrvxu0.fsf@HIDDEN>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: quoted-printable
X-Spam-Score: 2.0 (++)
X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org",
 has NOT identified this incoming email as spam.  The original
 message has been attached to this so you can view it or label
 similar future email.  If you have any questions, see
 the administrator of that system for details.
 
 Content preview:  * gnu/packages/coq.scm (coq-elpi): New variable. --- gnu/packages/coq.scm
    | 79 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 79 insertions(+)
    diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index bbb34df27d..5ae5392db4
    100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -8,6 +8,7
    @@ ;;; Copyright © 2020 Robin Green <gr [...] 
 
 Content analysis details:   (2.0 points, 10.0 required)
 
  pts rule name              description
 ---- ---------------------- --------------------------------------------------
  0.0 SPF_HELO_NONE          SPF: HELO does not publish an SPF Record
 -0.0 SPF_PASS               SPF: sender matches SPF record
  2.0 PDS_OTHER_BAD_TLD      Untrustworthy TLDs
                             [URI: yoctocell.xyz (xyz)]
 -0.0 T_SCC_BODY_TEXT_LINE   No description available.
X-Debbugs-Envelope-To: 57540
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-elpi): New variable.
---
 gnu/packages/coq.scm | 79 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 79 insertions(+)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index bbb34df27d..5ae5392db4 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -8,6 +8,7 @@
 ;;; Copyright =C2=A9 2020 Robin Green <greenrd@HIDDEN>
 ;;; Copyright =C2=A9 2021 Xinglu Chen <public@HIDDEN>
 ;;; Copyright =C2=A9 2021 Simon Tournier <zimon.toutoune@HIDDEN>
+;;; Copyright =C2=A9 2022 Garek Dyszel <garekdyszel@HIDDEN>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -685,3 +686,81 @@ (define-public coq-stdpp
 @end itemize")
     (home-page "https://gitlab.mpi-sws.org/iris/stdpp")
     (license license:bsd-3)))
+
+(define-public coq-elpi
+  (package
+    (name "coq-elpi")
+    ;; For more information on which version works with Coq 8.15,
+    ;; see the relevant issue:
+    ;; https://github.com/math-comp/hierarchy-builder/issues/297
+    ;; Here we use
+    ;; coq-elpi 1.14.0 + ocaml-elpi 1.15.2 +
+    ;; coq-mathcomp-hierarchy-builder 1.3.0 (Coq 8.15)
+    (version "1.14.0")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://github.com/LPCIC/coq-elpi")
+                    (commit (string-append "v" version))
+                    (recursive? #t)))
+              (file-name (git-file-name name version))
+              (sha256
+               (base32
+                "1v2p5dlpviwzky2i14cj7gcgf8cr0j54bdm9fl5iz1ckx60j6nvp"))))
+    (build-system gnu-build-system)
+    (outputs '("out"))
+    (arguments
+     `(#:make-flags ,#~(list (string-append "COQBIN=3D"
+                                            #$(this-package-input "coq-cor=
e")
+                                            "/bin/")
+                             (string-append "ELPIDIR=3D"
+                                            #$(this-package-input "ocaml-e=
lpi")
+                                            "/lib/ocaml/site-lib/elpi")
+                             (string-append "COQMF_COQLIB=3D"
+                                            (assoc-ref %outputs "out")
+                                            "/lib/ocaml/site-lib/coq")
+                             (string-append "COQLIBINSTALL=3D"
+                                            (assoc-ref %outputs "out")
+                                            "/lib/coq/user-contrib"))
+
+       #:phases (modify-phases %standard-phases
+                  (delete 'configure)
+                  (add-before 'build 'remove-extra-src-file
+                    (lambda* (#:key outputs #:allow-other-keys)
+                      ;; Remove the useless line "src/META.coq-elpi"
+                      ;; in file _CoqProject. The file
+                      ;; src/META.coq-elpi does not exist in the
+                      ;; repository, so this line inhibits compilation
+                      ;; unnecessarily.
+                      (invoke "sed" "-i" "s|src/META.coq-elpi||g"
+                              "_CoqProject")))
+                  (replace 'check
+                    ;; Error when running the "check" phase:
+                    ;; "make: *** No rule to make target 'check'.
+                    ;; Stop."
+                    ;; Tests run if we invoke "make test" instead.
+                    (lambda* (#:key tests? make-flags #:allow-other-keys)
+                      (when tests?
+                        (apply invoke "make" "test" make-flags)))))))
+    (inputs (list python))
+    (propagated-inputs (list ocaml
+                             ocaml-stdlib-shims
+                             ocaml-elpi
+                             ocaml-zarith
+                             coq-core
+                             coq-stdlib))
+    (home-page "https://github.com/LPCIC/coq-elpi")
+    (synopsis "Elpi extension language for Coq")
+    (description
+     "Coq-elpi provides a Coq plugin that embeds ELPI.  It also
+provides a way to embed Coq's terms into =CE=BBProlog using the
+Higher-Order Abstract Syntax approach and a way to read terms back.
+In addition to that it exports to ELPI a set of Coq's primitives, e.g.
+printing a message, accessing the environment of theorems and data
+types, defining a new constant and so on.  For convenience it also
+provides a quotation and anti-quotation for Coq's syntax in =CE=BBProlog.
+E.g. @code{{{nat}}} is expanded to the type name of natural numbers,
+or @code{{{A -> B}}} to the representation of a product by unfolding
+the @code{->} notation.  Finally it provides a way to define new
+vernacular commands and new tactics.")
+    (license license:lgpl2.1)))
--=20
2.37.2






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

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


Received: (at 57540) by debbugs.gnu.org; 7 Sep 2022 18:33:08 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Wed Sep 07 14:33:08 2022
Received: from localhost ([127.0.0.1]:56208 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1oVzrH-0007wB-SM
	for submit <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:33:08 -0400
Received: from knopi.disroot.org ([178.21.23.139]:38696)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <garekdyszel@HIDDEN>) id 1oVzrF-0007w3-Oh
 for 57540 <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:33:06 -0400
Received: from localhost (localhost [127.0.0.1])
 by disroot.org (Postfix) with ESMTP id 2E4DE49FCA;
 Wed,  7 Sep 2022 20:33:05 +0200 (CEST)
X-Virus-Scanned: SPAM Filter at disroot.org
Received: from knopi.disroot.org ([127.0.0.1])
 by localhost (disroot.org [127.0.0.1]) (amavisd-new, port 10024)
 with ESMTP id seUIkKGZIOOP; Wed,  7 Sep 2022 20:33:03 +0200 (CEST)
From: Garek Dyszel <garekdyszel@HIDDEN>
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=disroot.org; s=mail;
 t=1662575583; bh=3mnxBZR2b80pfRb0QAsvr5JEXkBQK0V1dv56pU6qxSs=;
 h=From:To:Cc:Subject:Date;
 b=dvN2mOm/aamiMIht7tSJ5AoZeqYgXHN+dnRcJ81NNkFfaNh6pCEV4XiM4ciGZP686
 yGmUXsJD9qcrQIRzKBq5F1pfvIh1yGqcn+0JTPhujkurFQhzFTiJsnGNzvghxPCsWy
 92HASwtrCKFas6jGhnTdCqSeDJeYiO7sIDhs6t0QgkbHd/yvyMlVpB+zKpSUAHByNl
 wEVjoT7IMZrSjYE71omjtX55xlc19QivGbvln3FYiKmg/bQrUNNjz4FsgYF/eO5EtS
 biAl5uoscr2BTYjsvMwHfsL3J8mxYMWBB0yLxjyfmUr6eAYfUJhpJi6/pxFwIHKJys
 BZpd/7GyoGPCw==
To: Julien Lepiller <julien@HIDDEN>
Subject: [RFC PATCH v2 03/19] gnu: Add ocaml-ansiterminal.*
 gnu/packages/ocaml.scm (ocaml-ansiterminal): New variable.
Date: Wed, 07 Sep 2022 14:33:00 -0400
Message-ID: <87pmg7vxur.fsf@HIDDEN>
Mime-Version: 1.0
Content-Type: text/plain
X-Spam-Score: -0.0 (/)
X-Debbugs-Envelope-To: 57540
Cc: 57540 <at> debbugs.gnu.org
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/ocaml.scm (ocaml-ansiterminal): New variable.
---
 gnu/packages/ocaml.scm | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index 11b982519b..ac0e0c0bc1 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -8929,3 +8929,32 @@ (define-public ocaml-atd
 good fit with a variety of data formats.")
     ;; Modified BSD license
     (license (license:non-copyleft "LICENSE.md"))))
+
+(define-public ocaml-ansiterminal
+  (package
+    (name "ocaml-ansiterminal")
+    (version "0.8.5")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://github.com/Chris00/ANSITerminal")
+                    (commit version)
+                    (recursive? #t)))
+              (file-name (git-file-name name version))
+              (sha256
+               (base32
+                "052qnc23vmxp90yympjz9q6lhqw98gs1yvb3r15kcbi1j678l51h"))))
+    (build-system dune-build-system)
+    (arguments
+     `(#:test-target "tests"))
+    (home-page "https://github.com/Chris00/ANSITerminal")
+    (synopsis
+     "Basic control of ANSI compliant terminals and the windows shell")
+    (description
+     "ANSITerminal is a module allowing to use the colors and cursor
+movements on ANSI terminals.")
+    ;; Variant of the GPL3 which permits
+    ;; static and dynamic linking when producing binary files.
+    ;; In other words, it allows one to link to the library
+    ;; when compiling nonfree software.
+    (license (license:non-copyleft "LICENSE"))))
-- 
2.37.2






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

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


Received: (at 57540) by debbugs.gnu.org; 7 Sep 2022 18:33:02 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Wed Sep 07 14:33:02 2022
Received: from localhost ([127.0.0.1]:56205 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1oVzrC-0007vt-Ge
	for submit <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:33:02 -0400
Received: from knopi.disroot.org ([178.21.23.139]:37540)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <garekdyszel@HIDDEN>) id 1oVzrA-0007vN-JI
 for 57540 <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:33:01 -0400
Received: from localhost (localhost [127.0.0.1])
 by disroot.org (Postfix) with ESMTP id 09DCD40123;
 Wed,  7 Sep 2022 20:33:00 +0200 (CEST)
X-Virus-Scanned: SPAM Filter at disroot.org
Received: from knopi.disroot.org ([127.0.0.1])
 by localhost (disroot.org [127.0.0.1]) (amavisd-new, port 10024)
 with ESMTP id KMDVTpJtRc8F; Wed,  7 Sep 2022 20:32:58 +0200 (CEST)
From: Garek Dyszel <garekdyszel@HIDDEN>
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=disroot.org; s=mail;
 t=1662575575; bh=pd9pUdKrEjzDqeqqhGEHu4Gcvar8m2RNX4vDewBfxxU=;
 h=From:To:Cc:Subject:Date;
 b=CnOuCzpMd6TE7CiV1v1LnT1iO+TWxB154Z/H6IolyWBsxPl12R0m9CKcnqQwLzws7
 qQY9m1HLvmdRd+u2dqbxDryO82yohQx2ixlrWtKumV909Rkm/25TRQsZGdRIGWpw8a
 fa+hxtyfpmcWDFMQ2XhNjbmOycrU+J4j41ugSeHA/dMTo6WebMWzZNfTkwkBuAkxQA
 FcZrzPUnHBASA+Xbm/Prf/kmpSTHoZMLMBr8tgRj95ignNfb2No40O0c4/4E6YmDqR
 dhD1+r0Ljn+F0CuytTk6kJAuilGYuDuObNWyO8IABqPi9DsB5V2Msp1TjBIfKr6Rt0
 UEbXins+KOR0A==
To: Julien Lepiller <julien@HIDDEN>
Subject: [RFC PATCH v2 02/19] gnu: Add ocaml-atd.* gnu/packages/ocaml.scm
 (ocaml-atd): New variable.
Date: Wed, 07 Sep 2022 14:32:52 -0400
Message-ID: <87r10nvxuz.fsf@HIDDEN>
Mime-Version: 1.0
Content-Type: text/plain
X-Spam-Score: -0.0 (/)
X-Debbugs-Envelope-To: 57540
Cc: 57540 <at> debbugs.gnu.org
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/ocaml.scm (ocaml-atd): New variable.
---
 gnu/packages/ocaml.scm | 59 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 59 insertions(+)

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index c4fa05b934..11b982519b 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -8870,3 +8870,62 @@ (define-public ocaml-elpi
 
 ELPI is free software released under the terms of LGPL 2.1 or above.")
     (license license:lgpl2.1)))
+
+;; NOTE: requires python-jsonschema with version at minimum 4.6.0 to run
+;; tests.
+;; See https://github.com/ahrefs/atd/issues/306 for more info on that.
+(define-public ocaml-atd
+  (package
+    (name "ocaml-atd")
+    (version "2.10.0")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://github.com/ahrefs/atd")
+                    (commit version)
+                    (recursive? #t)))
+              (file-name (git-file-name name version))
+              (sha256
+               (base32
+                "10fgahdigrl01py0k0q2d6a60yps38q96dxhjnzm9jz4g931716l"))))
+    (build-system dune-build-system)
+    (arguments
+     `(#:phases (modify-phases %standard-phases
+                  (replace 'check
+                    (lambda* (#:key tests? #:allow-other-keys)
+                      ;; The dune-build-system does not run "make test" but
+                      ;; "dune runtest test --release".
+                      ;; This project, rather, needs us to run "make test".
+                      ;;
+                      ;; For this package (ocaml-atd), we DO NOT run all the
+                      ;; tests. The atd repository has resources for several
+                      ;; different interfaces (python, scala, etc), but we
+                      ;; don't need to run those tests if we are just
+                      ;; interested in the ocaml interface.
+                      ;; So we stick with just the ocaml tests here.
+                      (when tests?
+                        (invoke "make" "test-ocaml")))))))
+    (propagated-inputs (list ocaml-menhir
+                             ocaml-easy-format
+                             ocaml-odoc
+                             ocaml-re
+                             ocaml-camlp-streams
+                             ocaml-biniou
+                             ocaml-yojson
+                             ocaml-cmdliner))
+    (native-inputs (list ocaml-alcotest
+                         python
+                         python-pypa-build
+                         python-jsonschema-4.15
+                         python-flake8
+                         python-mypy
+                         python-pytest))
+    (home-page "https://github.com/ahrefs/atd")
+    (synopsis "Parser for the ATD data format description language")
+    (description
+     "ATD is the OCaml library providing a parser for the ATD language
+and various utilities.  ATD stands for Adjustable Type Definitions in
+reference to its main property of supporting annotations that allow a
+good fit with a variety of data formats.")
+    ;; Modified BSD license
+    (license (license:non-copyleft "LICENSE.md"))))
-- 
2.37.2






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

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


Received: (at 57540) by debbugs.gnu.org; 7 Sep 2022 18:32:04 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Wed Sep 07 14:32:04 2022
Received: from localhost ([127.0.0.1]:56201 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1oVzqF-0007uG-Ro
	for submit <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:32:04 -0400
Received: from knopi.disroot.org ([178.21.23.139]:52166)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <garekdyszel@HIDDEN>) id 1oVzqC-0007ti-Ir
 for 57540 <at> debbugs.gnu.org; Wed, 07 Sep 2022 14:32:01 -0400
Received: from localhost (localhost [127.0.0.1])
 by disroot.org (Postfix) with ESMTP id AAE1549FB1;
 Wed,  7 Sep 2022 20:31:58 +0200 (CEST)
X-Virus-Scanned: SPAM Filter at disroot.org
Received: from knopi.disroot.org ([127.0.0.1])
 by localhost (disroot.org [127.0.0.1]) (amavisd-new, port 10024)
 with ESMTP id 0Gi2oDSXmWyU; Wed,  7 Sep 2022 20:31:56 +0200 (CEST)
From: Garek Dyszel <garekdyszel@HIDDEN>
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=disroot.org; s=mail;
 t=1662575516; bh=jy0rRrWFl0DBgusVuCdqy7pFYKpeiyEucD56ZbboIgY=;
 h=From:To:Cc:Subject:Date;
 b=WPLjVg6XrAb45OIQNvJ8FJ0a9JcgXkQy8C5VS1M3uW5Fy6dGlePFOWK8GgPTgWYop
 VLKU1uPoaZLddKpX7m0iH0eKBK5QS09p0WqE6kJg0Uq/LfApCinm5errottA0PWAmT
 Ym6AMFmbzzlKoJ+gj8iQOuVHOtwg+v3dVQ1Ecp+x4RfeJ4609o/q9WbQtIwUrQEnSk
 kvm968Dr4i/IAxBZtn2JSE/JIerpTJLNAsh/O0ggsiJlXoXQhvC9hiIFVeQmDQ4fRr
 7nM4sfBJ+YYZl/iS/HfxKyVFj8x6wQ5930/V7Fki4HCkcB1UFOsAfVCBG7QSPAr8Hh
 SFUq2R1uDh+kg==
To: Julien Lepiller <julien@HIDDEN>
Subject: [RFC PATCH v2 01/19] gnu: Add ocaml-elpi.
Date: Wed, 07 Sep 2022 14:31:47 -0400
Message-ID: <87sfl3vxws.fsf@HIDDEN>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: quoted-printable
X-Spam-Score: -0.0 (/)
X-Debbugs-Envelope-To: 57540
Cc: 57540 <at> debbugs.gnu.org
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 (-)

Hi Julien,

Thank you for your thoughtful suggestions! All patches are now split such t=
hat each package has its own patch.

* Quickies
> And then I wonder why you need that at all, if it doesn't change
> compilation result?
The file src/META.coq-elpi does not exist in the source tree. I changed the=
 comment; hopefully it's less ambiguous now.

> Please don't use #t at the end of phases anymore.
Thanks for catching this! It's removed.

>  Instead of replacing this phase, maybe try #:test-target "test-suite"
This worked, thanks!

> If that means that future versions will have tests (for instance if
> master has tests), maybe this should say it more explicitely.
It looks like coq-mathcomp-analysis has no tests and no plans to include an=
y tests in the traditional sense. I changed the comment to reflect that.

* Other changes
For all the ocaml packages, using #:test-target as suggested with the appro=
priate directory worked. There still remain three packages without tests, b=
ut tests were not supplied with those three.

I had to add about 10 python packages in order to get the tests for ocaml-a=
td to pass.

Some packages (python-pluggy-1.0, python-jsonschema-4.15, python-setuptools=
-scm-7) are present already in the Guix tree  were required by the ocaml-at=
d tests.

Is there a better way to include those packages without sending this patch =
through core-updates?

Lists should now be formatted with @itemize (assuming I didn't miss any!).

We now use git-references for most packages. In cases where git-references =
were not used, they were python packages. The tests with the PyPi versions =
passed, but using the git repository for the same package yielded failing t=
ests.=20

* Remaining issues
This set of patches still is not ready to be merged; python-hatchling break=
s Guix. The upstream hash differed this afternoon from a "guix hash -rx ." =
run from this morning, though the commit we are building from hasn't change=
d. The command "pytest -vv" in phase "check" fails with: "ERROR Missing dep=
endencies: pluggy>=3D1.0.0". It seems that python-pluggy-1.0 built correctl=
y, so maybe it is just not specified correctly in the inputs for python-hat=
chling?

What do you think?

Thanks again for the help!
Garek

* gnu/packages/ocaml.scm (ocaml-elpi): New variable.
---
 gnu/packages/ocaml.scm | 96 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 96 insertions(+)

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index 2fd519ca41..c4fa05b934 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -26,6 +26,7 @@
 ;;; Copyright =C2=A9 2021 Sarah Morgensen <iskarian@HIDDEN>
 ;;; Copyright =C2=A9 2022 Maxim Cournoyer <maxim.cournoyer@HIDDEN>
 ;;; Copyright =C2=A9 2022 John Kehayias <john.kehayias@HIDDEN>
+;;; Copyright =C2=A9 2022 Garek Dyszel <garekdyszel@HIDDEN>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -8774,3 +8775,98 @@ (define-public ocaml-guile
      "The OCaml guile library provides high-level OCaml bindings to GNU Gu=
ile
 3.0, supporting easy interop between OCaml and GNU Guile Scheme.")
     (license license:gpl3+)))
+
+(define-public ocaml-elpi
+  (package
+    (name "ocaml-elpi")
+    ;; For more information on which version works with Coq 8.15,
+    ;; see the relevant issue:
+    ;; https://github.com/math-comp/hierarchy-builder/issues/297
+    ;; Here we use
+    ;; coq-elpi 1.14.0 + ocaml-elpi 1.15.2 +
+    ;; coq-mathcomp-hierarchy-builder 1.3.0 (Coq 8.15)
+    ;;
+    ;; The package ocaml-elpi@HIDDEN appears to require a different
+    ;; build process.
+    (version "1.15.2")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://github.com/LPCIC/elpi")
+                    (commit (string-append "v" version))
+                    (recursive? #t)))
+              (file-name (git-file-name name version))
+              (sha256
+               (base32
+                "0swzqabwrxqb6sz8zpild2lfcnk3l0zxi9fw61dy2g1pzws2j2jy"))))
+    (build-system dune-build-system)
+    (arguments
+     `(#:test-target "tests"))
+    (propagated-inputs (list ocaml-stdlib-shims
+                             ocaml-ppxlib
+                             ocaml-menhir
+                             ocaml-re
+                             ocaml-ppx-deriving
+                             ocaml-atd
+                             ocaml-camlp-streams
+                             ocaml-biniou
+                             ocaml-yojson))
+    (native-inputs (list ocaml-ansiterminal ocaml-cmdliner time))
+    (home-page "https://github.com/LPCIC/elpi")
+    (synopsis "ELPI - Embeddable =CE=BBProlog Interpreter")
+    (description
+     "ELPI implements a variant of =CE=BBProlog enriched with Constraint
+Handling Rules, a programming language well suited to manipulate
+syntax trees with binders.
+
+ELPI is designed to be embedded into larger applications written in
+OCaml as an extension language.  It comes with an API to drive the
+interpreter and with an FFI for defining built-in predicates and data
+types, as well as quotations and similar goodies that are handy to
+adapt the language to the host application.
+
+This package provides both a command line interpreter (elpi) and a
+library to be linked in other applications (eg by passing -package
+elpi to ocamlfind).
+
+The ELPI programming language has the following features:
+
+@itemize
+@item Native support for variable binding and substitution, via an Higher
+Order Abstract Syntax (HOAS) embedding of the object language.  The
+programmer does not need to care about technical devices to handle
+bound variables, like De Bruijn indices.
+
+@item Native support for hypothetical context.  When moving under a binder
+one can attach to the bound variable extra information that is
+collected when the variable gets out of scope.  For example when
+writing a type-checker the programmer needs not to care about managing
+the typing context.
+
+@item Native support for higher order unification variables, again via
+HOAS.  Unification variables of the meta-language (=CE=BBProlog) can be
+reused to represent the unification variables of the object language.
+The programmer does not need to care about the unification-variable
+assignment map and cannot assign to a unification variable a term
+containing variables out of scope, or build a circular assignment.
+
+@item Native support for syntactic constraints and their meta-level
+handling rules.  The generative semantics of Prolog can be disabled by
+turning a goal into a syntactic constraint (suspended goal).  A
+syntactic constraint is resumed as soon as relevant variables gets
+assigned.  Syntactic constraints can be manipulated by constraint
+handling rules (CHR).
+
+@item Native support for backtracking.  To ease implementation of search.
+
+@item The constraint store is extensible.  The host application can declare
+non-syntactic constraints and use custom constraint solvers to check
+their consistency.
+
+@item Clauses are graftable.  The user is free to extend an existing
+program by inserting/removing clauses, both at runtime (using
+implication) and at \"compilation\" time by accumulating files.
+@end itemize
+
+ELPI is free software released under the terms of LGPL 2.1 or above.")
+    (license license:lgpl2.1)))
--=20
2.37.2






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

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


Received: (at 57540) by debbugs.gnu.org; 3 Sep 2022 18:40:44 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Sat Sep 03 14:40:44 2022
Received: from localhost ([127.0.0.1]:43024 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1oUY4S-0007Kh-EG
	for submit <at> debbugs.gnu.org; Sat, 03 Sep 2022 14:40:44 -0400
Received: from lepiller.eu ([89.234.186.109]:53502)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <julien@HIDDEN>) id 1oUY4O-0007KX-KH
 for 57540 <at> debbugs.gnu.org; Sat, 03 Sep 2022 14:40:43 -0400
Received: from lepiller.eu (localhost [127.0.0.1])
 by lepiller.eu (OpenSMTPD) with ESMTP id d8fe000d;
 Sat, 3 Sep 2022 18:40:38 +0000 (UTC)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed; d=lepiller.eu; h=date:from
 :to:cc:subject:message-id:in-reply-to:references:mime-version
 :content-type:content-transfer-encoding; s=dkim; bh=ox6TWUgPb88s
 kSOB7VAwSixZMt7C3pITidR8BjGCbeY=; b=Zre1ZZx7ohkYao4l+VOMA4l0i2cX
 wh2NBTR4frn8oSh1haS2r7Am2KtmAMK+IxAmCdX46V0JdSytMV+nw13g+yvIFIYA
 KQxJNEwP/ThJubjWeGBaTsvDaKVBr5c+mmfaTkfxNOrkR5O6ir9TpfHpKXZgPNYw
 HgVSJ85RUMZNar/UakdLMuUtoz94unZ8Nh8bpxQupf9DUxQrzriVr9qDuaptSNw4
 WtG1TVeN3wxB/dC977yddmKDnI70vuSD6MOaOmn22o4C06nrGW2Z21dCYlGeZDYK
 LHDcMlum9a/3BJ0D0CE4hOr12z3ysxXD1jdEqp95jpf31yZUeTtmEPiE7A==
Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id 1ae6b595
 (TLSv1.3:AEAD-AES256-GCM-SHA384:256:NO); 
 Sat, 3 Sep 2022 18:40:37 +0000 (UTC)
Date: Sat, 3 Sep 2022 20:40:35 +0200
From: Julien Lepiller <julien@HIDDEN>
To: Garek Dyszel <garekdyszel@HIDDEN>
Subject: Re: [bug#57540] [PATCH] Add ocaml-elpi (a dependency of
 coq-mathcomp-analysis)
Message-ID: <20220903204035.22e3b372@HIDDEN>
In-Reply-To: <79d544f7d8ba64b631a6f0f1d2ef0b08@HIDDEN>
References: <79d544f7d8ba64b631a6f0f1d2ef0b08@HIDDEN>
X-Mailer: Claws Mail 4.1.0 (GTK 3.24.30; x86_64-pc-linux-gnu)
MIME-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
X-Spam-Score: -0.0 (/)
X-Debbugs-Envelope-To: 57540
Cc: 57540 <at> debbugs.gnu.org
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 (-)

Hi Garek,

thanks for the patches! As I understand it, these patches introduce 8
new packages, but I count only 7 (with this one which didn't make it as
a part of the series). Could you split the last patch, so each new
package has its own patch?

Also, some points in your patches:

For "Don't know about directory test", you can try with an argument:
#:test-target "some-dir". This directory is the directory where tests
are located. If there is no single directory, you can try
#:test-target "."

Descriptions should use our subset of texinfo. Basically, lists should
look like:

@itemize
@item foo
@item bar
@end itemize

and you can use @file, @code, etc as you see fit (to replace markdown's
"`").

Whenever possible, we try not to rely on github tarballs, so it'd be
best to use a git-reference in all your patches :)

In coq-elpi:

> +                      ;; Remove the useless line
> +                      ;; "src/META.coq-elpi"
> +                      ;; in file _CoqProject.
> +                      ;; It does not affect
> +                      ;; the success of compliation.

should be "compilation". And then I wonder why you need that at all, if
it doesn't change compilation result?

> +                      #t))

Please don't use #t at the end of phases anymore.

> +                  (replace 'check

The gnu-build-system already runs "make test", doesn't it? Why do you
need to replace this phase?


In coq-mathcomp-hierarchy-builder:

> +                  (replace 'check

Instead of replacing this phase, maybe try #:test-target "test-suite"

> +       ;; Makefile.common has no references to tests at all
> +       ;; (yet).

If that means that future versions will have tests (for instance if
master has tests), maybe this should say it more explicitely.

Once you fix all this, could you send a v2 series? Thank you!




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

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


Received: (at 57540) by debbugs.gnu.org; 2 Sep 2022 15:29:05 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Fri Sep 02 11:29:05 2022
Received: from localhost ([127.0.0.1]:47483 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1oU8bR-00084q-7a
	for submit <at> debbugs.gnu.org; Fri, 02 Sep 2022 11:29:05 -0400
Received: from knopi.disroot.org ([178.21.23.139]:41538)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <garekdyszel@HIDDEN>) id 1oU8bQ-00084j-13
 for 57540 <at> debbugs.gnu.org; Fri, 02 Sep 2022 11:29:04 -0400
Received: from localhost (localhost [127.0.0.1])
 by disroot.org (Postfix) with ESMTP id 5E60C49FAC
 for <57540 <at> debbugs.gnu.org>; Fri,  2 Sep 2022 17:29:03 +0200 (CEST)
X-Virus-Scanned: SPAM Filter at disroot.org
Received: from knopi.disroot.org ([127.0.0.1])
 by localhost (disroot.org [127.0.0.1]) (amavisd-new, port 10024)
 with UTF8SMTP id Fqjb6HtN0_TZ for <57540 <at> debbugs.gnu.org>;
 Fri,  2 Sep 2022 17:29:01 +0200 (CEST)
Mime-Version: 1.0
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=disroot.org; s=mail;
 t=1662132348; bh=Y6CP7UBq27/LruMP8Ajvwr3NlhxPwVCIiDfLKm85lVU=;
 h=Date:From:To:Subject;
 b=C7CmnsJSMSE3UvxxUQ5qRZXoVDGaV1lZcw+FHlAfJYNHYjWGCMh1fDN4Ch7uS6Vlf
 7B2d3cdZtDzOjEPZF5dTaKx2mTKp12F4nnnxiZQAM6C3AkMttEqnp0gRAN/TJdCP1J
 qoqf8rNH1+J0cDfjZjAwG4uP3gVqoerCK9wvWW7yNuqV80ZoM9PXLkpxL7Yd15xzDL
 PcgjZsZlfpIs+hsMfm2RkVN3B+VmJdfZn8MAXsBcCTKeOnefi0HO8xrwhziACo/GIk
 Ttxi3Hi9xyeimOr3M70uHx4suVAx5peXkibSioLzDPS8jK3S3aXmmsBn+bOoJcoAlH
 eR/9EFImktifA==
Date: Fri, 02 Sep 2022 11:25:48 -0400
From: Garek Dyszel <garekdyszel@HIDDEN>
To: 57540 <at> debbugs.gnu.org
Subject: [PATCH 6/6] gnu: Add coq-mathcomp-bigenough and coq-mathcomp-analysis.
Message-ID: <e034d85426248aa93e3a8a1c0609d1e6@HIDDEN>
X-Sender: garekdyszel@HIDDEN
Content-Type: text/plain; charset=US-ASCII;
 format=flowed
Content-Transfer-Encoding: 7bit
X-Spam-Score: 0.0 (/)
X-Debbugs-Envelope-To: 57540
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-mathcomp-bigenough coq-mathcomp-analysis)
---
  gnu/packages/coq.scm | 105 +++++++++++++++++++++++++++++++++++++++++++
  1 file changed, 105 insertions(+)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index f0aa233..680c2fa 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -869,3 +869,108 @@ (define-public coq-mathcomp-finmap
  subsume notations for finite sets.")
      (home-page "https://math-comp.github.io/")
      (license license:cecill-b)))
+
+(define-public coq-mathcomp-bigenough
+  ;; On the homepage, it is mentioned that coq-mathcomp-bigenough
+  ;; is going to be obsolete sometime in the near future.
+  ;; This package was included because of the following error,
+  ;; encountered while building coq-mathcomp-analysis:
+  ;; "Warning: in file theories/altreals/realseq.v, library
+  ;; mathcomp.bigenough.bigenough is required and has not been
+  ;; found in the loadpath!"
+  ;; So added https://github.com/math-comp/bigenough.
+  (package
+    (name "coq-mathcomp-bigenough")
+    (version "1.0.1")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://github.com/math-comp/bigenough")
+                    (commit version)
+                    (recursive? #t)))
+              (file-name (git-file-name name version))
+              (sha256
+               (base32
+                
"02f4dv4rz72liciwxb2k7acwx6lgqz4381mqyq5854p3nbyn06aw"))))
+    (build-system gnu-build-system)
+    (arguments
+     `( ;"No rule to make target 'test'. Stop."
+       ;; No references to tests in Makefile.common.
+       #:tests? #f
+       #:make-flags ,#~(list (string-append "COQBIN="
+                                            #$(this-package-input 
"coq-core")
+                                            "/bin/")
+                             (string-append "COQMF_COQLIB="
+                                            (assoc-ref %outputs "out")
+                                            "/lib/ocaml/site-lib/coq")
+                             (string-append "COQLIBINSTALL="
+                                            (assoc-ref %outputs "out")
+                                            "/lib/coq/user-contrib"))
+       #:phases (modify-phases %standard-phases
+                  (delete 'configure))))
+    (propagated-inputs (list coq coq-core coq-mathcomp which))
+    (home-page "https://math-comp.github.io/")
+    (synopsis "Small library to do epsilon - N reasoning")
+    (description
+     "The package contains a package to reasoning with big enough
+objects (mostly natural numbers).  This package is essentially for
+backward compatibility purposes as `bigenough` will be subsumed by the
+near tactics.  The formalization is based on the Mathematical
+Components library.")
+    (license license:cecill-b)))
+
+(define-public coq-mathcomp-analysis
+  (package
+    (name "coq-mathcomp-analysis")
+    (version "0.5.3")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://github.com/math-comp/analysis")
+                    (commit version)))
+              (file-name (git-file-name name version))
+              (sha256
+               (base32
+                
"16bv2kxm6nrgfm9lp88sls1vqs26d4m3fxbccmy328ak5srcbn6l"))))
+    (build-system gnu-build-system)
+    (arguments
+     `( ;No tests were supplied with this library:
+       ;; No rule to make target 'check'. Stop.
+       ;; Makefile.common has no references to tests at all
+       ;; (yet).
+       #:tests? #f
+       #:make-flags ,#~(list (string-append "COQBIN="
+                                            #$(this-package-input 
"coq-core")
+                                            "/bin/")
+                             (string-append "COQBININSTALL="
+                                            (assoc-ref %outputs "out") 
"/bin/")
+                             (string-append "DESTDIR="
+                                            (assoc-ref %outputs "out"))
+                             (string-append "COQMF_COQLIB="
+                                            (assoc-ref %outputs "out")
+                                            "/lib/ocaml/site-lib/coq")
+                             (string-append "COQLIBINSTALL="
+                                            (assoc-ref %outputs "out")
+                                            "/lib/coq/user-contrib"))
+       #:phases (modify-phases %standard-phases
+                  (delete 'configure)
+                  (replace 'build
+                    (lambda* (#:key make-flags #:allow-other-keys)
+                      (apply invoke "make" "build" make-flags))))))
+    (inputs (list coq
+                  coq-stdlib
+                  coq-mathcomp
+                  coq-mathcomp-finmap
+                  coq-mathcomp-hierarchy-builder
+                  coq-elpi-1.14
+                  coq-mathcomp-bigenough
+                  coq-core
+                  which
+                  python))
+    (synopsis "Real analysis for the Coq proof assistant")
+    (description
+     "This repository contains an experimental library for
+real analysis for the Coq proof-assistant, using the Mathematical
+Components library.")
+    (home-page "https://math-comp.github.io/")
+    (license license:cecill-c)))
-- 
2.37.2




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

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


Received: (at 57540) by debbugs.gnu.org; 2 Sep 2022 15:28:25 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Fri Sep 02 11:28:25 2022
Received: from localhost ([127.0.0.1]:47479 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1oU8am-00083U-Qn
	for submit <at> debbugs.gnu.org; Fri, 02 Sep 2022 11:28:25 -0400
Received: from knopi.disroot.org ([178.21.23.139]:59054)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <garekdyszel@HIDDEN>) id 1oU8ak-00083L-8f
 for 57540 <at> debbugs.gnu.org; Fri, 02 Sep 2022 11:28:22 -0400
Received: from localhost (localhost [127.0.0.1])
 by disroot.org (Postfix) with ESMTP id C4FD240053
 for <57540 <at> debbugs.gnu.org>; Fri,  2 Sep 2022 17:28:21 +0200 (CEST)
X-Virus-Scanned: SPAM Filter at disroot.org
Received: from knopi.disroot.org ([127.0.0.1])
 by localhost (disroot.org [127.0.0.1]) (amavisd-new, port 10024)
 with UTF8SMTP id gcsrljN6yZkg for <57540 <at> debbugs.gnu.org>;
 Fri,  2 Sep 2022 17:28:20 +0200 (CEST)
Mime-Version: 1.0
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=disroot.org; s=mail;
 t=1662132292; bh=eOmf6HrQlOfB/0lGpMEl7LvT4fRHfyvr0KesZbTjhpA=;
 h=Date:From:To:Subject;
 b=iDLXCgIAdi8+jELGyG2LSEHdxH1/fK+WQOgz4je65mxyt3vAmgNUt+AiEh9/UpUAa
 +IqmM1kS43oknzDfQucYa44Q5p4pASPEUN4fxK7EAvsmMjFIWyDDS9mYhwZO9WKlJx
 3bO8yjtcP45aP1/47GztDwNyxSqj5o8ie+TGjmEOIxJpDD2RDgakVxJVHJ4Hn/p/Am
 6G2BU3K5SDFVFlzCL+Mi+FjiL4BbM0lOltuAHHQjy1UFkX9zdRpUW36tX3scWq1bmU
 ocmX7BihDZ0ej+HbpwcWzDaKXM1UOIONH2IDEYbK46CUdphNzq3IGoS5jcNTFwaCSa
 IxcSG9rBuZYBw==
Date: Fri, 02 Sep 2022 11:24:52 -0400
From: Garek Dyszel <garekdyszel@HIDDEN>
To: 57540 <at> debbugs.gnu.org
Subject: [PATCH 5/6] gnu: Add coq-mathcomp-finmap.
Message-ID: <d078c5f6e7a20b07c0867acad0d944b7@HIDDEN>
X-Sender: garekdyszel@HIDDEN
Content-Type: text/plain; charset=US-ASCII;
 format=flowed
Content-Transfer-Encoding: 7bit
X-Spam-Score: 0.0 (/)
X-Debbugs-Envelope-To: 57540
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-mathcomp-finmap)
---
  gnu/packages/coq.scm | 35 +++++++++++++++++++++++++++++++++++
  1 file changed, 35 insertions(+)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index bb4788a..f0aa233 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -834,3 +834,38 @@ (define-public coq-mathcomp-hierarchy-builder
      (home-page "https://math-comp.github.io/")
      ;; MIT license
      (license license:expat)))
+
+(define-public coq-mathcomp-finmap
+  (package
+    (name "coq-mathcomp-finmap")
+    (version "1.5.2")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://github.com/math-comp/finmap")
+                    (commit version)
+                    (recursive? #t)))
+              (file-name (git-file-name name version))
+              (sha256
+               (base32
+                
"1k72wpp15xa5ag358jl8a71gschng0bgbaqjx0l5a0in6x5adafh"))))
+    (build-system gnu-build-system)
+    (arguments
+     `( ;"No rule to make target 'check'."
+       ;; No tests supplied in Makefile.common.
+       #:tests? #f
+       #:make-flags (list (string-append "COQLIBINSTALL="
+                                         (assoc-ref %outputs "out")
+                                         "/lib/coq/user-contrib"))
+       #:phases (modify-phases %standard-phases
+                  (delete 'configure))))
+    (inputs (list coq coq-stdlib coq-mathcomp which))
+    (synopsis "Finite sets and finite types for coq-mathcomp")
+    (description
+     "This library is an extension of coq-mathcomp which supports 
finite sets
+and finite maps on choicetypes (rather than finite types).  This 
includes
+support for functions with finite support and multisets.  The library 
also
+contains a generic order and set libary, which will eventually be used 
to
+subsume notations for finite sets.")
+    (home-page "https://math-comp.github.io/")
+    (license license:cecill-b)))
-- 
2.37.2




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

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


Received: (at 57540) by debbugs.gnu.org; 2 Sep 2022 15:27:50 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Fri Sep 02 11:27:50 2022
Received: from localhost ([127.0.0.1]:47474 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1oU8aE-00082D-A6
	for submit <at> debbugs.gnu.org; Fri, 02 Sep 2022 11:27:50 -0400
Received: from knopi.disroot.org ([178.21.23.139]:50068)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <garekdyszel@HIDDEN>) id 1oU8aC-000826-Rz
 for 57540 <at> debbugs.gnu.org; Fri, 02 Sep 2022 11:27:49 -0400
Received: from localhost (localhost [127.0.0.1])
 by disroot.org (Postfix) with ESMTP id 4B0F049FE8
 for <57540 <at> debbugs.gnu.org>; Fri,  2 Sep 2022 17:27:48 +0200 (CEST)
X-Virus-Scanned: SPAM Filter at disroot.org
Received: from knopi.disroot.org ([127.0.0.1])
 by localhost (disroot.org [127.0.0.1]) (amavisd-new, port 10024)
 with UTF8SMTP id vUu1_jsXEIiR for <57540 <at> debbugs.gnu.org>;
 Fri,  2 Sep 2022 17:27:46 +0200 (CEST)
Mime-Version: 1.0
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=disroot.org; s=mail;
 t=1662132244; bh=bKftHjB2e8g573GX22ID6KFy+TVloCkAjNKhbXNj40M=;
 h=Date:From:To:Subject;
 b=YbmsRi6jzabmwD8G73KI/2Boym6ts4hcInmNklRpe0Jptc9ZKidC8mK/zu/zS8lY/
 zM+j9tEXfy1XHlE44idcICSF0JWMs5cMnNpIJm6544+qxL+PxRJkoCTF1/abubFm1K
 kAEgVc/7e6c94i/0Eq7vsdT9Lq8tXwmqjnCGahPQd5uLOE4kgQgFe+aLhYukpncV29
 wLnYxHonSflhgp4bTM11hKy80CneCHwUrtc1g4fsv21XF2fwlBg6Rymeq8CQQ7d0rp
 CnE7yyWjK5isCL6wXAnQwbOheOwHF3r6qVjEYPPqm+ICs4wUlpuNRnsYiYUZIyK6Zx
 WdL8PHllumDYA==
Date: Fri, 02 Sep 2022 11:24:04 -0400
From: Garek Dyszel <garekdyszel@HIDDEN>
To: 57540 <at> debbugs.gnu.org
Subject: [PATCH 4/6] gnu: Add coq-mathcomp-hierarchy-builder.
Message-ID: <1729554f0ccf90383607cbbcf1be7323@HIDDEN>
X-Sender: garekdyszel@HIDDEN
Content-Type: text/plain; charset=US-ASCII;
 format=flowed
Content-Transfer-Encoding: 7bit
X-Spam-Score: 0.0 (/)
X-Debbugs-Envelope-To: 57540
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-mathcomp-hierarchy-builder)
---
  gnu/packages/coq.scm | 75 ++++++++++++++++++++++++++++++++++++++++++++
  1 file changed, 75 insertions(+)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 5a37432..bb4788a 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -759,3 +759,78 @@ (define-public coq-elpi
  notation.  Finally it provides a way to define new vernacular commands
  and new tactics.")
      (license license:lgpl2.1)))
+
+(define-public coq-mathcomp-hierarchy-builder
+  (package
+    (name "coq-mathcomp-hierarchy-builder")
+    ;; For more information on which version works with Coq 8.15,
+    ;; see the relevant issue:
+    ;; https://github.com/math-comp/hierarchy-builder/issues/297
+    ;; Here we use
+    ;; coq-elpi 1.14.0 + ocaml-elpi 1.15.2 +
+    ;; coq-mathcomp-hierarchy-builder 1.3.0 (Coq 8.15)
+    (version "1.3.0")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url 
"https://github.com/math-comp/hierarchy-builder")
+                    (commit (string-append "v" version))
+                    (recursive? #t)))
+              (file-name (git-file-name name version))
+              (sha256
+               (base32
+                
"17k7rlxdx43qda6i1yafpgc64na8br285cb0mbxy5wryafcdrkrc"))))
+    (build-system gnu-build-system)
+    (arguments
+     `(#:make-flags ,#~(list (string-append "COQBIN="
+                                            #$(this-package-input 
"coq-core")
+                                            "/bin/")
+                             (string-append "COQBININSTALL="
+                                            (assoc-ref %outputs "out") 
"/bin/")
+                             (string-append "DESTDIR="
+                                            (assoc-ref %outputs "out"))
+                             (string-append "ELPIDIR="
+                                            #$(this-package-input 
"ocaml-elpi")
+                                            "/lib/ocaml/site-lib/elpi")
+                             (string-append "COQMF_COQLIB="
+                                            (assoc-ref %outputs "out")
+                                            "/lib/ocaml/site-lib/coq")
+                             (string-append "COQLIBINSTALL="
+                                            (assoc-ref %outputs "out")
+                                            "/lib/coq/user-contrib"))
+       #:phases (modify-phases %standard-phases
+                  (delete 'configure)
+                  (replace 'build
+                    (lambda* (#:key make-flags #:allow-other-keys)
+                      (apply invoke "make" "build" make-flags)))
+                  (replace 'check
+                    (lambda* (#:key tests? make-flags 
#:allow-other-keys)
+                      (when tests?
+                        (apply invoke "make" "test-suite" 
make-flags)))))))
+    (inputs (list coq
+                  coq-core
+                  coq-mathcomp
+                  which
+                  ocaml
+                  coq-elpi-1.14
+                  ocaml-elpi-1.15))
+    (synopsis "Hierarchy structures for the Coq proof assistant")
+    (description
+     "Hierarchy Builder (HB) provides high level commands to declare a
+hierarchy of algebraic structure (or interfaces if you prefer the
+glossary of computer science) for the Coq system.
+
+Given a structure one can develop its theory, and that theory becomes
+automatically applicable to all the examples of the structure.  One can
+also declare alternative interfaces, for convenience or backward
+compatibility, and provide glue code linking these interfaces to the
+structures part of the hierarchy.
+
+HB commands compile down to Coq modules, sections, records, coercions,
+canonical structure instances and notations following the packed
+classes discipline which is at the core of the Mathematical Components
+library.  All that complexity is hidden behind a few concepts and a few
+declarative Coq commands.")
+    (home-page "https://math-comp.github.io/")
+    ;; MIT license
+    (license license:expat)))
-- 
2.37.2




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

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


Received: (at 57540) by debbugs.gnu.org; 2 Sep 2022 15:27:06 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Fri Sep 02 11:27:06 2022
Received: from localhost ([127.0.0.1]:47470 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1oU8ZV-00080k-RA
	for submit <at> debbugs.gnu.org; Fri, 02 Sep 2022 11:27:06 -0400
Received: from knopi.disroot.org ([178.21.23.139]:38318)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <garekdyszel@HIDDEN>) id 1oU8ZT-00080b-TM
 for 57540 <at> debbugs.gnu.org; Fri, 02 Sep 2022 11:27:04 -0400
Received: from localhost (localhost [127.0.0.1])
 by disroot.org (Postfix) with ESMTP id 41F324A034
 for <57540 <at> debbugs.gnu.org>; Fri,  2 Sep 2022 17:27:03 +0200 (CEST)
X-Virus-Scanned: SPAM Filter at disroot.org
Received: from knopi.disroot.org ([127.0.0.1])
 by localhost (disroot.org [127.0.0.1]) (amavisd-new, port 10024)
 with UTF8SMTP id Rl_crPi7tJ6y for <57540 <at> debbugs.gnu.org>;
 Fri,  2 Sep 2022 17:27:01 +0200 (CEST)
Mime-Version: 1.0
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=disroot.org; s=mail;
 t=1662132183; bh=xLsE0++1plJqBOMf1U9BiTQLH7JqPn6HbYfGMquD+js=;
 h=Date:From:To:Subject;
 b=khPyUt/ZvYkIvuYp4J/4AgchBnJ5EHuurfgGK4oTss9IIF5ThGbJOOq6CYLkxGlbs
 BbWIn0nh0wQNSiSPeL6wvBApRiPpirNsO4QJEo+yzLqSWMlcbKFBwXP20NOdKdE5LA
 jPnfclY9zJhJ6zXp0vUgmEfme7hSosw0sZ2TYJN99zyn6TQy0hxFEyy5Tx1QmsCYDs
 rtrTCxImLRJA7nr4+BeTuSZzgQp3PQCUG9xan4stIRgmThyWTs+gSkz/20J3QA61QS
 TuWxgwMuRTtlhkMRIjLAmlKgS7McxGDwoo6iHFvUUkD2l5QMirJNzE6f/WsKW/onkp
 antAomnzuhrJA==
Date: Fri, 02 Sep 2022 11:23:02 -0400
From: Garek Dyszel <garekdyszel@HIDDEN>
To: 57540 <at> debbugs.gnu.org
Subject: [PATCH 3/6] gnu: Add coq-elpi.
Message-ID: <3f2ba54de977b831ef53b6903ccf931f@HIDDEN>
X-Sender: garekdyszel@HIDDEN
Content-Type: text/plain; charset=UTF-8;
 format=flowed
Content-Transfer-Encoding: 8bit
X-Spam-Score: 0.0 (/)
X-Debbugs-Envelope-To: 57540
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-elpi)
---
  gnu/packages/coq.scm | 74 ++++++++++++++++++++++++++++++++++++++++++++
  1 file changed, 74 insertions(+)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index bbb34df..5a37432 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -685,3 +685,77 @@ (define-public coq-stdpp
  @end itemize")
      (home-page "https://gitlab.mpi-sws.org/iris/stdpp")
      (license license:bsd-3)))
+
+(define-public coq-elpi
+  (package
+    (name "coq-elpi")
+    ;; For more information on which version works with Coq 8.15,
+    ;; see the relevant issue:
+    ;; https://github.com/math-comp/hierarchy-builder/issues/297
+    ;; Here we use
+    ;; coq-elpi 1.14.0 + ocaml-elpi 1.15.2 +
+    ;; coq-mathcomp-hierarchy-builder 1.3.0 (Coq 8.15)
+    (version "1.14.0")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://github.com/LPCIC/coq-elpi")
+                    (commit (string-append "v" version))
+                    (recursive? #t)))
+              (file-name (git-file-name name version))
+              (sha256
+               (base32
+                
"1v2p5dlpviwzky2i14cj7gcgf8cr0j54bdm9fl5iz1ckx60j6nvp"))))
+    (build-system gnu-build-system)
+    (arguments
+     `(#:make-flags ,#~(list (string-append "COQBIN="
+                                            #$(this-package-input 
"coq-core")
+                                            "/bin/")
+                             (string-append "ELPIDIR="
+                                            #$(this-package-input 
"ocaml-elpi")
+                                            "/lib/ocaml/site-lib/elpi")
+                             (string-append "COQMF_COQLIB="
+                                            (assoc-ref %outputs "out")
+                                            "/lib/ocaml/site-lib/coq")
+                             (string-append "COQLIBINSTALL="
+                                            (assoc-ref %outputs "out")
+                                            "/lib/coq/user-contrib"))
+
+       #:phases (modify-phases %standard-phases
+                  (delete 'configure)
+                  (add-before 'build 'remove-extra-src-file
+                    (lambda* (#:key outputs #:allow-other-keys)
+                      ;; Remove the useless line
+                      ;; "src/META.coq-elpi"
+                      ;; in file _CoqProject.
+                      ;; It does not affect
+                      ;; the success of compliation.
+                      (invoke "sed" "-i" "s|src/META.coq-elpi||g"
+                              "_CoqProject")
+                      #t))
+                  (replace 'check
+                    (lambda* (#:key tests? make-flags 
#:allow-other-keys)
+                      (when tests?
+                        (apply invoke "make" "test" make-flags)))))))
+    (inputs (list python))
+    (propagated-inputs (list ocaml
+                             ocaml-stdlib-shims
+                             ocaml-elpi-1.15
+                             ocaml-zarith
+                             coq-core
+                             coq-stdlib))
+    (home-page "https://github.com/LPCIC/coq-elpi")
+    (synopsis "Elpi extension language for Coq")
+    (description
+     "Coq-elpi provides a Coq plugin that embeds ELPI.  It also 
provides
+a way to embed Coq's terms into λProlog using the Higher-Order
+Abstract Syntax approach and a way to read terms back.  In addition to
+that it exports to ELPI a set of Coq's primitives, e.g.  printing a
+message, accessing the environment of theorems and data types,
+defining a new constant and so on.  For convenience it also provides a
+quotation and anti-quotation for Coq's syntax in λProlog.  E.g.
+`{{nat}}` is expanded to the type name of natural numbers, or `{{A ->
+B}}` to the representation of a product by unfolding the `->`
+notation.  Finally it provides a way to define new vernacular commands
+and new tactics.")
+    (license license:lgpl2.1)))
-- 
2.37.2




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

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


Received: (at 57540) by debbugs.gnu.org; 2 Sep 2022 15:26:15 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Fri Sep 02 11:26:15 2022
Received: from localhost ([127.0.0.1]:47466 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1oU8Yh-0007zI-Dp
	for submit <at> debbugs.gnu.org; Fri, 02 Sep 2022 11:26:15 -0400
Received: from knopi.disroot.org ([178.21.23.139]:53302)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <garekdyszel@HIDDEN>) id 1oU8Yf-0007z9-Sg
 for 57540 <at> debbugs.gnu.org; Fri, 02 Sep 2022 11:26:14 -0400
Received: from localhost (localhost [127.0.0.1])
 by disroot.org (Postfix) with ESMTP id 3ADF94A034
 for <57540 <at> debbugs.gnu.org>; Fri,  2 Sep 2022 17:26:13 +0200 (CEST)
X-Virus-Scanned: SPAM Filter at disroot.org
Received: from knopi.disroot.org ([127.0.0.1])
 by localhost (disroot.org [127.0.0.1]) (amavisd-new, port 10024)
 with UTF8SMTP id PLVtr_3yA-2I for <57540 <at> debbugs.gnu.org>;
 Fri,  2 Sep 2022 17:26:11 +0200 (CEST)
Mime-Version: 1.0
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=disroot.org; s=mail;
 t=1662132123; bh=9gXcLFsmbbrJHOZiMRQPAjFQfPnORXE80LTa6Yd+CEg=;
 h=Date:From:To:Subject;
 b=I7Clv87kcPOU+MMXv19C1PuSj018Uq4a90tYOvr13nxpgN43L8G1LSxY586GvKJMq
 ftFV+yvW1wb/Ses8dSOO+9khWDeA66yhFLgi4JJMA/8gIekN4J39G5WZFHJ9OruRTH
 yEnu9FvgK58XYyMvwpGq3rVs+wXiQgUuZrQ2Uq+eCivl/zOmVDwbjSg+j1K5P3GZ5W
 b1JlgyLw5KfKT332fBhohr5tUyuSnu4Mu8bD5Y2X+0OLEt2WJSPFBZtKoVGKfGab9b
 Zm3rBEmfxXJQ2dVHQhBF9RdGYNLw2KKwKhbIKvxTBaKpQ/unDS3ee2e6RDYfDzdVm4
 9ZBsChjNB/nTQ==
Date: Fri, 02 Sep 2022 11:22:03 -0400
From: Garek Dyszel <garekdyszel@HIDDEN>
To: 57540 <at> debbugs.gnu.org
Subject: [PATCH 2/6] gnu: Add ocaml-ansiterminal.
Message-ID: <a9069e2695c4720f38fb898ac58bb11a@HIDDEN>
X-Sender: garekdyszel@HIDDEN
Content-Type: text/plain; charset=US-ASCII;
 format=flowed
Content-Transfer-Encoding: 7bit
X-Spam-Score: 0.0 (/)
X-Debbugs-Envelope-To: 57540
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/ocaml.scm (ocaml-ansiterminal)
---
  gnu/packages/ocaml.scm | 31 +++++++++++++++++++++++++++++++
  1 file changed, 31 insertions(+)

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index c8ffef5..43c19c0 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -8878,3 +8878,34 @@ (define-public ocaml-atd
  good fit with a variety of data formats.")
      ;; Modified BSD license
      (license (license:non-copyleft "LICENSE.md"))))
+
+(define-public ocaml-ansiterminal
+  (package
+    (name "ocaml-ansiterminal")
+    (version "0.8.5")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://github.com/Chris00/ANSITerminal")
+                    (commit version)
+                    (recursive? #t)))
+              (file-name (git-file-name name version))
+              (sha256
+               (base32
+                
"052qnc23vmxp90yympjz9q6lhqw98gs1yvb3r15kcbi1j678l51h"))))
+    (build-system dune-build-system)
+    (arguments
+     `( ;Error: Don't know about directory test specified on the
+       ;; command line!
+       #:tests? #f))
+    (home-page "https://github.com/Chris00/ANSITerminal")
+    (synopsis
+     "Basic control of ANSI compliant terminals and the windows shell")
+    (description
+     "ANSITerminal is a module allowing to use the colors and cursor
+movements on ANSI terminals.")
+    ;; Variant of the GPL3 which permits
+    ;; static and dynamic linking when producing binary files.
+    ;; In other words, it allows one to link to the library
+    ;; when compiling nonfree software.
+    (license (license:non-copyleft "LICENSE"))))
-- 
2.37.2




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

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


Received: (at 57540) by debbugs.gnu.org; 2 Sep 2022 15:24:43 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Fri Sep 02 11:24:43 2022
Received: from localhost ([127.0.0.1]:47462 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1oU8XC-0007wS-WF
	for submit <at> debbugs.gnu.org; Fri, 02 Sep 2022 11:24:43 -0400
Received: from knopi.disroot.org ([178.21.23.139]:58560)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <garekdyszel@HIDDEN>) id 1oU8XA-0007wI-Pf
 for 57540 <at> debbugs.gnu.org; Fri, 02 Sep 2022 11:24:41 -0400
Received: from localhost (localhost [127.0.0.1])
 by disroot.org (Postfix) with ESMTP id A4BAB4A003
 for <57540 <at> debbugs.gnu.org>; Fri,  2 Sep 2022 17:24:38 +0200 (CEST)
X-Virus-Scanned: SPAM Filter at disroot.org
Received: from knopi.disroot.org ([127.0.0.1])
 by localhost (disroot.org [127.0.0.1]) (amavisd-new, port 10024)
 with UTF8SMTP id to9GYjdDdmek for <57540 <at> debbugs.gnu.org>;
 Fri,  2 Sep 2022 17:24:37 +0200 (CEST)
Mime-Version: 1.0
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=disroot.org; s=mail;
 t=1662132016; bh=0fGSc3mViFS0zq+YTDeCrYII5Ga01LXKBrnpKDNms/8=;
 h=Date:From:To:Subject;
 b=OMl/unqGRiPZtQvt6cwu2V/waMI55ZVzgY4S906CkzG/bkNTxPH5K4aJLj6oDs4V5
 Jev44PSgs1ZMhMNSVZXzBWTZePGnITBsXOQ+XaRMlFREO1iCrxMy4Ois10JH/DaQap
 R49LlTEdqpZ+NxP4ta8zVmhgNEryz1JEXBWmGjYVem0S9Cqh1T7bOHRDRZAcvLVCdY
 tAQeVFiLbZnfGewqaxGkZ8xQ86tNNWCkxI47D0midJkjKQnEeikQOkO42+myqKhSpi
 6noQGcpXU8+7B5ll+nvTbWsTr0JME8T2tpexw9+9VShfYl0iB9bghcx5Id+mi/nGjy
 l062tuaesFJ+A==
Date: Fri, 02 Sep 2022 11:20:15 -0400
From: Garek Dyszel <garekdyszel@HIDDEN>
To: 57540 <at> debbugs.gnu.org
Subject: [PATCH 1/6] gnu: Add ocaml-atd.
Message-ID: <608b4f6bdcbd56e28ba9ab0c34401790@HIDDEN>
X-Sender: garekdyszel@HIDDEN
Content-Type: text/plain; charset=US-ASCII;
 format=flowed
Content-Transfer-Encoding: 7bit
X-Spam-Score: 0.0 (/)
X-Debbugs-Envelope-To: 57540
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/ocaml.scm (ocaml-atd)
---
  gnu/packages/ocaml.scm | 35 +++++++++++++++++++++++++++++++++++
  1 file changed, 35 insertions(+)

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index 59f324e..c8ffef5 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -8843,3 +8843,38 @@ (define-public ocaml-elpi
  ELPI is free software released under the terms of LGPL 2.1 or above.")
      (license license:lgpl2.1)))

+(define-public ocaml-atd
+  (package
+    (name "ocaml-atd")
+    (version "2.10.0")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append
+                    "https://github.com/ahrefs/atd/releases/download/" 
version
+                    "/atdts-" version ".tbz"))
+              (sha256
+               (base32
+                
"1609hlj2snpvxnmmg892ic01hv3chdhfmsd2khdw9np9lh4p9lkp"))))
+    (build-system dune-build-system)
+    (arguments
+     `(;; Error: Don't know about directory test specified on the 
command line!
+       #:tests? #f))
+    (propagated-inputs (list ocaml-menhir
+                             ocaml-easy-format
+                             ocaml-odoc
+                             ocaml-re
+                             ocaml-camlp-streams
+                             ocaml-biniou
+                             ocaml-yojson
+                             ocaml-cmdliner
+                             ocaml-menhir))
+    (native-inputs (list ocaml-alcotest python))
+    (home-page "https://github.com/ahrefs/atd")
+    (synopsis "Parser for the ATD data format description language")
+    (description
+     "ATD is the OCaml library providing a parser for the ATD language
+and various utilities.  ATD stands for Adjustable Type Definitions in
+reference to its main property of supporting annotations that allow a
+good fit with a variety of data formats.")
+    ;; Modified BSD license
+    (license (license:non-copyleft "LICENSE.md"))))
--
2.37.2




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

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


Received: (at submit) by debbugs.gnu.org; 2 Sep 2022 07:45:48 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Fri Sep 02 03:45:47 2022
Received: from localhost ([127.0.0.1]:44732 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1oU1N5-0000Nm-3t
	for submit <at> debbugs.gnu.org; Fri, 02 Sep 2022 03:45:47 -0400
Received: from lists.gnu.org ([209.51.188.17]:41928)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <garekdyszel@HIDDEN>) id 1oTvjG-0007sr-Og
 for submit <at> debbugs.gnu.org; Thu, 01 Sep 2022 21:44:19 -0400
Received: from eggs.gnu.org ([2001:470:142:3::10]:53006)
 by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
 (Exim 4.90_1) (envelope-from <garekdyszel@HIDDEN>)
 id 1oTvjG-00070R-9d
 for guix-patches@HIDDEN; Thu, 01 Sep 2022 21:44:18 -0400
Received: from knopi.disroot.org ([178.21.23.139]:60448)
 by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
 (Exim 4.90_1) (envelope-from <garekdyszel@HIDDEN>)
 id 1oTvjD-0006Z0-O8
 for guix-patches@HIDDEN; Thu, 01 Sep 2022 21:44:17 -0400
Received: from localhost (localhost [127.0.0.1])
 by disroot.org (Postfix) with ESMTP id 7C4B5400BC
 for <guix-patches@HIDDEN>; Fri,  2 Sep 2022 03:44:11 +0200 (CEST)
X-Virus-Scanned: SPAM Filter at disroot.org
Received: from knopi.disroot.org ([127.0.0.1])
 by localhost (disroot.org [127.0.0.1]) (amavisd-new, port 10024)
 with ESMTP id CdVu1qa7V649 for <guix-patches@HIDDEN>;
 Fri,  2 Sep 2022 03:44:10 +0200 (CEST)
Mime-Version: 1.0
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=disroot.org; s=mail;
 t=1662083050; bh=YwI38aXsDNkkIqbBSarHFVS5YPZZVoaoZ935ISWILxA=;
 h=Date:From:To:Subject;
 b=H+LoIhOJhftOAhsd8lPo7i/QsvFAAR2zQugFnNCC8XXsZn21hs29yn/3B3US+1rxm
 B+qWxUolVOKVviwai0WIP62vVG9GM2bx8vsMx9TOFBxuvUpQKkTEBai6ZAiQtTMeOU
 qP9gLc95ejB0ozd1mxzN/AD29woX26qL7WlGII8WEB1jaWLlJe3XIJnsU2ilu0fnW6
 kjnjTnICqfblU9ipu3AMEoDdJI0ZhK4mxu4VTx7SMMzeCwah/dnGJUha0joWTtuQlj
 nPOjuXeoiONhg4P9hGESnW2JoUCrpsIp2hr6AjaywMwTf8Zv5qD7xSrun6xIbZZwv7
 2DIbVjoikwqGw==
Date: Thu, 01 Sep 2022 21:44:09 -0400
From: Garek Dyszel <garekdyszel@HIDDEN>
To: guix-patches@HIDDEN
Subject: [PATCH] Add ocaml-elpi (a dependency of coq-mathcomp-analysis)
Message-ID: <79d544f7d8ba64b631a6f0f1d2ef0b08@HIDDEN>
X-Sender: garekdyszel@HIDDEN
Content-Type: text/plain; charset=UTF-8;
 format=flowed
Content-Transfer-Encoding: 8bit
Received-SPF: pass client-ip=178.21.23.139;
 envelope-from=garekdyszel@HIDDEN; helo=knopi.disroot.org
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_NONE=0.001,
 SPF_PASS=-0.001, T_SCC_BODY_TEXT_LINE=-0.01 autolearn=ham autolearn_force=no
X-Spam_action: no action
X-Spam-Score: -1.4 (-)
X-Debbugs-Envelope-To: submit
X-Mailman-Approved-At: Fri, 02 Sep 2022 03:45:45 -0400
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 (--)

* gnu/packages/ocaml.scm (ocaml-elpi)
---
  gnu/packages/ocaml.scm | 102 +++++++++++++++++++++++++++++++++++++++++
  1 file changed, 102 insertions(+)

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index 0e8e5b2..59f324e 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -26,6 +26,7 @@
  ;;; Copyright © 2021 Sarah Morgensen <iskarian@HIDDEN>
  ;;; Copyright © 2022 Maxim Cournoyer <maxim.cournoyer@HIDDEN>
  ;;; Copyright © 2022 John Kehayias <john.kehayias@HIDDEN>
+;;; Copyright © 2022 Garek Dyszel <garekdyszel@HIDDEN>
  ;;;
  ;;; This file is part of GNU Guix.
  ;;;
@@ -8741,3 +8742,104 @@ (define-public ocaml-bibtex2html
      (description "This package allows you to produce, from a set of
  bibliography files in BibTeX format, a bibliography in HTML format.")
      (license license:gpl2)))
+
+(define-public ocaml-elpi
+  (package
+    (name "ocaml-elpi")
+    ;; For more information on which version works with Coq 8.15,
+    ;; see the relevant issue:
+    ;; https://github.com/math-comp/hierarchy-builder/issues/297
+    ;; Here we use
+    ;; coq-elpi 1.14.0 + ocaml-elpi 1.15.2 +
+    ;; coq-mathcomp-hierarchy-builder 1.3.0 (Coq 8.15)
+    ;;
+    ;; The package ocaml-elpi@HIDDEN appears to require a different
+    ;; build process.
+    (version "1.15.2")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://github.com/LPCIC/elpi")
+                    (commit (string-append "v" version))
+                    (recursive? #t)))
+              (file-name (git-file-name name version))
+              (sha256
+               (base32
+                
"0swzqabwrxqb6sz8zpild2lfcnk3l0zxi9fw61dy2g1pzws2j2jy"))))
+    (build-system dune-build-system)
+    (arguments
+     `(;; When running phase 'check', fails with the error:
+       ;; Error: Don't know about directory test specified on the
+       ;; command line!
+       ;;
+       ;; The "make tests" command requires replacing /usr/bin/time
+       ;; with the location of the input package "time".
+       #:tests? #f))
+    (propagated-inputs (list ocaml-stdlib-shims
+                             ocaml-ppxlib
+                             ocaml-menhir
+                             ocaml-re
+                             ocaml-ppx-deriving
+                             ocaml-atdgen
+                             ocaml-atdts
+                             ocaml-camlp-streams
+                             ocaml-biniou
+                             ocaml-yojson))
+    (native-inputs (list ocaml-ansiterminal ocaml-cmdliner time))
+    (home-page "https://github.com/LPCIC/elpi")
+    (synopsis "ELPI - Embeddable λProlog Interpreter")
+    (description
+     "ELPI implements a variant of λProlog enriched with Constraint
+Handling Rules, a programming language well suited to manipulate
+syntax trees with binders.
+
+ELPI is designed to be embedded into larger applications written in
+OCaml as an extension language.  It comes with an API to drive the
+interpreter and with an FFI for defining built-in predicates and data
+types, as well as quotations and similar goodies that are handy to
+adapt the language to the host application.
+
+This package provides both a command line interpreter (elpi) and a
+library to be linked in other applications (eg by passing -package
+elpi to ocamlfind).
+
+The ELPI programming language has the following features:
+
+- Native support for variable binding and substitution, via an Higher
+Order Abstract Syntax (HOAS) embedding of the object language.  The
+programmer does not need to care about technical devices to handle
+bound variables, like De Bruijn indices.
+
+- Native support for hypothetical context.  When moving under a binder
+one can attach to the bound variable extra information that is
+collected when the variable gets out of scope.  For example when
+writing a type-checker the programmer needs not to care about managing
+the typing context.
+
+- Native support for higher order unification variables, again via
+HOAS.  Unification variables of the meta-language (λProlog) can be
+reused to represent the unification variables of the object language.
+The programmer does not need to care about the unification-variable
+assignment map and cannot assign to a unification variable a term
+containing variables out of scope, or build a circular assignment.
+
+- Native support for syntactic constraints and their meta-level
+handling rules.  The generative semantics of Prolog can be disabled by
+turning a goal into a syntactic constraint (suspended goal).  A
+syntactic constraint is resumed as soon as relevant variables gets
+assigned.  Syntactic constraints can be manipulated by constraint
+handling rules (CHR).
+
+- Native support for backtracking.  To ease implementation of search.
+
+- The constraint store is extensible.  The host application can declare
+non-syntactic constraints and use custom constraint solvers to check
+their consistency.
+
+- Clauses are graftable.  The user is free to extend an existing
+program by inserting/removing clauses, both at runtime (using
+implication) and at \"compilation\" time by accumulating files.
+
+ELPI is free software released under the terms of LGPL 2.1 or above.")
+    (license license:lgpl2.1)))
+
-- 
2.37.2




Acknowledgement sent to Garek Dyszel <garekdyszel@HIDDEN>:
New bug report received and forwarded. Copy sent to guix-patches@HIDDEN. Full text available.
Report forwarded to guix-patches@HIDDEN:
bug#57540; 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: Sat, 24 Sep 2022 13:15:02 UTC

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