GNU bug report logs - #52164
[PATCH] gnu: coq: Update to 8.14.0.

Previous Next

Full log

View this message in rfc822 format

From: zimoun <zimon.toutoune <at> gmail.com>
To: Julien Lepiller <julien <at> lepiller.eu>
Cc: 52164 <at> debbugs.gnu.org
Subject: [bug#52164] [PATCH] gnu: coq: Update to 8.14.0.
Date: Mon, 29 Nov 2021 14:21:16 +0100

Hi Julien,

On Mon, 29 Nov 2021 at 13:30, Julien Lepiller <julien <at> lepiller.eu> wrote:

> >With this approach, 3 builds.  Is it required by kind-of Coq bootstrap?
>
> Coq now uses dune, and it is split into core, stdlib anl coq. I prefer to build one dune package in each guix package, rather than everything, especially since we want to separate coq-ide.

Thanks for the explanations.  So LGTM. :-)


> >>  (define-public coq-bignums
> >>    (package
> >>      (name "coq-bignums")
> >> -    (version "8.13.0")
> >> +    (version "8.14.0")
> >
> >This…
> >
> >>  (define-public coq-equations
> >>    (package
> >>      (name "coq-equations")
> >> -    (version "1.2.4")
> >> +    (version "1.3")
> >
> >and this… Cannot they be upgraded by a separated commit?
> >
> >They will probably be broken with Coq 8.13 but if their upgrade is right
> >after and pushed with the same batch, it is transparent and the
> >atomicity appears to me better.
>
> They're broken with coq 8.13, and the previous version is also broken with coq 8.14. This is why I was able to update coq semantics independently but not these two.

Hum, the breakage of coq-bignums or coq-equations is recent.  Because
using 65234d0 from Nov. 2nd, they are substituable; using coq <at> 8.13.2.
Or do you mean that coq-binums <at> 8.13 is broken with coq <at> 8.14?

In all cases, it appears to me clearer to have:

 1. update coq
 2. update coq-bignums
 3. update coq-equations

i.e., update the "compiler" and fix then the breakage introduced by
this "compiler" upgrade, e.g., upgrade other packages.  We are always
doing like that, no?


Cheers,
simon

Previous Next

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