Maxime Dénès (Mar 31 2023 at 16:33): Maxime Dénès (Mar 31 2023 at 16:33):My personal position is that developing a text editor is not the best use of the Coq devs' time. So we should phase it out in favor of IDEs that make it possible for us to develop only Coq-specific features. It will allow us to get rid of some technical debt related to the STM. I bet it will also lead to a much better user experience. I don't know what the team's position is leaning towards. At least @Pierre-Marie Pédrot expressed a very similar view recently on a PR.
Karl Palmskog (Mar 31 2023 at 16:52):I have a similar view, but I think the proper approach to splitting CoqIDE from Coq itself would be to give the community a chance to pick it up (e.g., via a public call for maintainers). The split-off project would be welcome in Coq-community, and could be archived if it doesn't find maintainers.
Ali Caglayan (Mar 31 2023 at 17:11):We could probably put some effort in to do a split. I think we were hesitant to do this previously since there really was no good alternative for a Coq editor (perhaps apart from PG). Now we have PG, VSCoq2 and coq-lsp I think we can safely put it into another repository.
There is one use case for CoqIDE that we should keep in mind, and is pretty much the entire reason CoqIDE is still alive, and that is for devs to quickly spin up and test .v files when developing Coq. We have to make sure that doing this through alternative editors is good enough.
Maxime Dénès (Mar 31 2023 at 17:15):IMHO VsCoq2 & coq-lsp are not quite ready for us to split right now, but that should be the plan. And the point of recent discussions was that it's probably not worth putting a lot of effort on CoqIDE improvements at this point.
Gaëtan Gilbert (Mar 31 2023 at 17:27):we also want to get coqide to stop depending on the stm by using some lsp
then we can work towards deleting stm
Maxime Dénès (Mar 31 2023 at 17:31):if some external developers want to do it, why not, but I think there are higher priorities for the team TBH
Karl Palmskog (Mar 31 2023 at 17:40):in my book, it would be reasonable to split off CoqIDE even while it depends on STM, then drop STM from Coq itself and ask volunteer maintainers to work towards getting CoqIDE to use LSP
Karl Palmskog (Mar 31 2023 at 17:40):at least assuming that PG, VsCoq2, coq-lsp are still maintained and functional going forward
Maxime Dénès (Mar 31 2023 at 17:45):Karl Palmskog said:
in my book, it would be reasonable to split off CoqIDE even while it depends on STM, then drop STM from Coq itself and ask volunteer maintainers to work towards getting CoqIDE to use LSP
Yes, that's what @Enrico Tassi and I had in mind. The STM could go with CoqIDE when splitting.
Karl Palmskog (Mar 31 2023 at 17:48):on the other hand, if you kill off STM, Alectryon would currently get killed as well (via SerAPI)
Théo Zimmermann (Apr 02 2023 at 17:19):I would do the splitting now (if there are volunteer maintainers, which I think there is) and move coqidetop + the STM to the CoqIDE repository once the other UIs are ready to move to LSP.
Karl Palmskog (Apr 02 2023 at 18:12):for the record, we have VsCoq1 as a dependency of coqidetop as well, so good to take that into account
Jim Fehrle (Apr 02 2023 at 20:39):I can make the Tuesday meeting.
CoqIDE would benefit from being split out from the Coq repository / release management process
Really? I expect it would mean more work for CoqIDE maintainers and would be less convenient for users. Let's try not to kill off CoqIDE. Isn't the real motivation to simplify the Coq repository? Who would maintain Stm?
Karl Palmskog (Apr 02 2023 at 20:47):Who would maintain Stm?
If you look here and here, the general plan is to remove the STM and let IDEs use alternative ways to interface with Coq, e.g., LSP servers. CoqIDE would need extensive changes for this, which would be best done in a standalone project. If CoqIDE doesn't find enough developer interest for an "LSP port", it will cease to work when STM disappears from Coq.
Michael Soegtrop (Apr 03 2023 at 07:24):Maybe we should also make a list of features CoqIDE has not yet available in VSCoq and PG. Such a split has a certain risk that CoqIDE becomes less usable in the future and we should evaluate if this could have bad effects on Coq users.
The only reason I am using CoqIDE these days is Jim's Ltac debugger. All new stuff I write is reflective / Ltac2 / Elpi, but I still use it quite frequently to analyse non trivial Ltac code from others (VST). Jim's Debugger is here very helpful in porting Ltac to newer methods.
In the past I also used it for compute intensive proofs to use parallelism, but this meanwhile also works in VsCoq.
What are other vital features in CoqIDE people need?
Pierre-Marie Pédrot (Apr 03 2023 at 08:32):From the Coq dev side, we need to ensure that vscoq is apt at handling borderline situations, like e.g. when the stdlib doesn't even compile. Notably we should be able to modify the Coq prelude from vscoq in a simple way.
Rodolphe Lepigre (Apr 03 2023 at 08:41):I naively thought one could use dune coq top for that, since I think it would automatically pick coqtop from the repo. Would something like that not be good enough? (Assuming some built-in support in editors.)
Pierre-Marie Pédrot (Apr 03 2023 at 09:50):You need to pass the -noinit flag somewhere. I guess my question boils down to whether it's not too messy to hack with the internals of the vscoq plugin to achieve this.
Gaëtan Gilbert (Apr 03 2023 at 10:16):I think -noinit isn't enough, you also need to pass -coqlib to the installed files (eg Logic depends on Notations so it needs the right path) and maybe -boot to avoid checking for the existence of Prelude.vo
the _CoqProject makes it pass -noinit btw
Michael Soegtrop (Apr 03 2023 at 10:21):@Pierre-Marie Pédrot : In VsCoq one can pass arbitrary command line arguments to coqtop. HoTT and UniMath appear to work in VSCoq (I did only do trivial smoke testing, though). It also picks up such options from _CoqProject (if it finds it), so it is reasonably comfortable.
Rodolphe Lepigre (Apr 03 2023 at 10:26):There is a PR by @Paolo Giarrusso somewhere that enables using dune coq top properly, it it would probably not be hard to extend it (if it needs to be) to pass additional flags.
Paolo Giarrusso (Apr 03 2023 at 10:36):As long as dune can build the code, dune coq top is supposed to do the same; users of _CoqProject might require additional hoops since they don't actually give the same semantics in this case
Paolo Giarrusso (Apr 03 2023 at 10:38):My dune coq top patch is working but I haven't found a moment for the last touch https://github.com/coq-community/vscoq/pull/319
Paolo Giarrusso (Apr 03 2023 at 10:41):However, I don't imagine that coq top will deal with dunestrap output? :frown:
Paolo Giarrusso (Apr 03 2023 at 10:43):That patch, BTW, is for vscoq1, but I assume the vscoq2 analog shouldn't be much harder
Ali Caglayan (Apr 03 2023 at 20:33):The dunestrap rules will not work with dune coq top I don't think. However the disabled dune files should still work in the repo, so anytime you want to use them you can just rename them to dune. We test those regularly in coq-universe.
Ali Caglayan (Apr 03 2023 at 20:34):They all handle the -noinit stuff correctly too AFAIK. The only reason we really moved to dunestrap is so we have more control over our rules for things like trying a new native compiler. We haven't actually done any of that yet though.
Emilio Jesús Gallego Arias (Apr 03 2023 at 22:01):We can make dune coq top work with dunestrap actually, but it was a bit hackish, as it involved declaring the stdlib as a theory with no modules
Emilio Jesús Gallego Arias (Apr 03 2023 at 22:01):coq-lsp integrates directly so it does work out of the box
Emilio Jesús Gallego Arias (Apr 03 2023 at 22:01):modulo some missing Dune support
Karl Palmskog (Apr 04 2023 at 16:15):so where will the discussion on CoqIDE split continue? We are prepared to help facilitate a "CoqIDE call for maintainers" in Coq-community, according to our process: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md#proposing-a-new-package
Ali Caglayan (Apr 04 2023 at 16:15):I've psuhed the meeting notes: https://github.com/coq/coq/wiki/Coq-Call-2023-04-04
Karl Palmskog (Apr 04 2023 at 16:17):for the record, I was talking mostly about (the possibility of) improving the CoqIDE automated testing through a split, since the current testing seemingly fails us every time I submit a CoqIDE package on opam-repository
Ali Caglayan (Apr 04 2023 at 16:19):Testing CoqIDE is difficult and restricted by the Coq CI; with a with a split we could test it better
Ali Caglayan (Apr 04 2023 at 16:20):And a key point of the meeting is that we are hoping to split the CoqIDE UI and not coqidetop + STM from the coq repo
Jim Fehrle (Apr 04 2023 at 16:26):I haven't noticed that there are a lot of developers who want to make improvements to CoqIDE (me, Sylvain, ???), let alone refactor the existing code (e.g. change the protocol, go to GTK4 or some other library) or do the added work to do its own releases, documentation, etc. I'm interested in developing/improving user visible features and doing some bug fixes.
Jim Fehrle (Apr 04 2023 at 16:28):Making an externalized version of CoqIDE work with multiple versions of Coq is not a simple change, either.
Karl Palmskog (Apr 04 2023 at 16:34):I think a call for maintainers would be a good way to determine the general interest in CoqIDE in the Coq community, regardless of outcome. The long-term interest in CoqIDE seems pretty modest among core devs.
Jim Fehrle (Apr 04 2023 at 16:36):Ali Caglayan Testing CoqIDE is difficult and restricted by the Coq CI; with a with a split we could test it better
I don't see this, would you elaborate a bit?
Karl Palmskog (Apr 04 2023 at 16:37):we have a CI system aimed at testing Coq code and plugin code, not UI. There's basically no user-level automated testing of CoqIDE at all, to my knowledge. The industry standard is to automate/simulate actions done by users interacting with UI elements
Karl Palmskog (Apr 04 2023 at 16:39):if anyone wants to add this to Coq's CI, they might have to add significant CI infrastructure code and dependencies unrelated to Coq. So unlikely to happen.
Jim Fehrle (Apr 04 2023 at 21:04):I thought the meeting notes didn't capture some important parts of the discussion, so I added comments on the bottom of the notes.
Théo Zimmermann (Apr 05 2023 at 08:40):Jim Fehrle said:
Making an externalized version of CoqIDE work with multiple versions of Coq is not a simple change, either.
It's probably pretty easy when the XML protocol doesn't change between Coq versions, which is most of the time. It actually already works to run a CoqIDE built for a specific Coq version with a different version of coqidetop (for some close versions of Coq). This is not something that you can test in the usual setting, but Nix makes this possible. The only issue is that in this case, CoqIDE doesn't try to detect the version of Coq, and thus doesn't report the correct version. See https://github.com/coq/coq/issues/16521. FTR, I just tested this again with nix-shell -p coqPackages_8_17.coqide coq_8_16.
Théo Zimmermann (Apr 05 2023 at 08:53):Based on the discussion at the Coq Call, I think that most of the team is onboard with splitting the UI part (with Jim being one of the least supportive / most concerned about such a split). Something that seems clear at this point is that while splitting CoqIDE could bring a more agile release process, Jim is not interested in acting as a CoqIDE maintainer / release manager and Sylvain cannot guarantee for how long he plans to be around, so the split would really make sense only if there is interest in improving / evolving CoqIDE beyond the people that attended the Call. So, I concur with Karl's proposal to make a call for maintainer. What we could do actually would be to write a short CEP where we clarify what the split would mean, the advantages and disadvantages that we anticipate for such a split, that we would do it only if there are available volunteer maintainers, and in what conditions we would revert the split if this experiment doesn't work. Personally, and also based on some answers to the Coq Community Survey, I think that there are people that will continue to be more satisfied by a standalone interface than one based on VS Code, and that we should enable these people to take agency in how CoqIDE is set to evolve.
Karl Palmskog (Apr 05 2023 at 09:01):I agree with making a CEP and would be happy to contribute comments from the ecosystem/packaging side.
Karl Palmskog (Apr 05 2023 at 09:02):to give one example, if I knew there were concerned maintainers when something breaks with CoqIDE during opam packaging, that's a big difference from reporting "open Coq issue number thousands + 1"
Théo Zimmermann (Apr 05 2023 at 09:05):Great! I don't expect anyone will take on this job except the two of us, so what about we schedule some time in the not too distant future to prepare such a CEP?
Karl Palmskog (Apr 05 2023 at 09:06):sure, I guess we could even live-write it, yes
Karl Palmskog (Apr 05 2023 at 16:17):one key question in a call for maintainers: what can be promised, or at least best-effort-provided, from core devs and other people in the ecosystem for CoqIDE development after the split?
For example, a basic build could be added to Coq's CI, there could be help in accommodating to XML protocol changes for some time, help in setting up new CI, help in migrating the issues and docs, ...
Maxime Dénès (Apr 06 2023 at 07:09):At least once we manage to split out the STM of Coq, I would strongly oppose to keeping it in the CI.
Maxime Dénès (Apr 06 2023 at 07:11):Otherwise we will gain very little from what would be otherwise a very nice cleanup. Worse, we will have to make cross repo patches as soon as we touch Coq's higher layers.
Maxime Dénès (Apr 06 2023 at 07:12):So my point is we can do some best effort things after this first step split, but we should be explicit about the fact that it will be limited in time.
Maxime Dénès (Apr 06 2023 at 07:13):Another important point is that I expect CoqIDE to be much more difficult to port to LSP once we get rid of the STM than other interfaces based on standard editors/IDE. Those interfaces will be able to benefit from existing LSP modes (for example for vim), whereas for CoqIDE, it will more or less mean a full rewrite of the logic.
Karl Palmskog (Apr 06 2023 at 12:56):@Maxime Dénès but you would be fine with having a basic CoqIDE build in Coq's CI as long as STM is around in Coq itself?
Théo Zimmermann (Apr 06 2023 at 12:58):Yes, from my discussions with Maxime, the real issues would start once the STM is removed from Coq.
Karl Palmskog (Apr 06 2023 at 12:59):then I think we say in the call for maintainers something to the effect that there is a clock ticking on the STM removal, but they can expect to receive updates until that point
Maxime Dénès (Apr 06 2023 at 13:33):Karl Palmskog said:
then I think we say in the call for maintainers something to the effect that there is a clock ticking on the STM removal, but they can expect to receive updates until that point
Yes, that was exactly my point.
Hugo Herbelin (Apr 07 2023 at 08:37):I have a few terminological questions in passing:
Hugo Herbelin (Apr 07 2023 at 08:37):In particular, is it correct to say that we have 4 different servers available (coqtop, coqidetop, the server used by coq-lsp, the server used by vscoq2), each coming with its own protocol (textual over Coq user commands, XML-based over Coq commands and other specific requests, 1st LSP-based over Coq commands and other specific requests, 2nd LSP-based over Coq commands and other specific requests), and that all 4 servers can be used (in theory) with any front-end?
Hugo Herbelin (Apr 07 2023 at 08:38): Hugo Herbelin (Apr 07 2023 at 08:38):Also:
Hugo Herbelin (Apr 07 2023 at 08:38):Are important things missing in this classification?
Hugo Herbelin (Apr 07 2023 at 10:35):Another question: if the STM is not used by either coqtop or coqc (as what told at the call iiuc), could it be linked to only coqidetop (as soon as now)? Or do I miss something?
Gaëtan Gilbert (Apr 07 2023 at 10:38):it is used by coqtop/coqc, however they don't use most of its features so it should be possible to replace it with something simpler
Pierre-Marie Pédrot (Apr 07 2023 at 10:51):relatedly, see https://github.com/coq/coq/pull/16190
Karl Palmskog (Apr 07 2023 at 10:56):another distinction to keep in mind. All the following IDEs have both a VS Code extension and a standalone executable they use to interface to Coq:
coqide-servercoq-lsp?)One persistent issue we have is that people have to get instructions both how to install the VS Code extension and the standalone executable "server" (except in the coqide-server case, where it is included in the coq opam package)
Théo Zimmermann (Apr 07 2023 at 11:29):Hugo Herbelin said:
In particular, is it correct to say that we have 4 different servers available (coqtop, coqidetop, the server used by coq-lsp, the server used by vscoq2), each coming with its own protocol (textual over Coq user commands, XML-based over Coq commands and other specific requests, 1st LSP-based over Coq commands and other specific requests, 2nd LSP-based over Coq commands and other specific requests), and that all 4 servers can be used (in theory) with any front-end?
Yes.
Théo Zimmermann (Apr 07 2023 at 11:30):The LSP executable from VsCoq2 is called vscoqtop AFAIK.
Théo Zimmermann (Apr 07 2023 at 11:33):@Karl Palmskog The name coqide-server is the opam package name, but the name of the executable is coqidetop.
Théo Zimmermann (Apr 07 2023 at 11:34):Karl Palmskog said:
One persistent issue we have is that people have to get instructions both how to install the VS Code extension and the standalone executable "server" (except in the
coqide-servercase, where it is included in thecoqopam package)
Indeed, that's why to remove the STM and coqidetop from Coq, I would argue that we need to introduce one LSP server in the official Coq package first.
Théo Zimmermann (Apr 07 2023 at 11:35):But at the very least, this alternative server should be in the Coq Platform.
Karl Palmskog (Apr 07 2023 at 11:36):I agree with that, it's somehow a service to users that they get one LSP server by default from the coq package. That doesn't preclude getting more servers through the Platform. My base assumption is basically that all these IDE-related things are in the Platform, unless they get abandoned
Karl Palmskog (Apr 07 2023 at 11:38):in an ideal world, CoqIDE and VsCoq2-extension might even share the LSP server executable
Guillaume Melquiond (Apr 07 2023 at 11:48):But, is that even possible? I thought that each one of the client/server pair was using a slightly different protocol (since LSP is not expressive enough for proof assistants), which makes them incompatible. Or did the various developers agree to merge all of those protocols into a single unified one?
Karl Palmskog (Apr 07 2023 at 12:06):the scenario I'm hoping for is where:
coq opam package to get support for both the VsCoq2 extension and CoqIDE GUI (coqidetop/coqide-server is removed, but replaced by something like vscoqtop) Karl Palmskog (Apr 07 2023 at 12:08):end result is hopefully that Coq GitHub repo has zero GUI-specific code, but one default LSP server executable, possibly with Coq-specific extensions.
(none of the above has been agreed by anyone yet, but the discussion could start if/when new maintainers of CoqIDE come aboard)
Hugo Herbelin (Apr 07 2023 at 13:17):I seems that we also need to enter into the details at some point. The information of being an LSP or XML-based server does not magically tell what features are implemented.
Hugo Herbelin (Apr 07 2023 at 13:18):For instance, vscoq2 roadmap gives some hints about what is already provided or aimed to be provided. One of these features is e.g. calling About on the LSP hovering request, which itself requires something to be done at the Coq-based server level as indicated in vscoq2 issue #343 (probably just a call to Coq's type_of actually).
Hugo Herbelin (Apr 07 2023 at 13:18):As another example, coq-lsp README says that coq-lsp implements "showing the type" on the LSP hovering request. Apparently, this is done by calling Coq's type_of on the global constant (if any) over which hovering happens.
Hugo Herbelin (Apr 07 2023 at 13:18):On the other side, coqide has hovering on warnings, and this is implemented without the protocol having a particular notion of hovering: it just uses the Message data of the protocol. Implementing an About or Check-like hovering would in principle be possible, either crudely by just sending an About request to Coq and decoding the result, or by making the existing query method more structured than it is now (as far as I understand it...).
Hugo Herbelin (Apr 07 2023 at 13:23):the new CoqIDE maintainers are willing to put effort into porting CoqIDE to use LSP
Is there a way to know what should exactly be done for that? For instance, continuing with the example of the hovering LSP request, it would be about finding how gtk3 supports hovering, and if a callback exists for hovering, to bind it to sending a request over LSP, right???
Hugo Herbelin (Apr 07 2023 at 13:25):As another example, would a CoqIDE button like "Fully check the document" make sense over LSP and be implementable (or would it have to be abandoned)?
Hugo Herbelin (Apr 07 2023 at 13:28):Also, would using LSP mean changing the "explicit" evaluation model of CoqIDE (based on the items of the Navigation menu) to an "implicit" automatic evaluation à la Isabelle/JEdit or not necessarily?
Guillaume Melquiond (Apr 07 2023 at 13:29):Hugo Herbelin said:
As another example, would a CoqIDE button like "Fully check the document" make sense over LSP and be implementable (or would it have to be abandoned)?
It already exists. But it is not a button, it is a textual command. (That said, perhaps one can turn textual commands into proper buttons in Vscode, but that is a graphical interface issue completely unrelated to Coq.)
Hugo Herbelin (Apr 07 2023 at 13:41):But it is not a button, it is a textual command.
Yes, my point was not so much about whether it is a button or a command but about whether the LSP servers used by vscoq2 or coq-lsp were supporting it (it is naive, I did not check).
Enrico Tassi (Apr 07 2023 at 13:58):That button is STM specific, and copes with the fact that delegated proof's constraints are not checked for consistency globally. One has to press the button.
Enrico Tassi (Apr 07 2023 at 14:01):A protocol clearly distinguishes the messages metadata from their payload (data). Coqtop does not have that, so it is not a protocol. Undo is, for example, both a message and it's contents.
Karl Palmskog (Apr 07 2023 at 14:07):unfortunately, the definition of "protocol" in the literature (e.g., in distributed systems) is pretty loose, so most would likely view coqtop as a protocol, even without the header/payload distinction
Karl Palmskog (Apr 07 2023 at 14:08):do reasonable and maintainable protocols [implementations] distinguish headers and payload? Probably, yes.
Enrico Tassi (Apr 07 2023 at 14:18):Is there even one example of a protocol in use where it is not the case? I can't think of any
Karl Palmskog (Apr 07 2023 at 14:40):"protocol" is not just whatever the IETF puts out. Do you see anything about "metadata" or "payload" or "headers" in papers about something like Paxos?
Enrico Tassi (Apr 07 2023 at 15:09):There NextBallot is a message, with no payload. It cannot be mistaken for the name of the elected party.
Another way to put it, the syntax MessageName(parameters) is enough to make it clear what is the message and what is the payload.
When coqtop receives Undo it does not really know if the text was part of a .v file being sent by the UI or the request of the UI to backtrack. That is all I'm saying.
Théo Zimmermann (Apr 07 2023 at 15:46):Hugo Herbelin said:
Also, would using LSP mean changing the "explicit" evaluation model of CoqIDE (based on the items of the Navigation menu) to an "implicit" automatic evaluation à la Isabelle/JEdit or not necessarily?
AFAIU not necessarily, especially as UI such as VsCoq2 / coq-lsp may want to keep such a mode available (as Clément pointed out during the last Coq WG, the automatic mode is harmful for battery life).
Maxime Dénès (Apr 07 2023 at 17:41):Hugo Herbelin said:
For instance, vscoq2 roadmap gives some hints about what is already provided or aimed to be provided. One of these features is e.g. calling
Abouton the LSP hovering request, which itself requires something to be done at the Coq-based server level as indicated in vscoq2 issue #343 (probably just a call to Coq's type_of actually).
What has to been done is the ability for Coq to output annotated terms. Calling type_of on x when you hover it in fun x => x will give you incorrect results (the type of a global x).
Maxime Dénès (Apr 07 2023 at 17:42):So you'd want a way to get the type for a subterm of a given term.
Hugo Herbelin (Apr 07 2023 at 20:06):So you'd want a way to get the type for a subterm of a given term.
Exactly! It has to take bound variables into account. The XML export was able to do it at some time, so, no doubt it is possible to do. So did you already implemented it? How do you do it? Is the information added to all sub-expressions in advance or is the information returned one sub-expression after the other, in an on-demand way? And does the annotation include a span of locations or is the retrieval done using ids? Or something else?
The dream would also that it can be used for free by all existing front-ends!
Paolo Giarrusso (Apr 07 2023 at 20:20):Looking forward to Emilio's paper explaining how the LSPs differ
Hugo Herbelin (Apr 08 2023 at 08:16):Still about hovering: is there typically a place (in the wiki, in one of the GUI repos, ...) where to discuss the feature? Possible actions are About and Check (as in vscoq "Hover function" setting) but we can imagine other possibilities, like expanding the notation if on a token of a notation, showing implicit arguments if on a global constant, showing the presence of surrounding coercions, showing statistics about a name, ...
It seems thus that an empirical compromise has to be found between too much information, most useful informations, configurability of the information, etc. What kind of such empirical knowledge do we already have?
Hugo Herbelin (Apr 08 2023 at 08:17):Or, should actions such as showing coercions or implicit arguments be the result of a selection rather than just hovering? Like having a ctrl-click item to locally switch a subexpression from a "normal" view to "Printing All", or "Printing Implicit", etc.
Karl Palmskog (Apr 08 2023 at 08:17):for anything related to VsCoq1/2 or vscoqtop LSP server, I recommend issues in the vscoq repo: https://github.com/coq-community/vscoq
Hugo Herbelin (Apr 08 2023 at 11:14):for anything related to VsCoq1/2 or vscoqtop LSP server
I was also thinking to a way to federate all kinds of works on GUIs, since we have at least 3 different levels which should somehow be freely composable. E.g.:
In particular, from the moment we rethink things (almost) from scratch, I think it is worth to plan far.
Karl Palmskog (Jun 02 2023 at 13:46):devs or other people reading this stream who have Twitter accounts, please help us reach more people with the CoqIDE maintainer call by retweeting: https://twitter.com/CoqLang/status/1664615830728876037
Last updated: Dec 05 2023 at 11:01 UTC