GNU bug report logs - #64249
[PATCH ocaml-team 1/2] gnu: ocaml: Update to 4.14.1.

Previous Next

Full log

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

From: Julien Lepiller <julien <at> lepiller.eu>
To: pukkamustard <pukkamustard <at> posteo.net>
Cc: 64249 <at> debbugs.gnu.org, DABY-SEESARAM Arnaud <ds-ac <at> nanein.fr>,
 Josselin Poiret <dev <at> jpoiret.xyz>
Subject: Re: [bug#64249] [PATCH ocaml-team v4 0/9]
Date: Sun, 30 Jul 2023 19:42:21 +0200

Le Fri, 28 Jul 2023 11:08:22 +0000,
pukkamustard <pukkamustard <at> posteo.net> a écrit :

> Hello,
> 
> This v4 fixes the previously broken Coq packages.
> 
> As mentioned (https://issues.guix.gnu.org/64249#20) this merges
> coq-core and coq-stdlib into coq.
> 
> It turns out that dune allows multiple package to be built at the
> same time by providing a comma-seperated list. Our #:package field
> can be fed such a comma-seperated list. With this trick only the
> 'install phase needs some tweaking. Eventually it would be nice to
> allow our #:package field to be a proper Scheme list.
> 
> Some Coq packages need to be updated for 8.17.1 compatibility. I have
> not systematically checked all Coq packages. Let's see what CI says.
> 
> opam is still broken. Very gracious if another pair of eyes could
> have a look.
> 
> Thanks,
> pukkamustard
> 
> pukkamustard (9):
>   gnu: ocaml: Update to 4.14.1.
>   gnu: Update coq-flocq to 4.1.1.
>   gnu: Update coq-gappa to 1.5.3.
>   gnu: Update coq-mathcomp to 1.17.0.

This patch breaks coq-coquelicot, but it can be updated to 1.4.0, and
that fixes the issue.

>   gnu: coq: Update to 8.17.1.

You've missed a coq-stdlib reference in coq-mathcomp-finmap, but simply
removing it fixes the issue.

coq-autosubst-1, coq-equations, coqstdpp, coq-interval and
coq-mathcomp-bigenough fail to build with the newer coq. coq-ide also
fails, but it used to fail already.

>   gnu: dune-bootstrap: Update to 3.9.1.
>   gnu: opam: Split build into smaller sub-packages.

there are quite a few more failures with this patch. For instance,
ocaml-topkg fails because it can't find the opam-installer binary.

>   gnu: Add opam-installer.

And of course this patch fixes the issue. I haven't followed closely
recent changes to policy, but it used to be that, if there were no
other solutions we would prefer to have multiple changes in a single
patch if separating them would break something, even in an intermediate
commit.

ocaml-ocb-stubblr still fails because it has opam instead of
opam-installer. It can be switche to new style inputs too :)

>   FIXME: gnu: opam: Update to 2.1.5.

You replaced the home-page of dose3 with the http version, but the
https version still works.

I looked into the build issue, but I can only see deprecation warnings.
Did I miss something?

> 
>  gnu/local.mk                                  |   4 -
>  gnu/packages/coq.scm                          |  77 ++--
>  gnu/packages/ocaml.scm                        | 365
> ++++++++++++------ .../ocaml-dose3-Fix-for-ocaml-4.06.patch      |
> 52 --- .../ocaml-dose3-Install-mli-cmx-etc.patch     | 133 -------
>  .../ocaml-dose3-add-unix-dependency.patch     |  25 --
>  .../ocaml-dose3-dont-make-printconf.patch     |   9 -
>  7 files changed, 267 insertions(+), 398 deletions(-)
>  delete mode 100644
> gnu/packages/patches/ocaml-dose3-Fix-for-ocaml-4.06.patch delete mode
> 100644 gnu/packages/patches/ocaml-dose3-Install-mli-cmx-etc.patch
> delete mode 100644
> gnu/packages/patches/ocaml-dose3-add-unix-dependency.patch delete
> mode 100644 gnu/packages/patches/ocaml-dose3-dont-make-printconf.patch
> 
> 
> base-commit: 01412c6c6a98e4da10676560638640d0f33e1a02

Previous Next

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