GNU bug report logs -
#75368
[PATCH] gnu: coq: Update to 8.20.0.
Previous Next
Full log
Message #8 received at 75368 <at> debbugs.gnu.org (full text, mbox):
[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.