GNU bug report logs - #49423
[PATCH] gnu: coq: Update to 8.13.2.

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: Julien Lepiller <julien@HIDDEN>; Keywords: patch; dated Mon, 5 Jul 2021 22:08:02 UTC; Maintainer for guix-patches is guix-patches@HIDDEN.

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


Received: (at 49423) by debbugs.gnu.org; 24 Jul 2021 13:17:41 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Sat Jul 24 09:17:41 2021
Received: from localhost ([127.0.0.1]:45384 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1m7HXB-0007JS-3K
	for submit <at> debbugs.gnu.org; Sat, 24 Jul 2021 09:17:41 -0400
Received: from h87-96-130-155.cust.a3fiber.se ([87.96.130.155]:34060
 helo=mail.yoctocell.xyz) by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <public@HIDDEN>) id 1m7HX6-0007JB-8c
 for 49423 <at> debbugs.gnu.org; Sat, 24 Jul 2021 09:17:39 -0400
From: Xinglu Chen <public@HIDDEN>
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=yoctocell.xyz;
 s=mail; t=1627132646;
 bh=5g8Meysniokgr+/0y8Jhxz0NLb+Jn0DMdBmKJoByPQk=;
 h=From:To:Subject:In-Reply-To:References:Date;
 b=mxRwtm9THN52KFHx9sjriILhMbOelWWyjylnrrJSSzF5SAPtvUGx2tHdldWy9vqDw
 NcwQafCIEgVQh6EzNITS45yOXBLDvS3WlXELn65mwFN/2AW0QpvKqX/hXulVbliDEb
 RA2RSsKRMNpaiR8amatvHq0mXUoR+BLTy537I3Fk=
To: Julien Lepiller <julien@HIDDEN>, 49423 <at> debbugs.gnu.org
Subject: Re: [bug#49423] [PATCH] gnu: coq: Update to 8.13.2.
In-Reply-To: <20210706000640.4630e3bb@HIDDEN>
References: <20210706000640.4630e3bb@HIDDEN>
Date: Sat, 24 Jul 2021 15:17:25 +0200
Message-ID: <87lf5v3l7e.fsf@HIDDEN>
MIME-Version: 1.0
Content-Type: multipart/signed; boundary="=-=-=";
 micalg=pgp-sha256; protocol="application/pgp-signature"
X-Spam-Score: 2.9 (++)
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:  On Tue, Jul 06 2021, Julien Lepiller wrote: > Hi guix! > >
 this small series updates coq to the latest version. I had to update > zarith
 and a few dependencies (some of which cannot be updated > independently of
 coq), and fix the installation o [...] 
 Content analysis details:   (2.9 points, 10.0 required)
 pts rule name              description
 ---- ---------------------- --------------------------------------------------
 -0.0 SPF_PASS               SPF: sender matches SPF record
 2.0 PDS_OTHER_BAD_TLD      Untrustworthy TLDs
 [URI: yoctocell.xyz (xyz)]
 0.0 SPF_HELO_NONE          SPF: HELO does not publish an SPF Record
 0.5 FROM_SUSPICIOUS_NTLD   From abused NTLD
 0.4 RDNS_DYNAMIC           Delivered to internal network by host with
 dynamic-looking rDNS
 0.0 PDS_RDNS_DYNAMIC_FP    RDNS_DYNAMIC with FP steps
X-Debbugs-Envelope-To: 49423
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.9 (++)
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:  On Tue, Jul 06 2021, Julien Lepiller wrote: > Hi guix! > >
    this small series updates coq to the latest version. I had to update > zarith
    and a few dependencies (some of which cannot be updated > independently of
    coq), and fix the installation o [...] 
 
 Content analysis details:   (2.9 points, 10.0 required)
 
  pts rule name              description
 ---- ---------------------- --------------------------------------------------
 -0.0 SPF_PASS               SPF: sender matches SPF record
  2.0 PDS_OTHER_BAD_TLD      Untrustworthy TLDs
                             [URI: yoctocell.xyz (xyz)]
  0.0 SPF_HELO_NONE          SPF: HELO does not publish an SPF Record
  0.5 FROM_SUSPICIOUS_NTLD   From abused NTLD
  0.4 RDNS_DYNAMIC           Delivered to internal network by host with
                             dynamic-looking rDNS
  1.0 BULK_RE_SUSP_NTLD      Precedence bulk and RE: from a suspicious TLD
 -1.0 MAILING_LIST_MULTI     Multiple indicators imply a widely-seen list
                             manager
  0.0 PDS_RDNS_DYNAMIC_FP    RDNS_DYNAMIC with FP steps

--=-=-=
Content-Type: text/plain
Content-Transfer-Encoding: quoted-printable

On Tue, Jul 06 2021, Julien Lepiller wrote:

> Hi guix!
>
> this small series updates coq to the latest version. I had to update
> zarith and a few dependencies (some of which cannot be updated
> independently of coq), and fix the installation of lablgtk.
>
> This version of coq uses dune, and I split the coq package into coq,
> coq-ide-server (contains coqidetop) and coq-ide (contains the graphical
> interface). This also simplifies the dependency graph for coq packages,
> as they no longer need the graphical stack.
>
> I tried building the documentation too, but it complains about missing
> coq package, even if I added it to the inputs of coq-doc, so it's not
> part of this series.
> From 73fc06926c86e8dad8bbb61f6a1728343fd2a487 Mon Sep 17 00:00:00 2001
> From: Julien Lepiller <julien@HIDDEN>
> Date: Mon, 5 Jul 2021 17:31:10 +0200
> Subject: [PATCH 1/4] gnu: ocaml-zarith: Update to 1.12.
>
> * gnu/packages/ocaml.scm (ocaml-zarith): Update to 1.12.
> ---
>  gnu/packages/ocaml.scm | 13 ++++++++++---
>  1 file changed, 10 insertions(+), 3 deletions(-)
>
> diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
> index cec6eb4f89..5f4ed3ae35 100644
> --- a/gnu/packages/ocaml.scm
> +++ b/gnu/packages/ocaml.scm
> @@ -1428,7 +1428,7 @@ files in these formats.")
>  (define-public ocaml-zarith
>    (package
>      (name "ocaml-zarith")
> -    (version "1.9.1")
> +    (version "1.12")
>      (source (origin
>                (method git-fetch)
>                (uri (git-reference
> @@ -1437,7 +1437,7 @@ files in these formats.")
>                (file-name (git-file-name name version))
>                (sha256
>                 (base32
> -                "0hv5ywz1q2cgn8apfz490clwk5hcynr937g2v8i13x2ax4bnv0lz"))=
))
> +                "1jslm1rv1j0ya818yh23wf3bb6hz7qqj9pn5fwl45y9mqyqa01s9"))=
))
>      (build-system ocaml-build-system)
>      (native-inputs
>       `(("perl" ,perl)))
> @@ -1448,7 +1448,14 @@ files in these formats.")
>         #:phases
>         (modify-phases %standard-phases
>           (replace 'configure
> -           (lambda _ (invoke "./configure"))))))
> +           (lambda _ (invoke "./configure")))
> +         (add-after 'install 'move-sublibs
> +           (lambda* (#:key outputs #:allow-other-keys)
> +             (let* ((out (assoc-ref outputs "out"))
> +                    (lib (string-append out "/lib/ocaml/site-lib")))
> +               (mkdir-p (string-append lib "/stublibs"))
> +               (rename-file (string-append lib "/zarith/dllzarith.so")
> +                            (string-append lib "/stublibs/dllzarith.so")=
)))))))
>      (home-page "https://forge.ocamlcore.org/projects/zarith/")
>      (synopsis "Implements arbitrary-precision integers")
>      (description "Implements arithmetic and logical operations over
> --=20
> 2.32.0
>
> From 76a337769e67e84a32c5b85d80ab6bc160792aef Mon Sep 17 00:00:00 2001
> From: Julien Lepiller <julien@HIDDEN>
> Date: Mon, 5 Jul 2021 17:52:03 +0200
> Subject: [PATCH 2/4] gnu: lablgtk3: Install with version information.
>
> This is required so recent versions of coq can check version
> requirements.
>
> * gnu/packages/ocaml.scm (lablgtk3)[arguments]: Ensure version is added
> to the META file.
> ---
>  gnu/packages/ocaml.scm | 6 ++++++
>  1 file changed, 6 insertions(+)
>
> diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
> index 5f4ed3ae35..4c8f04f29c 100644
> --- a/gnu/packages/ocaml.scm
> +++ b/gnu/packages/ocaml.scm
> @@ -6902,6 +6902,12 @@ support for Mparser.")))
>               (for-each (lambda (file)
>                           (chmod file #o644))
>                         (find-files "." "."))
> +             #t))

Nit: no need to add a trailing #t.

> +         (add-before 'build 'set-version
> +           (lambda _
> +             (substitute* "dune-project"
> +               (("\\(name lablgtk3\\)")
> +                (string-append "(name lablgtk3)\n(version " ,version ")"=
)))
>               #t)))))

Likewise.

Otherwise, looks good; everything builds fine.  :)

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

-----BEGIN PGP SIGNATURE-----

iQJJBAEBCAAzFiEEAVhh4yyK5+SEykIzrPUJmaL7XHkFAmD8EuUVHHB1YmxpY0B5
b2N0b2NlbGwueHl6AAoJEKz1CZmi+1x5eQoP/3iNFFmYkKxO0IlSYjzgElx/AhTl
yXteOJSI6aV3YTJ8FbjwnYBEtYyEQ3CPCf3kGFpg0B3iXGheqkgtAy3SmnEPQygw
dM5qu5HU/IAcK/hwWSvji04STwCtpRBj1Dhe06LM+5Mb3kQScHAIGkrfANRlG9qe
QbCI7t87jVQaKCFJrInB04StAErEYMy4tTFI4xT33IOoWCx5b5n45LX72g5kmSRo
xewKamw0cUkWJry4fKDs9Out1OzoCekqISkusELm5tqdBNgeUNFcduRgVas3pyaS
6B5HFbqE+6RIcEJVXG8qzi142wQH3bf+N/dawPXxPL1qSBwhLlp4FNR9+5Wx2Ad/
mH9HDohYiHh15wOjkKjwP+ZJCV3EdfK6DflsFToFJQQSNjQ1BzRdkLg9rMIWwvaR
QkBSiG/o1XRWmcDtYHHvxncNz2S1TUfGrlR95BhesVDMxVy0I7wFY0zanrKvBue2
U7+lMVQP+/nZFF9AgrfB9lflx4EagTfT8yC+14Nj9s2IglqQIQCjAeiJ1l6mGVaZ
fxzYjy15+LsRcAOLFlTA98CZpiAcvE20vFIRdmNDlOsigdvcbGSL6M3qBDrYeQkI
X5m1BSJP1OtirhEzVBT8LZGdqw+NcfFZnOVB2ZRLp7EsvqQA9FTw7pOIklxSOQ1v
CgZs7dAHUtYmJxkK
=0CHK
-----END PGP SIGNATURE-----
--=-=-=--




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

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


Received: (at 49423) by debbugs.gnu.org; 21 Jul 2021 14:08:03 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Wed Jul 21 10:08:02 2021
Received: from localhost ([127.0.0.1]:38166 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1m6CtG-00020Q-Ng
	for submit <at> debbugs.gnu.org; Wed, 21 Jul 2021 10:08:02 -0400
Received: from eggs.gnu.org ([209.51.188.92]:45268)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <ludo@HIDDEN>) id 1m6CtF-0001zd-4U
 for 49423 <at> debbugs.gnu.org; Wed, 21 Jul 2021 10:08:01 -0400
Received: from fencepost.gnu.org ([2001:470:142:3::e]:48834)
 by eggs.gnu.org with esmtp (Exim 4.90_1)
 (envelope-from <ludo@HIDDEN>)
 id 1m6Ct9-0000vH-1w; Wed, 21 Jul 2021 10:07:55 -0400
Received: from [2a01:e0a:1d:7270:af76:b9b:ca24:c465] (port=45264 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 1m6Ct8-0000i0-Qh; Wed, 21 Jul 2021 10:07:55 -0400
From: =?utf-8?Q?Ludovic_Court=C3=A8s?= <ludo@HIDDEN>
To: Julien Lepiller <julien@HIDDEN>
Subject: Re: bug#49423: [PATCH] gnu: coq: Update to 8.13.2.
References: <20210706000640.4630e3bb@HIDDEN>
Date: Wed, 21 Jul 2021 16:07:53 +0200
In-Reply-To: <20210706000640.4630e3bb@HIDDEN> (Julien
 Lepiller's message of "Tue, 6 Jul 2021 00:06:40 +0200")
Message-ID: <87lf5zhi9y.fsf@HIDDEN>
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/27.2 (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: 49423
Cc: 49423 <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 Lepiller <julien@HIDDEN> skribis:

> this small series updates coq to the latest version. I had to update
> zarith and a few dependencies (some of which cannot be updated
> independently of coq), and fix the installation of lablgtk.

I haven=E2=80=99t tested it but the whole series LGTM!

Thanks,
Ludo=E2=80=99.




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

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


Received: (at submit) by debbugs.gnu.org; 5 Jul 2021 22:07:05 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Mon Jul 05 18:07:05 2021
Received: from localhost ([127.0.0.1]:46787 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1m0Wjy-0001lq-02
	for submit <at> debbugs.gnu.org; Mon, 05 Jul 2021 18:07:05 -0400
Received: from lists.gnu.org ([209.51.188.17]:54844)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <julien@HIDDEN>) id 1m0Wjv-0001lh-Ir
 for submit <at> debbugs.gnu.org; Mon, 05 Jul 2021 18:06:56 -0400
Received: from eggs.gnu.org ([2001:470:142:3::10]:53622)
 by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
 (Exim 4.90_1) (envelope-from <julien@HIDDEN>)
 id 1m0Wjv-0006v1-Cd
 for guix-patches@HIDDEN; Mon, 05 Jul 2021 18:06:55 -0400
Received: from lepiller.eu ([2a00:5884:8208::1]:38686)
 by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
 (Exim 4.90_1) (envelope-from <julien@HIDDEN>)
 id 1m0Wjr-0000Kn-5e
 for guix-patches@HIDDEN; Mon, 05 Jul 2021 18:06:54 -0400
Received: from lepiller.eu (localhost [127.0.0.1])
 by lepiller.eu (OpenSMTPD) with ESMTP id 4c909d06
 for <guix-patches@HIDDEN>; Mon, 5 Jul 2021 22:06:44 +0000 (UTC)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed; d=lepiller.eu; h=date:from
 :to:subject:message-id:mime-version:content-type; s=dkim; bh=fhE
 10fzac3PVbJUvfvMdyN9ksEFV0sY7pk5rSvn2Ij4=; b=MS8B8Hzo+y5W6rdmmdM
 Av+oLAy6Uri5mXIAjAFdCaoEZb9zxXgvL2JmkpGku+/vYXwJT3XL2Q4Tny2Vw40u
 zj290+fn1l+MyQiDBZNgN8JQ4obwQdjLvWRL3wmqkUBG0wE79qihC5ZBuLisWBUz
 DAC0XWP+a3XDQGXQuLF62eGXqfNszVzi6HB9zIOIaP+3bUUJT9Rl5KTuhmRl34t5
 5503xIoL5vKj6/9nQHw/aACeWYpwfPS/tfga0ciLtHIyMMDQFnFL1ox8tTjAI3Wg
 /fEagYh3EyPeY+sMDeD+mjlvw0Mvcl3X/Z5AdbEptpy+XJ4Gi/ZKBc9ly3XReo/l
 eCQ==
Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id cbac0aa7
 (TLSv1.2:ECDHE-RSA-AES256-GCM-SHA384:256:NO)
 for <guix-patches@HIDDEN>; Mon, 5 Jul 2021 22:06:44 +0000 (UTC)
Date: Tue, 6 Jul 2021 00:06:40 +0200
From: Julien Lepiller <julien@HIDDEN>
To: guix-patches@HIDDEN
Subject: [PATCH] gnu: coq: Update to 8.13.2.
Message-ID: <20210706000640.4630e3bb@HIDDEN>
X-Mailer: Claws Mail 3.17.8 (GTK+ 2.24.32; x86_64-pc-linux-gnu)
MIME-Version: 1.0
Content-Type: multipart/mixed; boundary="MP_/jGUdlqUdtTBeoke1qO/tY2U"
Received-SPF: pass client-ip=2a00:5884:8208::1;
 envelope-from=julien@HIDDEN; helo=lepiller.eu
X-Spam_score_int: -20
X-Spam_score: -2.1
X-Spam_bar: --
X-Spam_report: (-2.1 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1,
 DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, SPF_HELO_PASS=-0.001,
 SPF_PASS=-0.001 autolearn=ham autolearn_force=no
X-Spam_action: no action
X-Spam-Score: -1.3 (-)
X-Debbugs-Envelope-To: submit
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -0.0 (/)

--MP_/jGUdlqUdtTBeoke1qO/tY2U
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Content-Disposition: inline

Hi guix!

this small series updates coq to the latest version. I had to update
zarith and a few dependencies (some of which cannot be updated
independently of coq), and fix the installation of lablgtk.

This version of coq uses dune, and I split the coq package into coq,
coq-ide-server (contains coqidetop) and coq-ide (contains the graphical
interface). This also simplifies the dependency graph for coq packages,
as they no longer need the graphical stack.

I tried building the documentation too, but it complains about missing
coq package, even if I added it to the inputs of coq-doc, so it's not
part of this series.

--MP_/jGUdlqUdtTBeoke1qO/tY2U
Content-Type: text/x-patch
Content-Transfer-Encoding: 7bit
Content-Disposition: attachment;
 filename=0001-gnu-ocaml-zarith-Update-to-1.12.patch

From 73fc06926c86e8dad8bbb61f6a1728343fd2a487 Mon Sep 17 00:00:00 2001
From: Julien Lepiller <julien@HIDDEN>
Date: Mon, 5 Jul 2021 17:31:10 +0200
Subject: [PATCH 1/4] gnu: ocaml-zarith: Update to 1.12.

* gnu/packages/ocaml.scm (ocaml-zarith): Update to 1.12.
---
 gnu/packages/ocaml.scm | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index cec6eb4f89..5f4ed3ae35 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -1428,7 +1428,7 @@ files in these formats.")
 (define-public ocaml-zarith
   (package
     (name "ocaml-zarith")
-    (version "1.9.1")
+    (version "1.12")
     (source (origin
               (method git-fetch)
               (uri (git-reference
@@ -1437,7 +1437,7 @@ files in these formats.")
               (file-name (git-file-name name version))
               (sha256
                (base32
-                "0hv5ywz1q2cgn8apfz490clwk5hcynr937g2v8i13x2ax4bnv0lz"))))
+                "1jslm1rv1j0ya818yh23wf3bb6hz7qqj9pn5fwl45y9mqyqa01s9"))))
     (build-system ocaml-build-system)
     (native-inputs
      `(("perl" ,perl)))
@@ -1448,7 +1448,14 @@ files in these formats.")
        #:phases
        (modify-phases %standard-phases
          (replace 'configure
-           (lambda _ (invoke "./configure"))))))
+           (lambda _ (invoke "./configure")))
+         (add-after 'install 'move-sublibs
+           (lambda* (#:key outputs #:allow-other-keys)
+             (let* ((out (assoc-ref outputs "out"))
+                    (lib (string-append out "/lib/ocaml/site-lib")))
+               (mkdir-p (string-append lib "/stublibs"))
+               (rename-file (string-append lib "/zarith/dllzarith.so")
+                            (string-append lib "/stublibs/dllzarith.so"))))))))
     (home-page "https://forge.ocamlcore.org/projects/zarith/")
     (synopsis "Implements arbitrary-precision integers")
     (description "Implements arithmetic and logical operations over
-- 
2.32.0


--MP_/jGUdlqUdtTBeoke1qO/tY2U
Content-Type: text/x-patch
Content-Transfer-Encoding: 7bit
Content-Disposition: attachment;
 filename=0002-gnu-lablgtk3-Install-with-version-information.patch

From 76a337769e67e84a32c5b85d80ab6bc160792aef Mon Sep 17 00:00:00 2001
From: Julien Lepiller <julien@HIDDEN>
Date: Mon, 5 Jul 2021 17:52:03 +0200
Subject: [PATCH 2/4] gnu: lablgtk3: Install with version information.

This is required so recent versions of coq can check version
requirements.

* gnu/packages/ocaml.scm (lablgtk3)[arguments]: Ensure version is added
to the META file.
---
 gnu/packages/ocaml.scm | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index 5f4ed3ae35..4c8f04f29c 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -6902,6 +6902,12 @@ support for Mparser.")))
              (for-each (lambda (file)
                          (chmod file #o644))
                        (find-files "." "."))
+             #t))
+         (add-before 'build 'set-version
+           (lambda _
+             (substitute* "dune-project"
+               (("\\(name lablgtk3\\)")
+                (string-append "(name lablgtk3)\n(version " ,version ")")))
              #t)))))
     (propagated-inputs
      `(("ocaml-cairo2" ,ocaml-cairo2)))
-- 
2.32.0


--MP_/jGUdlqUdtTBeoke1qO/tY2U
Content-Type: text/x-patch
Content-Transfer-Encoding: 7bit
Content-Disposition: attachment;
 filename=0003-gnu-coq-stdpp-Update-to-1.5.0.patch

From 8f374c9e8001db83a12ef6feee8404cbef4daaab Mon Sep 17 00:00:00 2001
From: Julien Lepiller <julien@HIDDEN>
Date: Mon, 5 Jul 2021 23:41:16 +0200
Subject: [PATCH 3/4] gnu: coq-stdpp: Update to 1.5.0.

* gnu/packages/coq.scm (coq-stdpp): Update to 1.5.0.
---
 gnu/packages/coq.scm | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index fa1f4078b8..a18eddeb0f 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -598,7 +598,7 @@ kernel.")
 (define-public coq-stdpp
   (package
     (name "coq-stdpp")
-    (version "1.4.0")
+    (version "1.5.0")
     (synopsis "Alternative Coq standard library std++")
     (source (origin
               (method git-fetch)
@@ -608,7 +608,7 @@ kernel.")
               (file-name (git-file-name name version))
               (sha256
                (base32
-                "1m6c7ibwc99jd4cv14v3r327spnfvdf3x2mnq51f9rz99rffk68r"))))
+                "1ym0fy620imah89p8b6rii8clx2vmnwcrbwxl3630h24k42092nf"))))
     (build-system gnu-build-system)
     (inputs
      `(("coq" ,coq)))
-- 
2.32.0


--MP_/jGUdlqUdtTBeoke1qO/tY2U
Content-Type: text/x-patch
Content-Transfer-Encoding: quoted-printable
Content-Disposition: attachment; filename=0004-gnu-coq-Update-to-8.13.2.patch

=46rom 074a392bc2139309a39a06b03520af0573c844b1 Mon Sep 17 00:00:00 2001
From: Julien Lepiller <julien@HIDDEN>
Date: Mon, 5 Jul 2021 21:32:33 +0200
Subject: [PATCH 4/4] gnu: coq: Update to 8.13.2.

* gnu/packages/coq.scm (coq): Update to 8.13.2.
(coq-ide-server, coq-ide): New packages.
(coq-gappa): Update to 1.4.6.
(coq-bignums): Update to 8.13.0.
(coq-interval): Update to 1.3.0.
(coq-equations): Update to 1.2.4.
---
 gnu/packages/coq.scm | 147 ++++++++++++++++++-------------------------
 1 file changed, 62 insertions(+), 85 deletions(-)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index a18eddeb0f..4ad172c6b0 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -1,5 +1,5 @@
 ;;; GNU Guix --- Functional package management for GNU
-;;; Copyright =C2=A9 2018 Julien Lepiller <julien@HIDDEN>
+;;; Copyright =C2=A9 2018-2021 Julien Lepiller <julien@HIDDEN>
 ;;; Copyright =C2=A9 2018, 2019 Tobias Geerinckx-Rice <me@HIDDEN>
 ;;; Copyright =C2=A9 2019 Dan Frumin <dfrumin@HIDDEN>
 ;;; Copyright =C2=A9 2020 Brett Gilio <brettg@HIDDEN>
@@ -38,6 +38,7 @@
   #:use-module (gnu packages python)
   #:use-module (gnu packages rsync)
   #:use-module (gnu packages texinfo)
+  #:use-module (guix build-system dune)
   #:use-module (guix build-system gnu)
   #:use-module (guix build-system ocaml)
   #:use-module (guix download)
@@ -50,7 +51,7 @@
 (define-public coq
   (package
     (name "coq")
-    (version "8.11.2")
+    (version "8.13.2")
     (source
      (origin
        (method git-fetch)
@@ -60,78 +61,24 @@
        (file-name (git-file-name name version))
        (sha256
         (base32
-         "1gia82dkmzqspw2w3s4gjyh39ghbmw4i41i4hyzc91g7mza17nbz"))))
+         "15r0cm3p9dlsxbg0lf05njjp1xi1y74vxvq6drxjykax67x95l8a"))))
     (native-search-paths
      (list (search-path-specification
             (variable "COQPATH")
-            (files (list "lib/coq/user-contrib")))))
-    (build-system ocaml-build-system)
-    (outputs '("out" "ide"))
+            (files (list "lib/coq/user-contrib")))
+           (search-path-specification
+            (variable "COQLIB")
+            (files (list "lib/ocaml/site-lib/coq"))
+            (separator #f))))
+    (build-system dune-build-system)
     (inputs
-     `(("lablgtk" ,lablgtk3)
-       ("python" ,python-2)
-       ("camlp5" ,camlp5)
-       ("ocaml-num" ,ocaml-num)))
+     `(("gmp" ,gmp)
+       ("ocaml-zarith" ,ocaml-zarith)))
     (native-inputs
-     `(("ocaml-ounit" ,ocaml-ounit)
-       ("rsync" ,rsync)
-       ("which" ,which)))
+     `(("which" ,which)))
     (arguments
-     `(#:phases
-       (modify-phases %standard-phases
-         (add-after 'unpack 'make-git-checkout-writable
-           (lambda _
-             (for-each make-file-writable (find-files "."))
-             #t))
-         (replace 'configure
-           (lambda* (#:key outputs #:allow-other-keys)
-             (let* ((out (assoc-ref outputs "out"))
-                    (mandir (string-append out "/share/man"))
-                    (browser "icecat -remote \"OpenURL(%s,new-tab)\""))
-               (invoke "./configure"
-                       "-prefix" out
-                       "-mandir" mandir
-                       "-browser" browser
-                       "-coqide" "opt"))))
-         (replace 'build
-           (lambda _
-             (invoke "make"
-                     "-j" (number->string (parallel-job-count))
-                     "world")))
-         (delete 'check)
-         (add-after 'install 'remove-duplicate
-           (lambda* (#:key outputs #:allow-other-keys)
-             (let* ((out (assoc-ref outputs "out"))
-                    (bin (string-append out "/bin"))
-                    (coqtop (string-append bin "/coqtop"))
-                    (coqidetop (string-append bin "/coqidetop"))
-                    (coqtop.opt (string-append coqtop ".opt"))
-                    (coqidetop.opt (string-append coqidetop ".opt")))
-               ;; These files are exact copies without `.opt` extension.
-               ;; Removing these saves 35 MiB in the resulting package.
-               ;; Unfortunately, completely deleting them breaks coqide.
-               (delete-file coqtop.opt)
-               (delete-file coqidetop.opt)
-               (symlink coqtop coqtop.opt)
-               (symlink coqidetop coqidetop.opt))
-             #t))
-         (add-after 'install 'install-ide
-           (lambda* (#:key outputs #:allow-other-keys)
-             (let ((out (assoc-ref outputs "out"))
-                   (ide (assoc-ref outputs "ide")))
-               (mkdir-p (string-append ide "/bin"))
-               (rename-file (string-append out "/bin/coqide")
-                            (string-append ide "/bin/coqide")))
-             #t))
-         (add-after 'install 'check
-           (lambda _
-             (with-directory-excursion "test-suite"
-               ;; These two tests fail.
-               ;; Fails because the output is not formatted as expected.
-               (delete-file-recursively "coq-makefile/timing")
-               ;; Fails because we didn't build coqtop.byte.
-               (delete-file "misc/printers.sh")
-               (invoke "make")))))))
+     `(#:package "coq"
+       #:test-target "test-suite"))
     (home-page "https://coq.inria.fr")
     (synopsis "Proof assistant for higher-order logic")
     (description
@@ -142,6 +89,31 @@ It is developed using Objective Caml and Camlp5.")
     ;; Some of the documentation is distributed under opl1.0+.
     (license (list license:lgpl2.1 license:opl1.0+))))
=20
+(define-public coq-ide-server
+  (package
+    (inherit coq)
+    (name "coq-ide-server")
+    (arguments
+     `(#:tests? #f
+       #:package "coqide-server"))
+    (inputs
+     `(("coq" ,coq)
+       ("gmp" ,gmp)
+       ("ocaml-zarith" ,ocaml-zarith)))))
+
+(define-public coq-ide
+  (package
+    (inherit coq)
+    (name "coq-ide")
+    (arguments
+     `(#:tests? #f
+       #:package "coqide"))
+    (propagated-inputs
+     `(("coq" ,coq)
+       ("coq-ide-server" ,coq-ide-server)))
+    (inputs
+     `(("lablgtk3" ,lablgtk3)))))
+
 (define-public proof-general
   ;; The latest release is from 2016 and there has been more than 450 comm=
its
   ;; since then.
@@ -274,7 +246,7 @@ inside Coq.")
 (define-public coq-gappa
   (package
     (name "coq-gappa")
-    (version "1.4.4")
+    (version "1.4.6")
     (source
      (origin
        (method git-fetch)
@@ -284,7 +256,7 @@ inside Coq.")
        (file-name (git-file-name name version))
        (sha256
         (base32
-         "0f3g3wjkvfkm961l4jpckhsqd43jnvm7f5qqk78qc32zh1fg339n"))))
+         "0492i0ksrz6dnc1d57jzsbmdlb9fp9hrh9ib5v8j0yqxpyi0x8f4"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("autoconf" ,autoconf)
@@ -298,13 +270,14 @@ inside Coq.")
     (inputs
      `(("gmp" ,gmp)
        ("mpfr" ,mpfr)
+       ("ocaml-zarith" ,ocaml-zarith)
        ("boost" ,boost)))
     (propagated-inputs
      `(("coq-flocq" ,coq-flocq)))
     (arguments
      `(#:configure-flags
-       (list (string-append "--libdir=3D" (assoc-ref %outputs "out")
-                            "/lib/coq/user-contrib/Gappa"))
+       (list (string-append "COQUSERCONTRIB=3D" (assoc-ref %outputs "out")
+                            "/lib/coq/user-contrib"))
        #:phases
        (modify-phases %standard-phases
          (add-before 'configure 'fix-remake
@@ -334,7 +307,7 @@ assistant.")
 (define-public coq-mathcomp
   (package
     (name "coq-mathcomp")
-    (version "1.11.0")
+    (version "1.12.0")
     (source
      (origin
        (method git-fetch)
@@ -343,7 +316,7 @@ assistant.")
              (commit (string-append "mathcomp-" version))))
        (file-name (git-file-name name version))
        (sha256
-        (base32 "1axywpa1jcpnidd86irpd1gdbbg2sfbwc652675xisq5wnmfmf6f"))))
+        (base32 "12cgrmzlcjnp9kv9zxsk34fgf0qfa35jdb23cbf13kmg8dyfi3h5"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("ocaml" ,ocaml)
@@ -429,7 +402,7 @@ theorems between the two libraries.")
 (define-public coq-bignums
   (package
     (name "coq-bignums")
-    (version "8.11.0")
+    (version "8.13.0")
     (source (origin
               (method git-fetch)
               (uri (git-reference
@@ -438,13 +411,14 @@ theorems between the two libraries.")
               (file-name (git-file-name name version))
               (sha256
                (base32
-                "1xcd7c7qlvs0narfba6px34zq0mz8rffnhxw0kzhhg6i4iw115dp"))))
+                "1n66i7hd9222b2ks606mak7m4f0dgy02xgygjskmmav6h7g2sx7y"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("ocaml" ,ocaml)
        ("coq" ,coq)))
     (inputs
-     `(("camlp5" ,camlp5)))
+     `(("camlp5" ,camlp5)
+       ("ocaml-zarith" ,ocaml-zarith)))
     (arguments
      `(#:tests? #f ; No test target.
        #:make-flags
@@ -462,7 +436,7 @@ provides BigN, BigZ, BigQ that used to be part of Coq s=
tandard library.")
 (define-public coq-interval
   (package
     (name "coq-interval")
-    (version "4.0.0")
+    (version "4.3.0")
     (source
      (origin
        (method git-fetch)
@@ -472,7 +446,7 @@ provides BigN, BigZ, BigQ that used to be part of Coq s=
tandard library.")
        (file-name (git-file-name name version))
        (sha256
         (base32
-         "01iz6qmnsm6b9s1vmdjs79vjx9xgwzn5rwyjp6bvs8hg3zlmhpip"))))
+         "1jqvd17czhliscf40idhnxgrha620039ilrdyfahn71dg2jmzqnm"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("autoconf" ,autoconf)
@@ -484,11 +458,12 @@ provides BigN, BigZ, BigQ that used to be part of Coq=
 standard library.")
      `(("flocq" ,coq-flocq)
        ("bignums" ,coq-bignums)
        ("coquelicot" ,coq-coquelicot)
-       ("mathcomp" ,coq-mathcomp)))
+       ("mathcomp" ,coq-mathcomp)
+       ("ocaml-zarith" ,ocaml-zarith)))
     (arguments
      `(#:configure-flags
-       (list (string-append "--libdir=3D" (assoc-ref %outputs "out")
-                            "/lib/coq/user-contrib/Gappa"))
+       (list (string-append "COQUSERCONTRIB=3D" (assoc-ref %outputs "out")
+                            "/lib/coq/user-contrib"))
        #:phases
        (modify-phases %standard-phases
          (add-before 'configure 'fix-remake
@@ -558,21 +533,23 @@ uses Ltac to synthesize the substitution operation.")
 (define-public coq-equations
   (package
     (name "coq-equations")
-    (version "1.2.3")
+    (version "1.2.4")
     (source (origin
               (method git-fetch)
               (uri (git-reference
                     (url "https://github.com/mattam82/Coq-Equations")
-                    (commit (string-append "v" version "-8.11"))))
+                    (commit (string-append "v" version "-8.13"))))
               (file-name (git-file-name name version))
               (sha256
                (base32
-                "1srxz1rws8jsh7402g2x2vcqgjbbsr64dxxj5d2zs48pmhb20csf"))))
+                "0i014lshsdflzw6h0qxra9d2f0q82vffxv2f29awbb9ad0p4rq4q"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("ocaml"  ,ocaml)
        ("coq"    ,coq)
        ("camlp5" ,camlp5)))
+    (inputs
+     `(("ocaml-zarith" ,ocaml-zarith)))
     (arguments
      `(#:test-target "test-suite"
        #:phases
--=20
2.32.0


--MP_/jGUdlqUdtTBeoke1qO/tY2U--




Acknowledgement sent to Julien Lepiller <julien@HIDDEN>:
New bug report received and forwarded. Copy sent to guix-patches@HIDDEN. Full text available.
Report forwarded to guix-patches@HIDDEN:
bug#49423; 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 Jul 2021 13:30:02 UTC

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