CEP on the future of CoqIDE. #68
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,102 @@ | ||
| --- | ||
| Title: Future of CoqIDE | ||
| Drivers: Karl Palmskog (@palmskog), Théo Zimmermann (@Zimmi48) | ||
| --- | ||
|
|
||
| ## Summary | ||
|
|
||
| The goal of this CEP is: | ||
|
|
||
| 1. to clarify the priority and focus shift by the Coq team away from maintaining and evolving CoqIDE; | ||
| 2. to give an opportunity to the community of CoqIDE users to assume maintenance of and lead the future evolution of CoqIDE through a source code split out of the Coq GitHub repository. | ||
|
|
||
| More specifically, the proposal is to make an open call for new volunteer maintainers of CoqIDE through Coq community channels, and then to proceed with a source code split only if volunteer maintainers are found. | ||
|
|
||
| ## Context and motivation | ||
|
|
||
| [CoqIDE](https://coq.inria.fr/refman/practical-tools/coqide.html) is an Integrated Development Environment (IDE) for Coq. CoqIDE is implemented using the OCaml programming language and the GTK3 widget toolkit for Graphical User Interfaces (GUIs), thanks to the [lablgtk3](https://opam.ocaml.org/packages/lablgtk3/) OCaml package. | ||
|
|
||
| CoqIDE communicates with Coq thanks to an [XML protocol](https://github.com/coq/coq/blob/master/dev/doc/xml-protocol.md), implemented by the coqidetop server (in the coqide-server opam package), which itself is based on a component in Coq called the [State Transaction Machine](https://coq.github.io/doc/master/api/coq-core/Stm/index.html) (STM). | ||
|
|
||
| The drawbacks of CoqIDE and coqidetop are that: | ||
|
|
||
| - maintaining a standalone IDE just for Coq means that a lot of standard work has to be redone and lots of standard IDE features are not implemented, | ||
| - the XML protocol is entirely custom and suited for the CoqIDE implementation, which means that any IDE wanting to interface with Coq through this protocol has to reimplement a lot of things, and that it won't always be well-suited to the model that the IDE expects. | ||
|
Comment on lines
+23
to
+24
There was a problem hiding this comment. I think it would be useful to quantify the "lot" in "a lot of standard work has to be redone", in "lots of standard IDE features are not implemented", and in "any IDE wanting to interface with Coq through this protocol has to reimplement a lot of things". In particular, is it only my perception or not, but I don't see LSP as magically solving the question of implementing features, or compliance to a protocol. If my perception is correct, it is probably worth to be made clear. There was a problem hiding this comment. It would require a proper evaluation, which I'm not able to conduct myself, but which I would be interested in if it were to happen. There was a problem hiding this comment. Indeed I think my comment above reflected the same thing, LSP solves a lot of practical problems (especially when bootstrapping), but from the Coq side it has little importance, in the sense that what we need to agree upon is how we want to implement something such as a LSP server. |
||
|
|
||
|
There was a problem hiding this comment. It seems to me that this paragraph conflates two parts of what we call "protocol" which are IMO different:
In the end, the transport layer doesn't matter much, for example the XML protocol could have some changes in its interaction model and greatly improve client's life, while maintaining the current transport layer. [Actually the XML protocol tied to offer an updated interaction model with |
||
| Recently, the Coq team has changed its strategy, by focusing instead on developing support for the [Language Server Protocol](https://microsoft.github.io/language-server-protocol/) (LSP) with minimal extensions, which should bring the possibility to develop Coq support for any standard IDE (starting with VS Code). Meanwhile, CoqIDE, coqidetop and the STM are considered outdated technology that the Coq team would like to avoid putting too much work into maintaining. | ||
|
There was a problem hiding this comment. For the sake of history LSP support was already discussed in 2016 ( rocq-archive/coq-serapi#26 ) and first implemented in Lambdapi in spring 2018 (with Atom as the main editor) There was a problem hiding this comment. Where is the "strategy of the Coq team" written down? There was a problem hiding this comment.
In this CEP. Part of the role of this CEP was to write this down. For the rest of the topics that the "strategy of the Coq team" should address, the answer is unfortunately virtually nowhere. There was a problem hiding this comment. I see, thanks! Indeed the CEP is a very good step. I think I was a bit confused by how I interpret the "support for LSP" bit. For me, "support for LSP" is indeed almost empty of meaning, in the sense that there are many ways to "support LSP" and even for LSP different protocol configurations do force widly different design requirements in the server and even in the client. (Notably VS Code is struggling to support some LSP features!) When we went ahead and bootstrapped the first server for Lambdapi, we choose LSP fully on practical concerns, but we knew it is not a great model for ITPs and in fact some design constraints we use are different than LSP and we lobby for LSP to correct some design mistakes it has as of today. IMHO the relevant bits for people working on language servers has more to do about different choices on the Coq design itself, in particular how to handle async vernaculars, interpretation deps, system layers, ASTs, etc... Even the build system plays a central role here, and LSP says little about it for example. There was a problem hiding this comment. IIUC, we're only using a small subset of the Microsoft-specified LSP protocol and we've made changes to the parts we've used. How much existing LSP code have we reused? (IIUC that was one of the main rationales for using it.) I assume we're using reusing the lower-level aspects, e.g. how messages are encoded (Json?) and the sequence of operations. |
||
|
|
||
| Because *some users still prefer a standalone IDE for Coq*, and some are *motivated to contribute to CoqIDE*, we want to give the opportunity to the community to take over CoqIDE maintenance by splitting out the CoqIDE source code from Coq's repository, on the condition that volunteer maintainers are found. | ||
|
There was a problem hiding this comment.
Is this data taken from the survey? There was a problem hiding this comment.
Survey + anecdotal evidence. But you are right that we should have explicitly acknowledged the findings from the survey in this text. There was a problem hiding this comment. I was wondering what the users are, maybe the way to find out is to do the split. There was a problem hiding this comment. If we do not find volunteer maintainers, then I would really discourage doing the split as it would just make it more complex for core Coq devs to maintain CoqIDE, without bringing any additional benefits (like a new dynamics). The previous example of a split without volunteer maintainers was bignums and it was a huge mistake (until it was finally fixed by finding such volunteer maintainers years later). There was a problem hiding this comment. A split without maintainers would go against what we say elsewhere in the CEP:
I think this requirement is the right thing, not least due to the experience with Bignums. There was a problem hiding this comment. I was wondering whether you could face here a bit of "chicken and egg" problem: people interested in contributing will not do so until the split is done, and the split is not done if not enough critical mass is perceived. As a person that has the technical knowledge to split and maintain CoqIDE, the question just below about having "complete freedom" is the most important one IMO. |
||
|
|
||
| ## Detailed design | ||
|
|
||
| ### Short-term actions | ||
|
|
||
| Upon acceptance of this CEP, we will send an open call for volunteer maintainers. The planned text of the call is available below, in an appendix to the CEP's main text. | ||
|
|
||
| In the case where volunteer maintainer(s) are found: | ||
|
|
||
| 1. The code for CoqIDE (the UI part) will be split into a separate repository (the code for coqidetop and the STM will remain in the Coq repository for as long as there are other major users besides CoqIDE that depend on them). The repository will temporarily be created in the Coq organization. | ||
| 2. Any issue in the Coq issue tracker pertaining to CoqIDE will be moved to this new repository. | ||
| 3. The repository will be transferred to the [Coq-community organization](https://github.com/coq-community/manifesto). | ||
| 4. The volunteer maintainer(s) will be given admin access to the repository. | ||
| 5. CoqIDE will be added in Coq's Continuous Integration (CI), but there is no commitment from the Coq team that it will get to stay there indefinitely. | ||
| 6. CoqIDE will keep being distributed as part of the [Coq Platform](https://github.com/coq/platform), for as long as it respects the inclusion criteria (timely release of compatible CoqIDE versions with new Coq releases), but will no longer be considered an official project by the Coq team. | ||
|
|
||
| The new CoqIDE maintainers will receive support from both the Coq team (for as long as CoqIDE is in Coq's CI, more about this in the next subsection) and from the Coq-community organization owners (to set up solutions for CI, deploying documentation, protecting branches, etc.), but they will have complete freedom to define: | ||
|
|
||
| - what features / changes to include, | ||
|
There was a problem hiding this comment. That seems like a tricky point, imagine new CoqIDE maintainers decide to drop the debugger (which IMHO needs reimplementing), what would that mean? This is also relevant to point 1, as keeping the STM in Coq codebase does greatly hamper development for other IDEs and sustract quite a lot of eng resources to maintain it. There was a problem hiding this comment. If the debugger isn't available in vsCoq2 at that time, I think the users of the debugger would be up in arms. |
||
| - what technology / internal changes to make, | ||
| - which versions of Coq to support, | ||
| - how to review and merge changes (in particular, we expect that the reviewing process will become more lightweight than it is currently in the Coq repository, with the ability, in particular, to self-merge some pull requests), | ||
| - when and how frequently to release new CoqIDE versions (keeping in mind that some releases will be mandated by the Coq Platform inclusion). | ||
|
|
||
| A recommendation to CoqIDE maintainers is to quickly make CoqIDE compatible with multiple Coq versions (at least when the XML protocol doesn't change). This technically already works with the limitation that CoqIDE doesn't check for the version of Coq: https://github.com/coq/coq/issues/16521. | ||
|
|
||
| ### Long-term plans | ||
|
|
||
| As explained above, members of the Coq team are currently developing support for LSP, along with VS Code extensions. There are two projects in this direction: | ||
| - [VsCoq2](https://github.com/coq-community/vscoq), a project for a stable Coq IDE led by Inria engineers and supported by stable Inria funding, and | ||
| - [coq-lsp](https://github.com/ejgallego/coq-lsp), a research project led by an Inria researcher and supported by research grants. | ||
|
There was a problem hiding this comment. This should be rewritten as "a project led by an Inria researcher", I think both the "research" qualification and the "supported by" wording are not accurate. There was a problem hiding this comment. If you have specific small rewordings like this that you want to include in the CEP text, I suggest you open a PR. For small rewordings, I think we can merge without having another formal process. There was a problem hiding this comment. Indeed, thanks @Zimmi48 , these don't seem like a big deal to me, but if I think some update is needed I'll take care myself of the PR. There was a problem hiding this comment.
Huh? This CEP has already been merged. |
||
|
|
||
| The two projects are based on different architectural choices and allow exploring different directions, but in both cases, they work with no dependency on the STM (VsCoq2 is based on a [new document manager](https://github.com/Coq-community/vscoq/blob/main/docs/developers.md#architecture) that can be considered as an evolved, more modular, and smaller STM, while coq-lsp is based on an incremental document checking engine called Flèche). There are hopes that despite the different architecture and implementation, the specification of the LSP extension that they implement can eventually be shared. coq-lsp is already available for use with recent versions of Coq, and VsCoq2 is planned to become available with Coq 8.18. | ||
|
|
||
| When Coq LSP support becomes stable enough, maintainers of IDE support packages for Coq (e.g., Proof General for Emacs, Coqtail for Vim) will be encouraged to migrate to using this protocol. We expect that Coqtail will be one of the first IDEs to migrate, as it currently depends on coqidetop and the XML protocol (and such a migration has already [seen experiments](https://github.com/whonore/Coqtail/pull/323)). | ||
|
|
||
| When no major IDE besides CoqIDE relies on the XML protocol anymore, the Coq team will start considering removal of coqidetop from the Coq repository. It will then become time for CoqIDE maintainers to decide what to do regarding the long-term future of CoqIDE. At this point, several options will be available: | ||
|
There was a problem hiding this comment. I expect we'll want to ensure that some current GUI features are available in at least one coq-lsp based GUI, such as the debugger and proof diffs, neither of which are currently supported by coq-lsp. Perhaps worth stating more explicitly as a goal rather than just the nonspecific "will start considering ..."? There was a problem hiding this comment. There is a protocol for debuggers, DAP. So I'm not so sure what do you really mean here. There was a problem hiding this comment. DAP! Yes, I should have mentioned DAP! I'm prone to forget the distinction because CoqIDE has only one protocol. We'll need to create coq-dap code. The point is that some current GUI features should be available in, say, vsCoq2 before we consider dropping coqidetop--gating on a bit more than "no major GUI besides CoqIDE". Is that clearer? Proof diffs requires rich text--what's the plan to support that? Also, is there a plan for supporting something akin to Pp.ml that will split lines in pleasing way? (The debugger has a need for that, too.) There was a problem hiding this comment. I don't think I can get the core team to formally commit at this time to a specific set of features that should be available in other IDEs before CoqIDE can be removed, but I also think that CoqIDE removal (when it's time) won't be a light decision, and needs of major users won't be easily ignored. |
||
|
|
||
|
There was a problem hiding this comment. That strategy seems too much in a lock-step to me, and thus of high risk. IMHO instead of a sudden "removal", a more gradual strategy should be used, in particular by gradually deprecating the most problematic features which can be done without breaking 3rd party systems too much. There was a problem hiding this comment. Removal of coqidetop is not as much of a breaking change as the removal of the STM APIs it relies on (coqidetop could be simply moved to the CoqIDE split repo). The feature removal you are talking about concerns mostly the underlying API, and we tried to convey this idea that features could be removed gradually instead of the whole component in the next paragraph on the STM. There was a problem hiding this comment. I saw that yes. Maybe what I mean here is that for example, it is easy to reimplement most of Stm API on top of Flèche, and there are other API bits that I'd personally remove. So in a sense it is a viable alternative to keep a STM-like API on top of Flèche, in fact I'm willing to do this depending on how the SerAPI migration goes, tho after having a look at what users need I'm convienced they want yet another API for their high-throughtpout use cases. There was a problem hiding this comment. Do you have a pointer to which features are the problematic ones? TBH I don't have a clear idea of what features the stm has. There was a problem hiding this comment. I have some notes, maybe that would be a good topic for the call (too late for this week tho), or even a CEP ? There was a problem hiding this comment. Whatever format you prefer. |
||
| - declare the end of the CoqIDE maintenance, | ||
| - migrate CoqIDE to rely on LSP instead of the XML protocol, following the example of other IDEs, but without the support of standard parts of LSP being natively suported in the editor, | ||
| - keep maintaining coqidetop for as long as the required APIs / components are there in Coq. | ||
|
|
||
| Note that coqidetop depends on the STM, and that the STM will be eventually removed from Coq (or features from the STM will be gradually removed) as STM users are gradually migrated off it or deprecated. (Besides coqidetop, another major STM user is [SerAPI](https://github.com/ejgallego/coq-serapi), on which [Alectryon](https://github.com/cpitclaudel/alectryon) is built, but there are already plans to migrate Alectryon off SerAPI and deprecating SerAPI in favor of coq-lsp.) At this point, if CoqIDE requires specific APIs that the Coq developers do not want to maintain, they won't hesitate to remove CoqIDE from Coq's CI. | ||
|
|
||
|
There was a problem hiding this comment. JsCoq is another mayor user of the STM. There was a problem hiding this comment. We can add it to the text. There was a problem hiding this comment. Sure, not a big deal tho. I'm happy to take care of such updates myself. |
||
| Other factors are likely to affect the future of CoqIDE, in particular its dependance on GTK3 through lablgtk. Migration from GTK2 to GTK3 was only possible thanks to a coordinated effort by maintainers of multiple GUIs to contribute to update lablgtk for compatibility with GTK3. We don't know if similar efforts will happen to make lablgtk keep up with changes to GTK (which is currently already at version 4). The number of GUIs depending on [lablgtk3](https://opam.ocaml.org/packages/lablgtk3/) is already much lower than the number that used to depend on [lablgtk2](https://opam.ocaml.org/packages/lablgtk/). Two other major users of lablgtk3 are Frama-C and Why3. At this time and to the best of our knowledge, there is no plan for these users to stop depending on lablgtk. However, if they were to decide at some point in the future to similarly prioritize VS Code support, this would leave the lablgtk ecosystem at higher risk of becoming unmaintained. | ||
|
|
||
| ## Drawbacks | ||
|
|
||
| - By giving the opportunity to the community to take over the maintenance of CoqIDE, we create the possibility that maintenance effort will be put in a technology that ends up outdated and unmaintained after a few years anyway. This is why this CEP tries to highlight not only the short-term benefits, but also the long-term risks. | ||
| - Another risk is that because new CoqIDE maintainers may have less strict reviewing and releasing policies, new CoqIDE versions include regressions affecting its user base (which is still quite large). In this case, we hope that the added flexibility in the CoqIDE maintenance will allow producing new releases which fix these regressions quickly, or that compatibility with several Coq versions will allow maintaining several lines of CoqIDE in parallel (e.g., a more stable line and a more experimental one with new features). | ||
|
|
||
| ## Alternatives | ||
|
|
||
| - The main alternative is to keep CoqIDE as part of the main Coq repository and as an official Coq project. In this case, the Coq team is not ready to do more than the minimal amount of maintenance effort because of its shift in priority focus. Therefore, users shouldn't expect big improvements to CoqIDE, even if they come from pull requests by external contributors (there will be no guarantee that these get reviewed and merged, as CoqIDE will be considered mostly "frozen"). | ||
|
|
||
| ## Unresolved questions | ||
|
|
||
| - Previous calls for volunteer maintainers (VsCoq1, Docker-Coq) have included a mention that the maintainers would be given recognition by adding them on the official Coq Team page. In this case, since the goal is to remove the official status of CoqIDE, it is not clear that this would be appropriate. If CoqIDE maintainers are acknowledged on this page, perhaps we should extend it to also acknowledge maintainers of other Coq IDEs, such as Proof General, Coqtail, and jsCoq. | ||
|
|
||
| ## Appendix: Call for volunteer maintainers of CoqIDE | ||
|
|
||
| The Coq core team and Coq-community are looking for volunteer maintainers of the CoqIDE project. | ||
|
|
||
| CoqIDE is an Integrated Development Environment (IDE) for Coq. CoqIDE is implemented using the OCaml programming language and the GTK3 widget toolkit for graphical user interfaces (GUIs). CoqIDE uses a legacy XML-based protocol to communicate with Coq and is licensed under the open source LGPL-2.1 license. | ||
|
|
||
| CoqIDE's source code is currently part of Coq's GitHub repository. Due to a desire to shift IDE-related work toward LSP and VS Code support, the Coq core team no longer considers CoqIDE maintenance and evolution a priority. With this call, the team wants to give an opportunity to the Coq community to take over CoqIDE maintenance and lead its future evolution. | ||
|
|
||
| If maintainers are found, CoqIDE sources will be moved to a repository in the Coq-community organization on GitHub, where it will receive support and fixes from the core team for a limited time. If no maintainers are found, CoqIDE sources will be kept in Coq's repository and minimally maintained until their eventual removal. | ||
|
|
||
| More details about the context and the plans for the future of IDEs for Coq can be found in the CEP leading to this call: \<add link to this CEP here\> | ||
|
|
||
| Please respond to this GitHub issue with a brief motivation and summary of relevant experience for becoming a CoqIDE maintainer. As part of their application, volunteer maintainers are encouraged to briefly present their short-term and long-term plans for CoqIDE and how long they think they will remain active on CoqIDE maintenance. However, this won't be considered as a commitment on their part, as plans and priorities can evolve based on the context and personal circumstances. The maintainer(s) will be selected from the issue responders by the Coq core team and Coq-community organization owners. Responders not selected will still be encouraged to contribute to CoqIDE in collaboration with the new maintainer(s) and other contributors. | ||
|
There was a problem hiding this comment. How about reformatting the entire document so all the lines are of a reasonable length, e.g. 80 characters max? There was a problem hiding this comment. And adding the link to this CEP? There was a problem hiding this comment. We will do two versions of the call for maintainers, one for Coq Discourse (Markdown) and one for email (Coq-club). The formatting of these calls will be different, so I don't see any point of pre-formatting the CEP appendix right now. There was a problem hiding this comment.
You should probably read the CEP using the Markdown renderer (e.g., the link in the top post).
This link should be a link to the merged CEP, so the document rather than the pull request, and it would be a broken link until we merge it. There was a problem hiding this comment.
I suggested reformatting the entire document, not just the appendix |
||
|
|
||
| Anyone else planning to get involved as an active and regular contributor to the CoqIDE project is also welcome to make themselves known in this GitHub issue and to briefly present which improvements and changes they plan to propose. | ||
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I feel like these are really 3 components (document manager = STM, transport layer = pretty thin XML component). In my experience people seem to get confused about the roles here.