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@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@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.  :)