GNU bug report logs - #75368
[PATCH] gnu: coq: Update to 8.20.0.

Previous Next

Full log

View this message in rfc822 format

From: Antero Mejr <mail <at> antr.me>
To: Arnaud Daby-Seesaram <ds-ac <at> nanein.fr>
Cc: pukkamustard <at> posteo.net, 75368 <at> debbugs.gnu.org, julien <at> lepiller.eu
Subject: [bug#75368] [PATCH] gnu: coq: Update to 8.20.0.
Date: Thu, 09 Jan 2025 16:27:44 -0500

Arnaud Daby-Seesaram <ds-ac <at> nanein.fr> writes:

> Thank you for your patch.  I have not had the time to look at it in
> detail yet, but here are a few questions/remarks that probably call for
> a V2:
>
> - some Coq-dependent packages are broken by the update (e.g. stdpp needs
>   to be updated to 1.11.0 to compile).  It would be nice to update
>   dependent packages if they support 8.20.

Yes, definitely.

Lately I've been wondering if a coq-build-system would be helpful, since
it seems there's a lot of commonality/boilerplate in the coq- packages.

> - If all Coq packages are updated to support 8.20 (I do not know if it
>   is possible), would it be worth renaming Coq into Rocq[0]?

AFAIK the rename is planned for the 9.0 release, which is still another
release away (after 8.21). The rename is going to be a mess. It appears
that the packaging system will be changing again, and also we'll have to
deprecate all the coq- packages if we want to maintain naming
consistency.

> - I understand the addition of python in the inputs, as Coq uses python
>   scripts.  However, I do not understand why rsync is added as an input.
>   Could you say a few words about this?

One of the test scripts uses rsync instead of mv to move a file. I chose
to add the dependency instead of patching it out. Maybe submitting a
patch upstream to fix that would be better.

Thanks for the review!

Previous Next

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