CEP on the future of CoqIDE. #68
Conversation
|
It is:
Yes
No, but I'm not aware of any LSP clients written in OCaml, so one has to start from scratch. Implementing an LSP client is simpler than implementing an XML protocol client. For example in order to get the basic functionality one can just send the entire text and display the diagnostics, while today CoqIDE has to keep a Document structure, to parse the text, send sentences one by one, map sentence ids to text locations to underline errors. |
Is there a way to quantify this "a lot"? I may be wrong but my perception was that the XML/lsp protocol is only the "emerged" part of the iceberg, that is about the basic features (completion, hovering, ...) while we certainly want to implement various features which are (maybe) not standardized as part of the XML/lsp protocols (such as annotated terms, with various actions on subterms such as turning a selected subterm into printing all, or printing notations mode, or about turning such equational statements into diagrammatic form, or turning such command into TeX-rendered forms, etc. In particular, it is clear that most of the work is to be done on the standardized part of the communication vs on specific proof-assistant features? |
|
@gares Roughly how long might it take someone who knows both CoqIDE and coq-lsp to do the conversion? Given that there's no internals documentation for either AFAIK, it could take much longer for someone who has less experience to reverse engineer the code so they could do the port. I'm all for simplifying, but that may not be the quickest path to move to coq-lsp because you have to convince yourself that each simplification is valid (keeping the same behavior, or has acceptable change) and it all needs to be tested. @Zimmi48 It would be helpful to outline the steps and time needed to setup CoqIDE in a separate repo and to do periodic releases as well as what transitional support would be available (and not available). I wouldn't want to spend a lot of time learning all the ins and outs of this and diagnosing build system problems. |
|
From the Coq Call, I noted that we could ask candidate volunteer maintainers what their roadmap for CoqIDE would be (if they have one).
Sure, but something to keep in mind is that making CoqIDE evolve is not just about reviewing and merging improvements, but also maintaining them longer term, so with each non-trivial PR that you accept to merge, there is an associated time commitment.
I agree with the point raised. I would go further. If we aim to present the Coq Platform as the standard way of using Coq, then its documentation needs to be as good and as accessible as the one of coq-core / coq-stdlib. But this is going to be difficult, so the first step would be to create a page for each Platform version that points to a (preferably versioned) documentation for the included packages (hosted on their own website to start with, and using whatever format they prefer). Keeping CoqIDE's documentation in the Coq repo would probably make it more difficult for maintainers to improve it, so maybe not such a good idea.
I've added a "blocker" tag on this PR, so this should be handled by 8.18, and so, before the CoqIDE split.
I don't know the answer to this question, but I hope that there will be good documentation, and even if there isn't, looking at the commits porting, e.g., Coqtail from coqidetop to LSP (when this happens), could give clues how to proceed to port CoqIDE (of course, more work will be needed, because basic LSP client stuff will need to be written, but this could be done using standard LSP documentation).
The split should not require too much work. The main piece of work will probably be to decide on the exact list of issues to transfer to the new repository. Regarding what transitional support would be available, the CEP tries to make this clear, but regarding the releasing process, I think this should be relatively easy thanks to the use of standard technology and the support of Coq-community admins / members. |
|
|
||
| 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? <add link to this CEP here>
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.
How about reformatting the entire document so all the lines are of a reasonable length, e.g. 80 characters max?
You should probably read the CEP using the Markdown renderer (e.g., the link in the top post).
And adding the link to this CEP?
<add link to this CEP here>
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 don't see any point of pre-formatting the CEP appendix right now.
I suggested reformatting the entire document, not just the appendix
I’m not in need of encouragements actually (I might even dislike it because I feel it’s often condescending); I just need to see that the project evolves in a way that interests me. You seem to have objectives very close to mine so this should not be a problem. Your behavior with me so far was very good: you say what you think, authentically, whether it is for or against my change, which gives me the ability to argue. This is what I need. Note: actually, one can take care to encourage while being authentic, if for some people authenticity is not in itself encouraging.
I would like to have the power to do such a maintenance on my own, on a good and successful project dealing with ergonomics problems. That would be very cool. I sometimes leave some annoying bug though… Couldn’t we use Coq to prove/certify CoqIDE 😁? Should we already post our roadmaps? I don’t expect to become a maintainer of CoqIDE so soon, but I suppose it can be useful to know that I would like to invest time in the project and how. |
I could readily jot down a number of worthwhile CoqIDE specific improvements, but I don't think any of them are particularly high on my personal priority list. Probably I wouldn't submit any such improvement PRs for a year or more from now. At the moment, I'd like to make progress on the debugger, which will need incidental changes to CoqIDE such as adding new menu items. The current reviewers seem uninterested in working with me. I'd say the second phase has been delayed 18 months (6 months waiting to learn if the first phase would ever be merged and 12 months after it was merged). I'd rather not abandon that project but eventually one has to move on. If in the future I want to make a significant Coq UI enhancement for (potential) use across all GUIs, I would evaluate whether CoqIDE or vsCoq2 is the best development platform for it at that time. An example: a refactoring framework implemented in Coq proper that needs GUI changes to access the functionality.
Some commitment, yes, but I think the nature of that commitment should be considerably more nuanced than your brief comment. Generally the submitter should be expected to fix their own problem. If the commitment was open ended then all Coq bugs would have been closed a long time ago. :-)
A good step. My usual rule is that blockers should take precedence over almost any other development task. A very common approach in industry, BTW.
I was hoping to hear from @gares on this one. I think the prerequisites would be a successful conversion by another GUI, perhaps coqTail and agreement that coq-lsp is relatively complete. coq-lsp would also need to support the equivalent debugger messages--maybe that's trivial, maybe it isn't.
My first thought would be to do so in lock step with Coq releases, which would also facilitate keeping CoqIDE doc in the main repository. I'm not sure I'd bother making CoqIDE support multiple versions of Coq--at least not as a first step. Of course, we could deviate from/re-visit this when there is a reason to do so.
Mostly. However, a decent GUI review may frequently require the reviewer to build and hand-test the changes. This includes considering usability and whether the changes will play nicely with existing features (which should be documented!). |
If you like, but probably as a new issue. After discussion, we might want to combine multiple individuals' lists into a consensus list. |
text/068-coqide-split.md
Outdated
|
|
||
| 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. | ||
|
|
||
| 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/). It is possible that Frama-C or Why3 decide to similarly prioritize VS Code support and stop contributing to the lablgtk ecosystem. |
There was a problem hiding this comment.
For Why3, that is not the case. (And neither it is the case for Frama-C, as far as I know.) The thing is, in addition to the actual WhyML code, the user can also manipulate a large blob of data, the so-called proof session. So, while there is a VSCode interface, since it only sees the WhyML code and not the proof session, it is severely crippled compared to Why3IDE. For an accurate analogy, you can imagine a version of Coq where only one single tactic would be available: easy. One can go quite far that way (this is also the approach followed by the HTML interface of Why3 and it has proved to be quite effective for education purpose), but that is not what we want for Why3.
I don't know. Predicting how long it takes to operate a change to piece of software is not one of my skills, I'm sorry. It looks kind of magic to me, I really don't know how people manage to guess right. |
Yes, it certainly would be useful to anyone looking to become a CoqIDE maintainer. So, as part of the call for volunteer maintainers, we could also encourage people planning to contribute actively but not as maintainer to make themselves known and to share their own personal roadmaps if they have one (in the relevant issue thread when it is created).
I would in fact argue that making CoqIDE support multiple versions of Coq would be a trivial task that would greatly facilitate the release management of CoqIDE. For instance, at the current time, we have to release a new CoqIDE version for each patch-level release of Coq (and this is a hassle, as @palmskog can testify, since he's the one who has handled most of the opam packaging lately). Supporting multiple versions of Coq would mean that new patch-level release of Coq wouldn't require new releases of CoqIDE (as for any other Coq package). And even some major releases of Coq might not require new releases of CoqIDE (this frequently happens to be the case for VsCoq or for Coqtail, I believe). Another benefit of decoupling the release process is that new UI features that didn't require changes in Coq could be released quickly and that bug fixes could more easily be applied across multiple Coq versions (if the fixed CoqIDE support these versions). |
I think it is neither fair or true to state that "@ejgallego broke CoqIDE tooltips in December", tooltips in CoqIDE are already severely broken in 8.16, due to incorrect code in the debugger PRs. It is true that while trying to correct some of the serious issues introduced by the debugger PR I made some cases worse, but also some cases better. The fix for master is #17382 by the way, and it seems it needs a little bit more fine tuning but should be ready soon. It is also not fair to assert that we haven't submitted a fix to master, we just did submit a different fix, which after discussion with @herbelin deemed better than the code in 8.17. |
ocaml-lsp does include a full-fledged client library; coq-lsp does include some useful bits too. |
It's a fair statement. There were some corner cases in the tooltips that were incorrect in 8.16, some of which we had not considered. But your December commit made all tooltips disappear, a big step backwards. The problem is that the change relied on using a line number value that the protocol didn't send to CoqIDE. You can readily observe that tooltips are missing by comparing the same script in 8.16 and master. Try Pff.v. 8.16 has tooltips for warnings on lines 107, 241, 243 and hundreds more. master shows the same warnings in the Message panel but does not show any tooltips.
This hasn't been merged and, as you know, I tested that code and pointed out several cases it didn't handle correctly (the same ones we discussed earlier). It's not done until it's correct and merged. "submit" is not so significant. Everyone makes mistakes in their PRs. IMO I should take first responsibility for fixing problems I create. I don't understand why you refuse to take the good fixes (that work!) I produced at least as an interim step. I don't mind if you want to rewrite them shortly thereafter provided your version also works, but leaving master (still) broken for 4+ months and (I think) delaying 8.17 several months waiting for a fix is a very poor way to handle this. I've assumed that you want to spend less time maintaining CoqIDE. If so, your bug fixing strategy makes even less sense to me: why bother rewriting a CoqIDE fix that works? Surely there are other things you'd rather work on, such as coq-lsp. |
|
Will coqbot be available if CoqIDE is in a separate repository? If not, we'd have to go back to the bad old ways of merging :-(. @palmskog Just curious, how troublesome is it to package CoqIDE for each Coq release? |
|
@jfehrle the main problem with opam packaging of CoqIDE is that the testing on CoqIDE is very lightweight, so for the last 3-4 releases, there have always been missing dependencies or dependency bounds that are discovered by the OCaml opam repository's nitpicky CI. These bounds/dependencies can take several days of real time to resolve, since each complete CI run in the OCaml opam repository can take hours. |
|
@palmskog Would these issues vanish if CoqIDE is in a separate repository? How much clock and developer time might it take to package CoqIDE if it's in a separate repository? The "missing dependencies or dependency bounds" refer to issues in linking to code that's in Coq proper? I've no idea what "dependency bounds" are nor do I see how "the testing on CoqIDE is very lightweight" would have a bearing on opam packaging. The latter sounds related to run time errors, which seems unrelated to opam. |
Most people are poor guessers. We used to use a rule of thumb that you take the engineer's estimate and double it. And there usually things that are impossible to predict (e.g. the number of GTK bugs you'll have to overcome). I should have asked you how difficult it will be to switch over from Thanks. |
|
The stm2 lives in the vscoq2 repository, it does speak LSP. @ejgallego knows an lsp client written in ocaml, I guess he is in a better position to guess how hard would it be to integrate it in CoqIDE. |
|
FTR, stm2 is just jargon, you won't find a file named like that. |
We can make any feature of coqbot that you'd like available for the CoqIDE repo, but what do you mean by "go back to the bad old ways of merging"? If you mean using the merge script, then I would suggest not to, and simply using GitHub's merge button. It is too limited for our usage in Coq (e.g., it cannot check that a PR has the right labels / milestone, unless you implement a GitHub Action that transforms this information into a status check), but it should be fine for a smaller project like CoqIDE.
They clearly wouldn't. However, decoupling the CoqIDE release process from the Coq release process would:
|
@jfehrle since I don't use CoqIDE, I'm not very interested in packaging it on opam, yet we need to package it every time there is a Coq release, even for minor releases. This takes lots of time away from more important Coq ecosystem matters. CoqIDE depends on a complex set of GUI-related bindings available in the OCaml opam, such as the package |
I had no idea. Calendar time on the order of days per release, requires intermittent developer attention for the duration but mostly running very long scripts?
IIUC from time to time there are new versions of packages such as
How hard would it be set up testing for additional versions? Could a focused effort upfront make it easy to manage going forward? Perhaps that should be done whether we split off CoqIDE or not. (The list of combos would also need updating from time to time.)
Nothing automated. It would require lots of instrumentation in GTK. |
CoqIDE packages/releases submitted to the OCaml opam repository typically take 2-3 calendar days to get merged, with some taking up to 5-6 days and some only a single day. Each repository CI run can take several hours, and 3-5 package adjustments and discussion have been needed recently.
Yes, new GUI-related bindings get released and they are typically not taken into account by Coq's CI. I only handle the build errors as part of packaging, since I don't use CoqIDE. For all I know, there might be runtime errors as well, but this is not on the packager's table (but rather the Coq release manager and the Coq Team in general).
You could emulate the OCaml opam repository by testing opam dependency package downgrading, e.g., trying to downgrade |
"[lack of] interest" meaning no one wants that to exist? The delay issue could be addressed by making it something that's started manually, akin to the full CI/short CI distinction in coqbot. If no maintainers step forward, the current version of the CEP says we'll continue with the status quo, though with fewer (if any) CoqIDE code changes. In that case, wouldn't it make the packager's life easier to have such a set up?
What sort of things are discussed? Does it get to be a deep discussion? Hopefully these are not complex discussions and some of the participants would continue to advise. |
|
@jfehrle discussions are typically about why some OCaml opam CI job fails. Personally, I don't think it's worth the trouble to put engineering effort into fine-tuning Coq's CI for CoqIDE, given the Coq Team's view of CoqIDE's future. Since opam packaging falls outside the scope of the Coq release manager's tasks, volunteer packagers like myself may simply decline to package CoqIDE going forward. |
Surely they would, as I expect most of them being opam-repository maintainers. |
text/068-coqide-split.md
Outdated
|
|
||
| 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.
It is not part of LSP.
Vscode supports it.
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.
|
It seems to me that the discussion has settled and that it would become time to merge. Please speak up if that's not the case. Otherwise, I intend to put merging this CEP at the agenda of the next Coq Call. |
Following discussion at the Coq Call.
|
We've pushed one final last minor clarification to the CEP text following the discussion at the last Coq Call (notes: https://github.com/coq/coq/wiki/Coq-Call-2023-05-23#coqide). We will give a few more days for any last comments and merge next Tuesday. The call for volunteers will be prepared and sent at the end of next week. |
|
Merging as announced. |
There was a problem hiding this comment.
Thanks for the CEP Karl and Théo, I'm not the target audience at all so I'm unsure how it reads, but for sure it seems pretty helpful and accurate.
From the point of view of an IDE creator, I'm unsure the CEP does address the key problems that have been holding back IDE development for Coq, in particular the large list of technical problems that the API have and the development methodology in terms of interfacing with a reactive system.
While the CEP does encourage the new maintainers to feel free about technical choices, this is not something that can be done independently of Coq, on the contrary, even little details such as the internal Coq IO interface are relevant to the IDE developer. So coupling is high.
I think that in order for an independent IDE effort to work out, Coq needs to provide to their developers a clear view of the UI interfacing methodology that will be available to them, and maybe this CEP (accurately) reflects that as of today Coq's setup seems pretty confusing.
For completeness I'd mention the two previous efforts to make CoqIDE independent, which didn't come to fruition:
|
|
||
| - 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. | ||
|
|
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:
- the transport layer, in this case some custom XML
- the interaction model, which determines what actions / responses are available to clients.
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 newtip, I guess based on Isabelle's PIDE changes, but that model was buggy and was never fully usable, even if jsCoq uses it with some success]
| [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). | ||
|
|
There was a problem hiding this comment.
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.
| - 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. | ||
|
|
||
| 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.
Where is the "strategy of the Coq team" written down?
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.
|
|
||
| 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. | ||
|
|
||
| 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.
some users still prefer a standalone IDE for Coq, and some are motivated to contribute to CoqIDE
Is this data taken from the survey?
There was a problem hiding this comment.
Is this data taken from the survey?
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:
If no maintainers are found, CoqIDE sources will be kept in Coq's repository and minimally maintained until their eventual removal.
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.
|
|
||
| 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.
|
|
||
| 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.
@Zimmi48 I think we can merge without having another formal process.
Huh? This CEP has already been merged.
| 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. The decision to remove coqidetop will be made after first evaluating whether all the important features that the Coq team wishes to continue supporting have been made available in other IDEs or through other IDE-related protocols. At this point, it will then become time for CoqIDE maintainers to decide what to do regarding the long-term future of CoqIDE. Several options will be available: | ||
|
|
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.
| - keep maintaining coqidetop in the CoqIDE repository 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.
| - 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. |
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.
|
|
||
| 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. The decision to remove coqidetop will be made after first evaluating whether all the important features that the Coq team wishes to continue supporting have been made available in other IDEs or through other IDE-related protocols. At this point, it will then become time for CoqIDE maintainers to decide what to do regarding the long-term future of CoqIDE. Several options will be available: |
There was a problem hiding this comment.
To make things more concrete, it would help to have a list of concrete "important features" that we think matter.
There was a problem hiding this comment.
This was also asked by Jim, but since this CEP is kind of a commitment of the Coq team, I didn't know if we could get an explicit consensus of the team at this point on what these important features are. This can always be solved by another PR adding this explicit list to this CEP, where we can ensure that we have consensus on this list.
There was a problem hiding this comment.
@herbelin Absolutely, the team should come up with a list of important IDE features and rank them by difficulty and expected benefit to users. And we should do that for the other parts of Coq. But not in this CEP :-).
There was a problem hiding this comment.
Yup, that's very important, what methodology you folks have in mind to make such a list?
There was a problem hiding this comment.
Ah, think before writing, get feedback from others. Mostly based on our experience with GUIs for all kinds of things.
This is mostly due to a lack of documentation. Learning how to change the GUI from the source code was not that difficult, but it took a long time, Dealing with the GTK limitations was the most difficult part--though it would help to have good notes on things that are known to work well. |
I agree that this is a documentation problem, however we havent' decided a methodology for many technical issues (exn handling, state handling, etc...) which are critical parts of the API that a reactive system needs, so indeed it is not easy to document something that we haven't agreed upon yet. |
Rendered