Stream: Coq devs & plugin devs

Topic: Splitting CoqIDE

view this post on Zulip Emilio Jesús Gallego Arias (Jul 17 2020 at 09:34):

Hi all, in these last days the thought of moving CoqIDE to its own independent project has crossed my mind again, and I'm finally becoming convinced that this makes a lot of sense by several reasons.

In particular, there is no reason for CoqIDE releases to be tied to Coq releases; also, packaging and testing of CoqIDE is a bit challenging for Coq core devs. Having a split repos would also allow for more contributors, a lighter process, and the use of more dependencies on CoqIDE's side.

Moreover, the current setup is not bound to scale if we add more UI's to Coq repos; we would have to spend significant time keeping track of the dependencies. For 8.13, the main installation images are supposed to come from the platform indeed, so CoqIDE would be a good candidate to use that, tho CoqIDE itself could provide Coq + CoqIDE images in its repos.


view this post on Zulip Karl Palmskog (Jul 17 2020 at 11:55):

since I help out with Coq opam packaging, I can tell you CoqIDE has been a pain every time to package due to its dependencies. We have started to submit Coq and CoqIDE opam packages separately to the general repo since CoqIDE will usually get stuck on CI. I think this would be an argument in favor of decoupling Coq from CoqIDE.

view this post on Zulip Paolo Giarrusso (Jul 17 2020 at 16:49):

Does CoqIDE have any dependencies on the Coq version?

view this post on Zulip Paolo Giarrusso (Jul 17 2020 at 16:50):

(Currently wondering if Coq 8.12.0 could reuse CoqIDE 8.11.2 as-is, but I feel I've exhausted my hack quota.)

view this post on Zulip Michael Soegtrop (Jul 17 2020 at 16:56):

In opam cpqide is already a separate package. Maybe one could try what happen if one relaxes the version restrictions ...

view this post on Zulip Enrico Tassi (Jul 17 2020 at 19:43):

IIRC the XML protocol did not change, hence CoqIDE should work. IMO Coq should version the XML protocol (there is a init message, but I don't recall if it carries a version). CoqIDE should just check that version that say: I'm too new/old. This is the prerequisite for a split, IMO.

view this post on Zulip Théo Zimmermann (Jul 18 2020 at 18:10):

Other IDEs working with the XML protocol already manage to support several versions. The XML protocol is very stable.

Last updated: Oct 21 2021 at 21:03 UTC