Stream: Coq devs & plugin devs

Topic: Making the Debian packages follow coq's


view this post on Zulip Julien Puydt (Feb 02 2022 at 18:03):

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)

view this post on Zulip Guillaume Melquiond (Feb 02 2022 at 18:47):

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.

view this post on Zulip Julien Puydt (Feb 02 2022 at 18:51):

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

view this post on Zulip Guillaume Melquiond (Feb 02 2022 at 18:54):

No idea. I don't know what coqide-server is. And I cannot find any documentation mentioning that name.

view this post on Zulip Julien Puydt (Feb 02 2022 at 19:32):

coqide-server is an opam package provided by coq...

view this post on Zulip Guillaume Melquiond (Feb 02 2022 at 19:40):

$ 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.

view this post on Zulip Karl Palmskog (Feb 02 2022 at 19:42):

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.

view this post on Zulip Guillaume Melquiond (Feb 02 2022 at 19:48):

And given its first line, I have no idea why it was even committed to the repository in the first place.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 02 2022 at 21:03):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 02 2022 at 21:10):

Whether we want to keep it that way, it is open.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 02 2022 at 21:10):

By the way there was some discussion today in the Dune meeting about making thigns better for Debian but I had to leave.

view this post on Zulip Julien Puydt (Feb 03 2022 at 12:33):

So I should just drop that coqide-server stuff until you decide... Good!


Last updated: Feb 01 2023 at 16:03 UTC