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

Previous Next

Package: guix-patches;

Reported by: Antero Mejr <mail <at> antr.me>

Date: Sun, 5 Jan 2025 00:56:02 UTC

Severity: normal

Tags: patch

Full log


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

From: Arnaud Daby-Seesaram <ds-ac <at> nanein.fr>
To: Antero Mejr <mail <at> antr.me>
Cc: pukkamustard <at> posteo.net, 75368 <at> debbugs.gnu.org, julien <at> lepiller.eu
Subject: Re: [bug#75368] [PATCH] gnu: coq: Update to 8.20.0.
Date: Thu, 09 Jan 2025 10:37:16 +0100
[Message part 1 (text/plain, inline)]
Hi Antero,

Antero Mejr <mail <at> antr.me> writes:
> Deprecates coq-ide-server, which is now part of the main coq package.
>
> * gnu/packages/coq.scm (coq): Update to 8.20.0.
> [native-inputs]: Add python, rsync.
> [arguments]: Patch tests, build coqide-server, symlink `coqidetop`.
> (coq-ide-server): Deprecate package.
> (coq-ide)[propagated-inputs]: Remove coq-ide-server.
> (coq-for-coqtail): Remove hidden package.
> * gnu/packages/coq.scm (vim-coqtail)[native-inputs]: Remove
> coq-for-coqtail.
> [native-inputs]: Add coq.

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.

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

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

[0] https://rocq-prover.org/


Best regards,

-- 
Arnaud
[signature.asc (application/pgp-signature, inline)]

This bug report was last modified 115 days ago.

Previous Next


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