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.
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.
Does CoqIDE have any dependencies on the Coq version?
(Currently wondering if Coq 8.12.0 could reuse CoqIDE 8.11.2 as-is, but I feel I've exhausted my hack quota.)
In opam cpqide is already a separate package. Maybe one could try what happen if one relaxes the version restrictions ...
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.
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