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

[zimoun <zimon.toutoune@gmail.com>]

Hi Julien,

On Mon, 29 Nov 2021 at 13:30, Julien Lepiller <julien@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@8.13.2.
Or do you mean that coq-binums@8.13 is broken with coq@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