Hi Antero,

Antero Mejr <mail@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