Now that I have the Debian package for coq a bit better in hand, I would like to change how it divides coq into binary packages. The current situation is: coq coqide coq-theories libcoq-ocaml/libcoq-ocaml-dev.
I would like to make it: coq coqide libcoq-stdlib libcoq-core-ocaml/libcoq-core-ocaml-dev -- and perhaps something like libcoqide-server-ocaml/libcoqide-server-ocaml-dev ; but it isn't clear what coq's coqide-server package actually is and I can't find the list of files in the opam packages.
For example, the current Debian coqide package has /usr/bin/coqidetop* files which I feel should perhaps belong to the coqide package... or not?
(From here: https://tracker.debian.org/pkg/coq, at the bottom left you have links to the binary packages, and for each, you can access the list of files at the bottom of the associated page)
Julien Puydt said:
For example, the current Debian coqide package has /usr/bin/coqidetop* files which I feel should perhaps belong to the coqide package... or not?
I suppose you meant to say that the coq
package contains coqidetop
? That is fine. For example, if someone were to package coq-jupyter
, they would need the coqidetop
binary but they would certainly not want to depend on the coqide
package.
Ok, coqidetop doesn't go with coqide. But should it go with coq or coqide-server? I had the impression that coqide-server was somehow supposed to be a coqide-agnostic lib to interface with coq...
No idea. I don't know what coqide-server
is. And I cannot find any documentation mentioning that name.
coqide-server is an opam package provided by coq...
$ opam show coqide-server
[ERROR] No package matching coqide-server found
And as the maintainer of the Opam packages for Coq 8.14, I assure you that there is no such package. And you can check for yourself on https://opam.ocaml.org/packages/ for Coq 8.15.
I think this is the package definition alluded to: https://github.com/coq/coq/blob/master/coqide-server.opam
However, this package is not registered in any archives, it only lives in the Coq GitHub repo.
And given its first line, I have no idea why it was even committed to the repository in the first place.
Guillaume Melquiond said:
And given its first line, I have no idea why it was even committed to the repository in the first place.
That's due to opam needing the files to be committed. Should be eventually fixed upstream? Was discussed a few times.
coqide-server was created to have the xml-protocol stuff not in the main Coq package, in case we'd like to split it to an independent project.
Whether we want to keep it that way, it is open.
By the way there was some discussion today in the Dune meeting about making thigns better for Debian but I had to leave.
So I should just drop that coqide-server stuff until you decide... Good!
Last updated: Jun 09 2023 at 07:01 UTC