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

Previous Next

Full log

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

From: Julien Lepiller <julien <at> lepiller.eu>
To: zimoun <zimon.toutoune <at> gmail.com>
Cc: 52164 <at> debbugs.gnu.org
Subject: Re: bug#52164: [PATCH] gnu: coq: Update to 8.14.0.
Date: Mon, 29 Nov 2021 08:39:23 -0500

>
>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?

I meant to say bignums 8.13 is broken with coq 8.14, and bignums 8.14 is broken with coq 8.13.

>
>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?

I've always updated dependents first whenever possible (without breaking anything), then the compiler, then the rest that needs the new compiler. However, I've always been careful not to introduce breakage with a commit, even if it's inside a series. I think that's the policiy, but I'm not sure if it overrides the one-change per commit policy.

>
>
>Cheers,
>simon

Previous Next

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