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

Previous Next

To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 49423 in the body.
You can then email your comments to 49423 AT debbugs.gnu.org in the normal way.

Toggle the display of automated, internal messages from the tracker.

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

From: Julien Lepiller <julien <at> lepiller.eu>
To: guix-patches <at> gnu.org
Subject: [PATCH] gnu: coq: Update to 8.13.2.
Date: Tue, 6 Jul 2021 00:06:40 +0200

[Message part 1 (text/plain, 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.

[0001-gnu-ocaml-zarith-Update-to-1.12.patch (text/x-patch, attachment)]

[0002-gnu-lablgtk3-Install-with-version-information.patch (text/x-patch, attachment)]

[0003-gnu-coq-stdpp-Update-to-1.5.0.patch (text/x-patch, attachment)]

[0004-gnu-coq-Update-to-8.13.2.patch (text/x-patch, attachment)]

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

From: Ludovic Courtès <ludo <at> gnu.org>
To: Julien Lepiller <julien <at> lepiller.eu>
Cc: 49423 <at> debbugs.gnu.org
Subject: Re: bug#49423: [PATCH] gnu: coq: Update to 8.13.2.
Date: Wed, 21 Jul 2021 16:07:53 +0200

Hi,

Julien Lepiller <julien <at> lepiller.eu> 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’t tested it but the whole series LGTM!

Thanks,
Ludo’.

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

From: Xinglu Chen <public <at> yoctocell.xyz>
To: Julien Lepiller <julien <at> lepiller.eu>, 49423 <at> debbugs.gnu.org
Subject: Re: [bug#49423] [PATCH] gnu: coq: Update to 8.13.2.
Date: Sat, 24 Jul 2021 15:17:25 +0200

[Message part 1 (text/plain, inline)]

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 <at> lepiller.eu>
> 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
>
> From 76a337769e67e84a32c5b85d80ab6bc160792aef Mon Sep 17 00:00:00 2001
> From: Julien Lepiller <julien <at> lepiller.eu>
> 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.  :)

[signature.asc (application/pgp-signature, inline)]

Message #16 received at 49423-done <at> debbugs.gnu.org (full text, mbox):

From: Julien Lepiller <julien <at> lepiller.eu>
To: 49423-done <at> debbugs.gnu.org
Subject: Re: [bug#49423] [PATCH] gnu: coq: Update to 8.13.2.
Date: Sat, 31 Jul 2021 23:07:31 +0200

Le Tue, 6 Jul 2021 00:06:40 +0200,
Julien Lepiller <julien <at> lepiller.eu> a écrit :

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

Pushed to master as 96707d5a309d083b1a9bf1f0c8fc1251cf203337 to
e38b4d5ceb344c9707917a7d32df50d0ced082b5, thanks!

Previous Next

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