Enrico Tassi (Mar 31 2023 at 18:19): Enrico Tassi (Mar 31 2023 at 18:19):Serapi is deprecated. I don't know which are the plans for alectryon.
Karl Palmskog (Mar 31 2023 at 18:35):Clement said he would update Alectryon to not rely on SerAPI, but not sure when that will happen. Would be unfortunate if projects with Alectryon documentation generation are left hanging in 8.18, for example.
Ali Caglayan (Mar 31 2023 at 20:17):The only reason serapi (mind you not serlib) is deprecated is because all of its functionality is subsumed by coq-lsp. Alectryon would most likely move to using coq-lsp.
Karl Palmskog (Mar 31 2023 at 20:19):that's what I would expect too (Alectryon moving to coq-lsp). But I'm asking core to please not drop STM until this happens, in particular so we can keep Hydras & Co. and its autogenerated book going (https://github.com/coq-community/hydra-battles). Many other projects are using Alectryon too, of course.
Enrico Tassi (Apr 01 2023 at 12:09):I'm maintainer of the STM and I use Alectryon for coq-elpi. So I won't let it die, don't worry.
Enrico Tassi (Apr 01 2023 at 12:14):Said that, I don't believe a single minute that this is true:
Ali Caglayan said:
all of its functionality is subsumed by coq-lsp. Alectryon would most likely move to using coq-lsp.
So IMO @Clément Pit-Claudel should try to speak to Coq directly. Alectryon is becoming too widely used to rely on many intermediate projects. Or at least, the risk looks too high to me.
Paolo Giarrusso (Apr 01 2023 at 18:10):You doubt coq-lsp, or Alectryon having resources for migration?
Paolo Giarrusso (Apr 01 2023 at 18:10):(I guess the latter, but your message seems to imply the former)
Enrico Tassi (Apr 01 2023 at 21:00):I think an lsp server and serapi are very different things, one is geared toward interaction, the other is more low level. Both depend on serlib which depends on ppx and manual labor to stay in sync with Coq.
I doubt migrating is a good time investment, over developing an ad hoc link to Coq. But this is just my feeling, I only have a high level understanding of the requirements of Alectryon.
Enrico Tassi (Apr 01 2023 at 21:04):What is not true is that coq-lsp subsumes serapi. If it was true then the porting would be trivial. Reading the relevant streams suggests otherwise.
Emilio Jesús Gallego Arias (Apr 02 2023 at 21:13):Enrico Tassi said:
Said that, I don't believe a single minute that this is true:
Ali Caglayan said:all of its functionality is subsumed by coq-lsp. Alectryon would most likely move to using coq-lsp.
What makes you believe that is not true?
Emilio Jesús Gallego Arias (Apr 02 2023 at 21:14):Indeed the porting is very easy, as I discussed with Clément, other than the usual annoying change from sexp to yojson, etc...
Emilio Jesús Gallego Arias (Apr 02 2023 at 21:17):I think an lsp server and serapi are very different things, one is geared toward interaction, the other is more low level. Both depend on serlib which depends on ppx and manual labor to stay in sync with Coq.
I'm unsure what is the story for a general lsp server, but in the case of coq-lsp, it is the direct successor of SerAPI. There is nothing preventing coq-lsp to provide lower-level APIs and in fact it does.
serlib is almost an optional dependency, but required if your use case needs seralized ASTs, or you want to enable some advanced Ast analysis, without that analysis incrementality is much worse tho, but serlib is far from an essential part of coq-lsp , and also of SerAPI
Emilio Jesús Gallego Arias (Apr 02 2023 at 21:19):Moreover serapi is in maintenance mode, which is a bit different from deprecated, but that's just a technicality
Jim Fehrle (Apr 02 2023 at 21:21):@Karl Palmskog What is the rationale for deprecating Stm?
Karl Palmskog (Apr 02 2023 at 21:22):you'll have to ask Enrico for specifics, but what I've heard consistently is the maintenance burden (from a design that I believe is now 10+ years old)
Jim Fehrle (Apr 02 2023 at 21:49):IIUC Enrico is creating a new Stm. (I've no idea what that entails or if that's correct.)
Emilio Jesús Gallego Arias (Apr 02 2023 at 23:06):@Jim Fehrle the rationale for moving on from the current stm implementation is mainly due to us realizing back in 2017/2018 that the scope of changes that would be needed bascially amounted to a rewrite.
A rewrite did start in 2019 with coq-lsp, using the ideas that were developed for a different system (lambdapi) and all that I learned while hacking many hours in the Stm, but it stalled till summer 2022 when we decided to revive it, and now you have a document manager Fleche, which servers the role of the Stm, coq-lsp is then just a thin layer over Fleche.
Another concurrent document manager effort was started in https://github.com/coq/coq/pull/12461 which I believe to be now the basis for the document manager in the vscoq repos.
I think Stm is too specific of a terminology, I propose to use Document Manager.
What does it entail to replace the current Coq document manager? Indeed I feel that there is no consensus about the concrete definition there, as at some point you need to fix some design choices and there is a large space in these terms.
Flèche is opinionated in the sense Coq itself is seen as a library providing state and command management. Then Flèche defines a simple interpreter over this algebra, which is then enriched using algebraic effects to provide some interesting features. This has several advantages, in particular if you remove the effects you get what we called "the simple compiler", so the code is fairly straighforward and in a concrete sense, modular.
Emilio Jesús Gallego Arias (Apr 02 2023 at 23:09):This approach is also very dynamic, meaning that it is rare for the document manager workflow to impose restrictions on the downstream API as long as the downstream API is functional and sound w.r.t. chosen semantics of commands
Ali Caglayan (Apr 02 2023 at 23:26):Enrico Tassi said:
Said that, I don't believe a single minute that this is true:
Ali Caglayan said:all of its functionality is subsumed by coq-lsp. Alectryon would most likely move to using coq-lsp.
So IMO Clément Pit-Claudel should try to speak to Coq directly. Alectryon is becoming too widely used to rely on many intermediate projects. Or at least, the risk looks too high to me.
BTW this is what I was talking about with respect to subsumation. Here is a migation guide: https://github.com/ejgallego/coq-lsp/blob/main/etc/SerAPI.md
Jim Fehrle (Apr 02 2023 at 23:47):@Emilio Jesús Gallego Arias Is there any documentation of fleche? Weren't you going to make the slides you presented a month or two ago in the UI meeting available?
Emilio Jesús Gallego Arias (Apr 02 2023 at 23:49):I actually wrote a paper for ITP but had to redo a lot of stuff, so I pulled it out. I'm glad I did as the paper seems in much better shape now, so I hope to upload it to ArXiV this week as I'm finally submitting it.
Emilio Jesús Gallego Arias (Apr 02 2023 at 23:51):So yes I'm late with that, but I think I'll be done soon. Once I put the paper, I will do a pass on the slides, there was some outdated info.
I will link to all the docs from the Fleche repos, as IMHO the desing for 1.0 has finally (even if only recently) converged.
There is also regular doc in Fleche repos, including the structure of the project, the OCaml API, etc...
Main entry point is https://ejgallego.github.io/coq-lsp/coq-lsp/Fleche/Doc/index.html
Enrico Tassi (Apr 03 2023 at 11:38):Emilio Jesús Gallego Arias said:
Moreover serapi is in maintenance mode, which is a bit different from deprecated, but that's just a technicality
I heard you say deprecated, sorry if I misunderstood.
Enrico Tassi (Apr 03 2023 at 11:43):Emilio Jesús Gallego Arias said:
I think an lsp server and serapi are very different things, one is geared toward interaction, the other is more low level. Both depend on serlib which depends on ppx and manual labor to stay in sync with Coq.
I'm unsure what is the story for a general lsp server, but in the case of coq-lsp, it is the direct successor of SerAPI. There is nothing preventing coq-lsp to provide lower-level APIs and in fact it does.
serlibis almost an optional dependency, but required if your use case needs seralized ASTs, or you want to enable some advanced Ast analysis, without that analysis incrementality is much worse tho, but serlib is far from an essential part of coq-lsp , and also of SerAPI
Let's take a concrete example. A client like Alectryon needs to know where sentences begin and end, so that it can implement a an action when the text is clicked.
The LSP protocol has his virtue in being language agnostic, there is no notion of sentence and indeed the client sends raw text. With the protocol API I see in the standard, including the extra message for goal display you document in coq-lsp, I don't see how one gets this piece of info.
Enrico Tassi (Apr 03 2023 at 12:02):Jim Fehrle said:
IIUC Enrico is creating a new Stm. (I've no idea what that entails or if that's correct.)
A mistake I made was to put the STM inside Coq, rather than in the UI. The new STM is the document manager of vscoq2, i.e. the LSP agnostic part of the language server. It is not just me, Maxime wrote a big chunk of it. I did most of the plumbing for proof delegation etc.
Having the STM in Coq made it more complex, and paved the way for a few features which did never took off, like .vio (or .vos).
These can be implemented independently of the STM, and probably in a simpler way these days.
Paolo Giarrusso (Apr 03 2023 at 12:03):Would dropping the STM also drop vos files? That'd also be unfortunate...
Karl Palmskog (Apr 03 2023 at 12:03):if you hadn't put the STM inside Coq, I don't think we could have done any reasonable machine learning / code analysis research in Coq the last few years - seems hopeless to work directly with the UI for that
Enrico Tassi (Apr 03 2023 at 12:06):Paolo Giarrusso said:
Would dropping the STM also drop vos files? That'd also be unfortunate...
Today's implementation depends on the STM, but as I was saying "skipping proofs" can be implemented in a much simpler way today. Again, don't worry, I'm only explaining a long term plan.
Enrico Tassi (Apr 03 2023 at 12:08):Karl Palmskog said:
if you hadn't put the STM inside Coq, I don't think we could have done any reasonable machine learning / code analysis research in Coq the last few years - seems hopeless to work directly with the UI for that
One thing is a component which implements the STM APIs. Another thing is to use them also for the basic coqc.
Having the component "in Coq" but not used by what we consider the TCB (but only by the UI or other tools) would have resulted in a simpler design.
Enrico Tassi (Apr 03 2023 at 12:13):Eg, I had to make the kernel aware of "async proofs", but the level of safety has never been on par (eg universes).
If you only need .vos, you can just use the codepath for Admitted, which was there even before the STM, no need to change the kernel.
Internally, this mistake was mostly reverted (thanks to Pierre Marie), see https://github.com/coq/ceps/blob/master/text/040-no-delayed-opaque-proofs-in-kernel.md (just in case).
Emilio Jesús Gallego Arias (Apr 03 2023 at 16:12):Enrico Tassi said:
Let's take a concrete example. A client like Alectryon needs to know where sentences begin and end, so that it can implement a an action when the text is clicked.
The LSP protocol has his virtue in being language agnostic, there is no notion of sentence and indeed the client sends raw text. With the protocol API I see in the standard, including the extra message for goal display you document in coq-lsp, I don't see how one gets this piece of info.
That's why we implemented coq/getDocument at Clement's request, some use cases have arisen for a coq/getSentence so that'll land soon in main. But indeed both inherit the limitatons of SerAPI sentence-based model, so more discussion is needed to hopefully achieve a better integration (and address other open concerns)
Clément Pit-Claudel (Apr 04 2023 at 06:17):Sorry folks that I haven't looked very deep into this.
I'm planning to allocate roughly one week this summer to port Alectryon to the LSP server. LSP is much more painful to interact with than SerAPI (mostly because there is no good LSP client for Python and because incremental processing is more complicated), but I added experimental support for Dafny through LSP recently (so at least the base protocol parts are done) and I added one-shot whole-document processing not too long ago for Lean (so I won't need to rely on incremental support).
I'm not sure whether coq-lsp now has all the required support yet. When @Emilio Jesús Gallego Arias told me about SerAPI going potentially away a few months ago we looked at what was missing in coq-lsp for the port and identified a few things; more may pop up once I actually try my hand at a port. The main blockers when we first looked where structured goals (not text), breaking the document into sentences, and pull diagnostics (to know when the document finishes processing).
Emilio Jesús Gallego Arias (Apr 04 2023 at 11:14):Thanks @Clément Pit-Claudel for the summary, as of today you got the 3 things you mention in place, tho both structured goals and breaking the doc into sentence use extensions to LSP.
What makes the incremental support more complex in LSP tho?
I discussed with Ali (and also noted in the migration guide) about offering a "SerAPI"-like API, it is indeed very easy to simulate the Add / Cancel model on top of Flèche if needed; we did not as we didn't think clients would prefer the old API, but certainly it would be possible; as well as offering Sexp support.
Enrico Tassi (Apr 05 2023 at 12:59):Emilio Jesús Gallego Arias said:
Enrico Tassi said:
Let's take a concrete example. A client like Alectryon needs to know where sentences begin and end, so that it can implement a an action when the text is clicked.
The LSP protocol has his virtue in being language agnostic, there is no notion of sentence and indeed the client sends raw text. With the protocol API I see in the standard, including the extra message for goal display you document in coq-lsp, I don't see how one gets this piece of info.That's why we implemented
coq/getDocumentat Clement's request, some use cases have arisen for acoq/getSentenceso that'll land soon inmain. But indeed both inherit the limitatons of SerAPI sentence-based model, so more discussion is needed to hopefully achieve a better integration (and address other open concerns)
Oh, I did not see all these extra messages you have in addition to the LSP ones. So I guess I was wrong,the data which was previously accessible via serapi is now accessible via non-LSP messages supported by coq-lsp as extensions to LSP. So I guess porting serapi clients to coq-lsp is doable.
At the same time you said many time the serialization code of serapi/serlib was painful to keep up to date w.r.t. Coq internals. This is I why I did not imagine you had used all that in coq-lsp in the first place.
Emilio Jesús Gallego Arias (Apr 05 2023 at 13:07):Yes I thought that LSP + custom would beat 100% custom, tho after some discussion maybe we provide a 100% identical compat layer (including sexp), it is easy to emulate on top of Fleche.
The problem with extensible ASTs is general to any tool that would like to access AST, but indeed, as it was already done, it make sense to re-use it.
Jim Fehrle (Apr 15 2023 at 02:30):Enrico Tassi A mistake I made was to put the STM inside Coq, rather than in the UI. The new STM is the document manager of vscoq2, i.e. the LSP agnostic part of the language server.
What do you mean by "put the STM ... in the UI"? I expect there is a single new STM that will be shared by vsCoq2 and other GUIs. So IIUC the wording "in the UI" is a misleading/can be misinterpreted. (Still waiting to see slides and that draft paper on coq-lsp and Fleche, so I don't fully understand the architecture.)
Jim Fehrle (Apr 15 2023 at 02:35):Is it feasible/reasonable to have plugins define new lsp messages? That might be a useful approach for prototyping or delivering some kinds of new GUI functionality. OTOH it may not be pretty to implement (I have no idea).
Théo Zimmermann (Apr 15 2023 at 10:55):Jim Fehrle said:
Enrico Tassi A mistake I made was to put the STM inside Coq, rather than in the UI. The new STM is the document manager of vscoq2, i.e. the LSP agnostic part of the language server.
What do you mean by "put the STM ... in the UI"? I expect there is a single new STM that will be shared by vsCoq2 and other GUIs. So IIUC the wording "in the UI" is a misleading/can be misinterpreted. (Still waiting to see slides and that draft paper on coq-lsp and Fleche, so I don't fully understand the architecture.)
No, it will not be shared by all the GUIs: it is not used (and will not be used) by coq-lsp based UIs, which depends on Flèche instead. However, it will be used by any of the GUI using VsCoq2's LSP server (vscoqtop).
Paolo Giarrusso (Apr 15 2023 at 12:25)::+1: to Jim's questions... From the sidelines, I can tell "why not merge efforts?" must have been discussed, but it still seems a FAQ that warrants a public answer somewhere at _some_ point. I infer the point is sth like "different groups believe in very different approaches" and maybe "some technical feasibility questions have not been answered"
Paolo Giarrusso (Apr 15 2023 at 12:26):It's not clear to me if the plan is to maintain both efforts long-term, or to pick a winner at some point, or if that's a topic of discussion.
Karl Palmskog (Apr 15 2023 at 12:27):even from just publicly available information, one can deduce that the key people involved in both coq-lsp and VsCoq2 know each other since way back. From there, it's not hard to jump to the conclusion that it's not just a simple matter of "merging efforts", but seemingly fundamental view differences
Paolo Giarrusso (Apr 15 2023 at 12:28):Exactly, I've seen the meta-discussions about the internal talks, since I spend way too much here :sweat_smile:
Karl Palmskog (Apr 15 2023 at 12:29):I've co-authored papers with both sides, and let's just say, for everyone's sanity, forced extensive collaboration [between parties under discussion] may not always work out. (as opposed to, say, finding some common ground here and there)
Paolo Giarrusso (Apr 15 2023 at 12:30):Yeah there's clearly a lot that's not being said. Sooner or later, open-source contributors might ask for some amount of transparency and design rationale? I guess involved people know, it's just strange from outside
Karl Palmskog (Apr 15 2023 at 12:31):for better or worse, Coq has by far the lowest bus factor of any (widely used?) ITP. Lean4 looks like it has the highest, then Isabelle and HOL4 not long after.
Paolo Giarrusso (Apr 15 2023 at 12:33):lowest bus factor = biggest core team? and the link is "this isn't a cathedral development but a bazaar one"?
Paolo Giarrusso (Apr 15 2023 at 12:34):but all I wanted to say: :+1: to Jim's questions, even if I see meta-reasons they've not been answered. And looking forward to Emilio's papers!
Karl Palmskog (Apr 15 2023 at 12:34):it's more bazaarish then others, at least from what I can tell. The size of the team doesn't necessarily determine the bus factor, I think it's more about how decision making and vision and direction gets distributed.
Enrico Tassi (Apr 15 2023 at 14:15):Paolo Giarrusso said:
:+1: to Jim's questions... From the sidelines, I can tell "why not merge efforts?" must have been discussed, but it still seems a FAQ that warrants a public answer somewhere at _some_ point. I infer the point is sth like "different groups believe in very different approaches" and maybe "some technical feasibility questions have not been answered"
Let's say that while I understand the confusion (of having two LSP servers in the works) I don't think they will ever be merged into a single product, even if cherry picking of ideas can be done. A similar question was raised at the last UI meeting (see the UI stream).
If I had to find the most distinguishing difference, I'd say that:
I think the main convergence we should seek is to share the format of the one non-standard LSP message all UIs need to understand: goal printing. In this way "basic" UIs speaking LSP (+ this message) can pick one or the other server.
Karl Palmskog (Apr 15 2023 at 14:24):there seems to be a spectrum with "ITP strongly integrated with a single UI" (think Isabelle) on one hand, and "ITP hardly having an UI" on the other (think emacs buffer only). Coq is somewhere in between, meaning there is constant discussion of what parts of Coq belong where (and the location of something like STM matters a lot in practice)
Paolo Giarrusso (Apr 15 2023 at 14:36):Thank you Enrico! I guess the "Isabelle-style" UX is another major difference. (EDIT: ah right that's what the legacy checking mode is about)
Paolo Giarrusso (Apr 15 2023 at 14:37):And congrats on vscoq2 having permanent funding — that answers another important question
Jim Fehrle (Apr 15 2023 at 17:27):If vsCoq2 uses the new Stm then CoqIDE should share that code.
@Enrico Tassi could you summarize
Enrico Tassi (Apr 15 2023 at 20:04):The old STM was doing 2 things at the same time (using the same data representation, its main architectural flaw I believe):
The "new" stm is not a single component, but a few of them part of the language server of vscoqtop, in the dm/ directory you can find executionManager, schedule/documentManager, delegationManager ...
So, the new STM is a rewriting of the old one, without the mess of mixing too many things in one component, and with the big advantage that now Coq is able to parse without executing. So the two jobs of the old stm are no more intertwined. Here the components: https://github.com/coq-community/vscoq/blob/main/docs/developers.md
The current STM is deprecated because it was proved to be too hard to build an LSP server on top of it (vscoq1), and because its code is messy/entangled. I'm the only maintainer left, it's my baby, I think I have enough reasons to let it go. It had a reasonably clean design, then it had to support all sort of corner cases, and it grow into a mess.
The last question is delicate. LSP is much simpler to implement for UIs than the previous protocol. But CoqIDE main problem is that you don't want to program an editor yourself, you don't want to do it on obsolete technology, you don't want to do it in a niche language, you don't want to do it with limited resources. I've been saying that CoqIDE should have never existed before LSP was invented, it makes no sense to write such a piece of software: if you have a protocol (no matter which one), put on the UI side something that exists already, that you don't maintain, that works!
Enrico Tassi (Apr 15 2023 at 20:06):To be honest with history, at the beginning there was no protocol between CoqIDE and Coq, they were a single binary. Then a good step was made to separate the two. Then, instead of realizing the original mistake (not using a protocol to connect it to a third party editor), we kept the thing alive.
Karl Palmskog (Apr 15 2023 at 20:09):ironically, LCF's 1970s REPL loop lives on as all UIs die around it
Enrico Tassi (Apr 15 2023 at 20:12):The bad idea was to consider a REPL as a "protocol" to build a UI on top. A REPL is a very useful tool, as a hammer is. But if you need to put a screw... it may not be the best tool.
Jim Fehrle (Apr 17 2023 at 21:57):@Enrico Tassi Why does the old Stm have to be removed, forcing significant work on CoqIDE (or killing it entirely)? Despite its limitations, CoqIDE is useful as a simple interface and it's the only one that can currently be installed with opam/coq platform.
If it must be removed, can CoqIDE interface to the new Stm (perhaps with modest changes) even if it keeps the current XML protocol?
But CoqIDE main problem is that you don't want to program an editor yourself, ... you don't want to do it in a niche language, you don't want to do it with limited resources.
To quibble: The CoqIDE text editing code is from a library, it's not our code, so not sure what you mean. I agree OCaml is not a great match for GUI development because of some feature limitations. Resources are always limited--maybe you mean "inadequate resources"?
I think we should keep CoqIDE around and fix just a few of its limitations. Redoing any of the plumbing (Stm, protocol) is not something I want to waste time on. Perhaps we can find some time to chat about this at the CUDW. Diving into it in Zulip is not likely to be fun.
Enrico Tassi (Apr 18 2023 at 12:41):It does not have to be removed. We can move it to the CoqIDE folder. But we are also discussing to move CoqIDE out the main repo eventually, so its maintenance cost is lifted from core dev.
I think I repeated it may times already: we will do that when the alternative(s) will be real, since then it sill stay (the STM).
Enrico Tassi (Apr 18 2023 at 12:42):fix just a few of its limitations.
I think core devs made it clear that do not want to invest time on CoqIDE. It should be considered frozen as Ltac1 was waiting for Ltac2.
Karl Palmskog (Apr 18 2023 at 12:44):from Coq-community side as a potential host for the split-off CoqIDE, I'd very much like to avoid having a project that hosts both CoqIDE-the-UI and STM. The reasonable thing to do is to keep STM in Coq even after CoqIDE is split, but put STM on ticking clock before removal from Coq
Karl Palmskog (Apr 18 2023 at 12:46):it's very, very unlikely we will find someone who can, and agrees to, effectively maintain both CoqIDE and STM
Jim Fehrle (Apr 18 2023 at 16:58):fix just a few of its limitations.
I think core devs made it clear that do not want to invest time on CoqIDE.
That's not entirely clear. I'm not expecting others to create fixes. And I do want to finish up the debugger, which I don't plan to personally port to other GUIs myself (though very happy to consult).
Théo Zimmermann (Apr 19 2023 at 09:11):That should be made clearer, and the CEP proposing the split (on which we plan to discuss tomorrow with Karl) will help make this clearer. Furthermore, "investing time" for a core dev in CoqIDE is not just about making fixes or changes themselves, but also about reviewing PRs or maintaining APIs that are only needed for CoqIDE.
Last updated: Nov 29 2023 at 22:01 UTC