Subject: [bug#52164] [PATCH] gnu: coq: Update to 8.14.0.

From: zimoun <[email-masked]>
Date: Mon, 29 Nov 2021 14:21:16 +0100

Hi Julien,

On Mon, 29 Nov 2021 at 13:30, Julien Lepiller <[email-masked]> 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 [email-masked].
Or do you mean that [email-masked] is broken with [email-masked]?

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