Hi all, in these last days the thought of moving CoqIDE to its own independent project has crossed my mind again, and I'm finally becoming convinced that this makes a lot of sense by several reasons.
In particular, there is no reason for CoqIDE releases to be tied to Coq releases; also, packaging and testing of CoqIDE is a bit challenging for Coq core devs. Having a split repos would also allow for more contributors, a lighter process, and the use of more dependencies on CoqIDE's side.
Moreover, the current setup is not bound to scale if we add more UI's to Coq repos; we would have to spend significant time keeping track of the dependencies. For 8.13, the main installation images are supposed to come from the platform indeed, so CoqIDE would be a good candidate to use that, tho CoqIDE itself could provide Coq + CoqIDE images in its repos.
WDYT?
since I help out with Coq opam packaging, I can tell you CoqIDE has been a pain every time to package due to its dependencies. We have started to submit Coq and CoqIDE opam packages separately to the general repo since CoqIDE will usually get stuck on CI. I think this would be an argument in favor of decoupling Coq from CoqIDE.
Does CoqIDE have any dependencies on the Coq version?
(Currently wondering if Coq 8.12.0 could reuse CoqIDE 8.11.2 as-is, but I feel I've exhausted my hack quota.)
In opam cpqide is already a separate package. Maybe one could try what happen if one relaxes the version restrictions ...
IIRC the XML protocol did not change, hence CoqIDE should work. IMO Coq should version the XML protocol (there is a init message, but I don't recall if it carries a version). CoqIDE should just check that version that say: I'm too new/old. This is the prerequisite for a split, IMO.
Other IDEs working with the XML protocol already manage to support several versions. The XML protocol is very stable.
Hi folks, now that we have updated our build infrastructure, I have become very convinced that it is time for CoqIDE to be moved to its own repository, and I think the tradeoff is very positive towards this move, at least with the reasoning I've been using.
That's not urgent at all, but I'm opening this thread for preliminary discussion.
I think if we want to do this, we need to do it in a way that won't disrupt developer workflow. I don't think the user workflow will be affected since coqide is already a separate opam package. One thing that I and other developers like to do is to test stuff in coqide when hacking away on coq. If we move coqide to a separate repo, how will we be able to call or hack coqide?
I believe that CoqIDE should be somewhat version agnostic, but this requires a more rigid way of updating and versioning the XML protocol than we currently have.
for the first point, dune's pitch is that you can keep a similar workflow even with separate repos, if you check them out in the same workspace. Of course in coq there is extra glue code over dune that would need updating.
I think it's a good idea to generally develop CoqIDE separately and potentially have it be compatible with multiple Coq versions. But indeed thanks to Dune and nice CI technology, the repo code placement needn't change for that...
I would totally support this move.
I think that the main interest of moving CoqIDE out would be to decouple the Coq and CoqIDE releases and have CoqIDE support multiple Coq versions. But this only makes sense if the CoqIDE maintainers are actually interested in doing this. If not, then this will just make the workflow more complex for no benefit.
I will repeat my official position: moving CoqIDE to another repo is a death sentence. You're free to consider it's a positive outcome, though.
[In particular, there is no point to do this split if in the end it is the Coq RM who needs to take care of doing CoqIDE releases.]
@Pierre-Marie Pédrot Can you clarify why you think that? I can see several possible reasons, but I'd like to hear that from you.
Did someone agree to become the maintainer and release manager of Coqide? We should not even be talking about splitting Coqide away from Coq if we cannot find someone serious to take over.
@Théo Zimmermann CoqIDE barely survives today already. It's based on a legacy GTK library over bindings that are not really developed anyways. It uses a protocol whose design is dubious. It is a terrible text editor and even for Coq dev it's not great.
Anything adding friction to the CoqIDE development is likely to simply discourage any maintenance.
@Guillaume Melquiond I'm an official maintainer as per github teams, but I won't be candidate for release management.
Too much hassle.
The only reason I like CoqIDE is that it comes bundled with Coq so it's the only easily available UI when hacking the Coq implem.
OK, then that's basically the same point that I was making right above.
Yes, I fully agree, we need to keep the existing workflow; regarding the protocol update, last time I checked it was basically stable for years; I think we should do some changes on the technical aspect of the implementation tho.
Pierre-Marie Pédrot said:
I will repeat my official position: moving CoqIDE to another repo is a death sentence. You're free to consider it's a positive outcome, though.
I can see why you would think that way, but on the other hand if that would happen, it means that what we have is a zombie?
So in fact, giving coqide its own space could maybe mean its only chance to get out of the zombie status then!
It was stable for years, and then there was 8.15.
Bundling with Coq would of course be preserved
So in fact, giving coqide its own space could maybe mean its only chance to get out of the zombie status then!
This could turn out to be very true. But then this would mean acknowledging that CoqIDE is no longer backed by the Coq development team and that it needs to recruit new maintainers (who can of course overlap with the Coq dev team), e.g., as part of Coq-community.
Bundling with Coq would of course be preserved
This point is easy to achieve, especially now with the Coq Platform.
I have been convinced about the move after all the discussion I have been having lately privately, in the hackathon, and publicily. Having a more focused project can really help. Also, having coqide here is really a barrier for attracking UI people. In some sense we have the worst of both worlds now:
The point of "I am only interested in maintaining coqide if it is in the coq repos" is understandable to me, but not sure very logical
of course would be split coqide it would still remain an official coq project, and on the coq organization
but I agree that there seems to be a deeper discussion here, about how to develop Coq:
do we want a monorepos apporach, or a multi-repos one. It is only natural that Coq becomes a set of components over time, and both approaches (multi vs mono) have their advantages.
I like multi-repos but I also agree that our current tooling is far from good for it
Something that could be worth doing then is to make a call for CoqIDE maintainers where we ask "Would you be interested in becoming a CoqIDE maintainer if it was maintained separately from Coq in its own repository?". If the call is successful, then the split makes sense. But if it isn't, then it is best to let CoqIDE where it is, at least until we decide that we want to stop supporting it.
That seems reasonable @Théo Zimmermann , on the other hand one point of the move is to attrach new maintainers, and allow other maintainers to work with different commit rules
also there is the point of some Coq (not coqide) maintainers willing the move to happen
so I dunno
lablgtk is in a zombie state, you can't develop an UI atop of that that is not itself in zombie state...
certainly we are now in a mono repos but out commit rules can't work for a mono repos
Pierre-Marie Pédrot said:
lablgtk is in a zombie state, you can't develop an UI atop of that that is not itself in zombie state...
that's an argument in favor or against the split?
neither
so?
it's an argument about the inexorability of death
that's a very interesting discussion, and it gets more actual as we enter the 21st century, I'd even recommend a few recent expositions about it (follow me on insta for art stuff)
What do you mean by "out commit rules"?
however for the purpose of the split discussion I dunno
my point is that if you split, it's dead now. if you don't it might survive a bit.
Théo Zimmermann said:
What do you mean by "out commit rules"?
Indeed I wasn't precise, I meant our commit and review system. For example, the rule that we can't commit our own PRs, which is very uncommon
now the true question is whether we have an "officially supported UI".
Pierre-Marie Pédrot said:
my point is that if you split, it's dead now. if you don't it might survive a bit.
I see you point, however I am not sure how it follows from a logical deduction
I don't think development on CoqIDE will improve in a separate repo. As I understand it, CoqIDE was created and maintained as a side project. Many Coq users, including myself, use CoqIDE for actual Coq developments. I believe that there is sufficient demand for an official Coq GUI.
Part of the reason CoqIDE has been maintained for so long is because it is using ocaml bindings for GTK. This is both a blessing and a curse. On one hand, coq developers can easily tweak parts of the gui, on the other hand, as has been said, gtk bindings and GUI in general in OCaml are poorly supported.
This kind of question always brings up the question of a Coq LSP. Which everybody likes to dream about and talk about but the actual implementation of such a project is very difficult. I know various people have been trying things out, but as of today it doesn't exist.
So I think the question isn't really "should CoqIDE be split off" but rather "are we willing to put some effort in to get an LSP that can be used by everybody?"
Pierre-Marie Pédrot said:
now the true question is whether we have an "officially supported UI".
that's a very interesting question, but IMHO a bit unrelated, as I don't see how a technical organization matter can alter support status which is a manpower one
obviously technical details matter, that's the whole point of this discussion
@Ali Caglayan Coq LSP has been resurrected thanks to efforts by myself and @Ramkumar Ramachandra , ping us in private, but a release is expected soon
Pierre-Marie Pédrot said:
obviously technical details matter, that's the whole point of this discussion
How is support (a manpower issue) related to repository organization
My point is that for community development, a more focused repository will improve community interaction
maybe it doesn't
because monorepo means more (involuntarily) manpower
but IMHO we are at the point that trying could be worth it
hard to know
Pierre-Marie Pédrot said:
because monorepo means more (involuntarily) manpower
That's an interesting hypothesis, how have you measured that?
simply sharing the RM anihilates the need for a separate one
If you want serious GUI devs to maintain CoqIDE I think we need to move away from doing GUI in OCaml. The OCaml parts should just be the LSP.
RM for CoqIDE is keeping the changes file
then dune-release
@Emilio Jesús Gallego Arias somebody needs to do that at some point
even if it's ε > 0, it's still non-null
Ali Caglayan said:
If you want serious GUI devs to maintain CoqIDE I think we need to move away from doing GUI in OCaml. The OCaml parts should just be the LSP.
LSP doesn't solve the core problems we have now , but let's have that discussion on a different thread please
Pierre-Marie Pédrot said:
even if it's ε > 0, it's still non-null
But you need to substract the time saved by the Coq RM as not having to care about CoqIDE
which is ε
I don't think it has been \eps
I've been a RM and didn't suffer from the CoqIDE release
Well the recent development of the debugger has made a bigger splash than usual no?
definitely
but in this case it's not so much release than just the fact everything is subtly broken
And this isn't to put blame on adding new features, this is a problem with how CoqIDE is developed. It is difficult to add new stuff.
as a user I'd rather have a half-decent text editor than adding new features used by 2 persons in the wolrd, but YMMV
(not even taking into account the fact that a new Ltac features is adding tactic insult to UI injury)
People are still using Ltac as of today, so helping them debug their code is not absurd. Just look at Talia's message on Coq-Club on why she doesn't use Ltac2 today...
I'm not saying that we don't want to debug Ltac, I'm saying that the current design is based on piles of quicksand
This thread is already very long an diverging.
@Emilio Jesús Gallego Arias can you write somewhere, maybe in an issue:
foobar.opam
would be moved outMy take is that we must keep one "language server" in Coq. Be it coqide-server or something other in the future. For now coqide-server is not used by just CoqIDE, and IMO it should stay (it is clearly misnamed). About the GTK interface, that can be moved out IMO.
Actually, there are sufficiently many types of consequences that this should be a CEP.
Outsider perspective:
I think that there are three possible end-users to consider here, all three of which I have some experience with:
dune exec ./dev/shim/coqide-prelude
to spin up an editor that is guaranteed to be properly linked to the Coq version that I'm hacking on, without me having to mess with the PATH
or anything else. Anything that would jeopardize that workflow would be a shame. I know that I can just "drop in" the CoqIDE repo, and then Dune will take care of everything, but this is an additional (nontrivial!) step that needs to be taken.Whether to move coqide-server or not is an interesting question. Also moving to its own repository doesn't mean that a project is not "a part of Coq" anymore
having a separate repository is meant to enable a different development practice
or a different release schedule, so it could be well the case that a language server would like to do releases outside of Coq's main cycle
@Lasse I agree with all 3 points here, in particular point 3 should keep working whether we move to an outside repos or not, we have the tooling to make that happen easily
@Emilio Jesús Gallego Arias , but with a separate repo, for point (3) I will presumably still have to do some kind of manual clone of the CoqIDE repo and drop it somewhere right? Or do you suggest having CoqIDE as a git submodule?
@Lasse there are many approaches to have that work, a submodule, but even an auto-checkout
Is it possible to do in a way that makes the workflow look exactly the same as today? i.e. hack on coq and coqide, commit changes together finally push (but it would really push to a seperate repo?)
@Ali Caglayan for that we'd need to improve our overlay workflow a bit
but if we do, it would be similar, actually, we could just have a tooling that does "hack with all these plugins together, then create the branches / push / etc... automatically"
I do have a lot of notes for improving the overlay workflow for plugins
again that's a more fundamental mono/multi repos
but also the organization thing
I dunno
@Lasse how’s that course set up? my experience with CoqIDE is that (a) it’s never been usable on Mac (b) even on Linux, it doesn’t work with more than one file — as in, I tried installing CoqIDE for a colleague and I failed to figure it out, so we switched to Emacs. (Admittedly, it’s because I didn’t know about _CoqProject).
if those are the concerns, I wonder if it’d help to do something like “package VsCoq with Coq”, at least in the sense of an installer giving you both in the correct configuration. (It “just” needs to set the Coq path in vscoq’s settings).
Yes, I think we should get the LSP stuff merged in-tree.
Although I wonder if VSCoq could be a good solution: it does have its fair share of bugs, and it's not exactly well-maintained.
Separate discussion, but thanks to vscode it's much more usable IMHO (in certain ways), and it does async proofs. (Even if it doesn't cope with STM bugs as well as coqide, I've heard).
@Paolo Giarrusso In my country, Mac is not very popular so this has never really been an issue (the one or two students who have a Mac are accustomed to having to fiddle around with things because they use non-standard hardware/software). In my experience CoqIDE works flawlessly on bot Linux and Windows (modulo all of its known peculiarities and bugs of course). I've never had any complaints (outside of the fact that the inferface in general is outdated and not super user-friendly compared to other editors).
In the past, we just linked students to Coq's homepage and told them to install it however they wanted. On Windows, this meant through the (old) installer. On Linux, usually through their distro's package manager. More recently we've also been experimenting with some package customizations, which has been more tricky. For windows, this means creating custom installers (through Coq platform) and for Linux/Mac we've mainly been using Opam.
Ramkumar Ramachandra said:
Although I wonder if VSCoq could be a good solution: it does have its fair share of bugs, and it's not exactly well-maintained.
The current effort behind VSCoq aims at maintaining the current version while working on new foundations (separation of parsing and execution in Coq, a new document manager etc). So basing strategic plans on what VsCoq is today does not make a lot of sense.
@Paolo Giarrusso : I am using CoqIDE on Mac every day and have no issues with it (except when I insist on using a German PC keyboard layout, which makes it hard ti type | or @ in CoqIDE). It is also officially supported by Coq Platform and reports about Mac issues are quite infrequent. On Mac both the "compile from sources" version and the DMG version work fine to my knowledge. I am also using it with many files every day. So honestly I have no idea what you are talking about.
@Lasse Blaauwbroek : I think some Coq professionals are (still) using CoqIDE because the support of parallel proofs. I tend to start it with -async-proofs-j 12
(yes on Mac) and for large developments it is just so much faster than the alternatives - especially when restructuring larger developments where one needs to remcompile larger files frequently. Not sure how the status of parallel proofs is in VsCoq these days. Definitely without parallel proofs such restructuring work would take 3 times longer (@Enrico Tassi : thanks!).
parallel proofs work in VsCoq with some bugs (maybe more?)
@Michael Soegtrop you're aware of https://github.com/coq/platform/issues/217, and you know it hasn't been solved; I'll certainly acknowledge that things work fine for you :-)
before this issue, I have gotten stuck somewhere else that I only vaguely recall: IIRC, I had keybinding conflicts, I tried to remap things, I struggled to use Cmd in remapping.
and the conflict was on "next statement", even if the conflicting keybinding might be available normally.
but since I haven't ever managed to use CoqIDE on Linux, I can't tell apart what's macOS-specific from "all of its known peculiarities and bugs" that @Lasse Blaauwbroek mentions.
IMHO a crash when opening the preferences hardly justifies to state that it never worked on Mac. The access issues will be fixed in the next release (afaik the trick is to replace the shell script which calls CoqIDE with a C program with the same functionality). But I guess this won't fix it for you since compile from sources doesn't work for you either.
but since I haven't ever managed to use CoqIDE on Linux
This should also work. What issues do you have there?
I didn't say "it never worked on Mac", I said "not usable", and gave details...
But since CoqIDE's not going to become comparable to alternatives, IMHO it's more useful to say "what would you demand before we can ditch it"...
If coqIDE is to be ditched eventually, then it doesn't make sense to split it out, does it?
No no, it is a way to unplug it ;-)
Despite totally agreeing on the rational level, I will still be sad the day that happens...
I can see there is some pessimism about the future of CoqIDE
but it could be well the case that an independent project revitalizes it
there is story in my village
there was an old man, "un hermano" as they are called there in sign of respect
they couldn't bury him
Alternatives are not mature enough that we can just drop support for CoqIDE today, IMHO. However, we need to stop spending resources on its development in favor of higher priorities. I'd suggest we switch CoqIDE to bugfix-only maintenance mode. That doesn't prevent people from describing other long term plans for CoqIDE. We can see whether splitting makes sense if that happens.
But that is already the case. The last major feature of Coqide dates back from 8.5 (the asynchronous mode). Since then, nothing noteworthy happened. (In fact, as far as I am concerned, most of the things since then were actually counter-productive, like rejecting filenames containing dashes.)
Indeed @Maxime Dénès splitting is a way to say "maintenance only mode" [by the overalys] but also opens the doors at other persons doing work on it easily if they want
https://coq.inria.fr/refman/changes.html suggests the Ltac visual debugger is CoqIDE-specific.
Paolo Giarrusso said:
https://coq.inria.fr/refman/changes.html suggests the Ltac visual debugger is CoqIDE-specific.
it is in principle not
shouldn't the meaning of "maintenance only" be something like: we don't accept PRs with features, only bugfixes
@Guillaume Melquiond I suspect some activity must have happened, since we saw some regressions recently, no? Maybe it wasn't clearly identified as CoqIDE items?
@Karl Palmskog could be like this, or just "it is on a separate repos which we won't touch except for overlays"
@Karl Palmskog Yes, that's exactly what I suggest.
I gotta go, but I guess cc @Jim Fehrle
OK, then I think this gives a reasonable criterion for when a repo split could/should happen: if someone comes along who wants to add features and can credibly take over maintenance
otherwise the most efficient way to do bugfix-based maintenance seems to be in the coq
repo...
Yes, this was what I meant "describing other long term plans". But I'd go for the most efficient approach : maintenance only while keeping it where it is, moving to a dedicated repo if a credible alternative comes up (group of devs with experience and a roadmap).
The open question for me is whether moving could cause "a group of devs with interest and a roadmap" to appear. Community formation is not something that develops in a planned way I think
There is a loop here: we make contributing hard, so people don't contribute
Maxime Dénès said:
Guillaume Melquiond I suspect some activity must have happened, since we saw some regressions recently, no? Maybe it wasn't clearly identified as CoqIDE items?
As @Emilio Jesús Gallego Arias said, it was for features of Coq itself which were mirrored into Coqide. I don't think there was any feature specific to Coqide as an editor.
and we don't make contributing easier as there is not a lot of people interested in contributing
so the hypothesis at play here is whether splitting would have a positive or negative effect
I don't know
but isn't it also that we think CoqIDE is basically a technological dead-end?
I know how things have gone so far
Maxime Dénès said:
but isn't it also that we think CoqIDE is basically a technological dead-end?
that's a very good question, and I don't know
do we really want to attract development forces to work on text editting features over GTK?
for example, would we have done the splitting in 2017 I would have used ppx to simplity a lot of the stuff
or do we want to attract contributors on more core aspects to the Coq project?
simplify
these are good questions @Maxime Dénès , I have no idea
I like the fact that I don't have to see CoqIDE related stuff in the coq repos
all these issues, etc...
I'd be happy as a developer to see them moved to a different bug tracker
I am interested in having coq/coq focused in core coq tech
I havent' followed the details, what other UI than CoqIDE supports the visual Ltac debugguer?
and that the tech that is in coq/coq is better specified than the current ad-hoc ide stuff
that also misleads a lot of people, who come and see that's an standard
Maxime Dénès said:
I havent' followed the details, what other UI than CoqIDE supports the visual Ltac debugguer?
it doesn't not atm, but I tried my best to be sure it can be mapped to DAP easily
it was a very frustating discussion tho
as my feedback is continiously and regularly ignored
So maybe we should extend this notion of maintenance-only mode. A new feature should not have CoqIDE as its primary target.
and put in question without the corresponding backing technical arguments
What should be the target of a new feature then?
for example for the debugger, I requested for the protocol to conform to dap
We don't have a central server for editors
we have some standards, they are not the best, but we certainly have targets
PG uses coqtop, CoqIDE, coqtail and VSCoq use coqidetop
the UI group will resume soon and will set up design guidelines
Ali Caglayan said:
PG uses coqtop, CoqIDE, coqtail and VSCoq use coqidetop
all that is obsolete
on this we agree
I never understand this discussion, what is the alternative?
The alternative for what?
@Ali Caglayan it is still open, but for a start LSP
but there are other issues we need to discuss, hence the UI WG
Right, so they are not obsolete yet
which will resume soon
actually Im busy as hell today :/
I have to leave
Ali Caglayan said:
Right, so they are not obsolete yet
yes they are, and their immediate deprecation and removal is a topic I'd propose for the UI meeting
If we are talking development, I'd expect we focus on 1- non-UI related feature on the Coq side and 2- solid foundations for UIs in the various efforts ongoing around interfaces.
as this is what other systems have done, so there is a lot of backing experience
But we have to have a working alternative that is better in every aspect.
Ali Caglayan said:
But we have to have a working alternative that is better in every aspect.
it is not so simple, as supporting legacy features may block the development of new features
this is consistent with experience in other systems such as Isabelle
Implementing a major UI-oriented feature that primarly targets CoqIDE doesn't seem to make a lot of sense.
it doesn not
Right, but what other alternative was there?
And it wastes a lot of core dev resources.
There is no central UI server which is the core problem not CoqIDE.
The alternative is to focus on non-UI oriented features, on the Coq side, as I wrote.
And build a central UI server on solid foundations.
So instead of deprecating CoqIDE I think we should focus on that.
Who said we wanted to deprecate CoqIDE?
(I may have missed some parts of the discussion)
There was some discussion above about that.
I wanted to deprecate coqidetop yes, not coqide
deprecating CoqIDE (putting it in maintenance mode) is the obvious step if the core team wants to focus on a new IDE server + non-IDE things
but that's what I'm thinking, we need to discuss of course
As I said, replacing coqide top with somethin like serapi (a bit of ppx) is very easy
Karl Palmskog said:
deprecating CoqIDE (putting it in maintenance mode) is the obvious step if the core team wants to focus on a new IDE server + non-IDE things
I see, to me deprecation and maintenance-only are to different things.
and much smallar code and maintenance wise, but we need to split coqide for it to happen, so hence "el pescado que se muerde la cola"
hmm, I usually read deprecation as being "no longer the future"
coqidetop is not longer the future
coqide maybe
The most pressing point IMHO is to stop consuming core development resources on CoqIDE.
Let's take all that effort and stick it into a UI meeting :)
right, I think you can call that [no longer consuming resources] as deprecation or something else, as long as the meaning is clear...
Meetings are nice, but they also consume a lot of resources. It would be more efficient to write down the policy for changes accepted to CoqIDE, circulate it and discuss it briefly at a Coq call IMHO.
isn't this comparable to Function
vs. Equations in some sense? I don't think anyone wants to do anything with Function besides fixing clear bugs, but it will live on without a set expiration date. And Equations is the future, but will develop separately for a while longer, without any specific bound.
I have the feeling that Function
does not steal as much time from Pierre-Marie and Emilio (for example), but I may be wrong.
Each case is specific for me @Karl Palmskog
CoqIDE can indeed be decided on a call
however core Coq stuff needs to a meeting i think, but we will see on the way
Funind is indeed a PITA when you have to do architectural changes (e.g. removal of the legacy tactic engine)
but thankfully it's effectively legacy code that is not touched and thus cannot regress
So the idea for the future is to consolidate some sort of server for Coq's UI stuff. Isn't this essentially the LSP at this point?
It would nice indeed to phase it out too as we did with omega, but that's a lot of work, anyways that is not on topic for this trhead
Ali Caglayan said:
So the idea for the future is to consolidate some sort of server for Coq's UI stuff. Isn't this essentially the LSP at this point?
It looks like it, but we need to discuss more IMHO
OK let's make a topic for the coqcall?
there are many details to figure out, and UI design is not an exact science
Ali Caglayan said:
OK let's make a topic for the coqcall?
a UI working group is being formed as we speak
@Maxime Dénès we have data on CoqIDE usage from the survey, maybe that should be summarized before any CoqIDE decisions?
Emilio Jesús Gallego Arias said:
Ali Caglayan said:
OK let's make a topic for the coqcall?
a UI working group is being formed as we speak
it will go slow due to ERC and ANR calls being close, but will pick up lots of momentum soon
For now please don't add this topic to the call
maxime and I will take care asap
I think we should add it to the call, if we talk specifically about switching CoqIDE to maintenance-only.
yes coqide yes
I mean general UI roadmap
The larger topic of interaction with Coq and so on needs more bandwidth, yes.
if someone want to help summarizing the discussion at diversity (which includes UI) would be great, is on my todo but not gonna happen until after the 17th
Paolo Giarrusso said:
I didn't say "it never worked on Mac", I said "not usable", and gave details...
But since CoqIDE's not going to become comparable to alternatives, IMHO it's more useful to say "what would you demand before we can ditch it"...
As I said - the main reason I still use CoqIDE is the support for parallel proofs. Not sure if VSCoq has this.
But then there is also the installation simplicity aspect @Lasse Blaauwbroek mentioned. I remember that I once wanted to attend a course on AGDA and couldn't follow it because I didn't manage to get the editor running - and I usually get things working. The feedback I get from teachers on CoqPlatform and CoqIDE is that it works quite reliably and with little tutor effort in classes. I think it is a very important aspect for the future of Coq that we don't loose students in a class course of stupid technical issues. <joking> Of course it might happen that we loose some students because they are disgusted by the design of CoqIDE </joking>
Emilio Jesús Gallego Arias said:
As I said, replacing coqide top with somethin like serapi (a bit of ppx) is very easy
For me at least, one of the biggest hurdles to switching away from coqidetop is documentation. Getting the XML protocol to work for coqtail was fairly painful, so I'm reluctant to do it all over again with something else. Some sort of guide for smoothly transitioning from XML to serapi would be very helpful.
For sure, IDE maintainers should not switch their production-ready version from the XML protocol to SerAPI (because SerAPI does not come bundled with Coq by default). What Emilio is proposing is to create a new protocol inspired by SerAPI, make it official (and thus bundle it with Coq) and document it as such. But I guess some feedback loop with IDE maintainers will also be quite useful to make sure that it fits their needs correctly.
Michael Soegtrop said:
I think some Coq professionals are (still) using CoqIDE because the support of parallel proofs.
Fair enough.
Michael Soegtrop said:
<joking> Of course it might happen that we loose some students because they are disgusted by the design of CoqIDE </joking>
I've actually seen this happen first-hand. I'm not saying CoqIDE is especially bad (I use it quite happily), but compared to the aesthetics of VScode or Jetbrains (something many students are used to) it is indeed not very good. In my experience, people are very easily impressed by nice visuals and usability (including myself). I've seen a group of students be extremely impressed by Lean (over Coq) not necessarily for its technical merits, but simply because the IDE looks nice and because it has this feature where Lean's state is automatically synchronized with the location of the caret (I'm personally not sure whether or not that is actually desirable).
@Guillaume Melquiond To illustrate what I was writing above, here's an example of a patch which touches the coqide server component and does not look like a strict bugfix to me: https://github.com/coq/coq/pull/15737
The good news is that it was not merged :-).
@Lasse Blaauwbroek : indeed it is a good point that Coq has to compete also in point of UI aesthetics with other provers.
If there is something I can do in Coq Platform to make the use of VSCoq easier, please let me know. It is quite imaginable that the Coq Platform script also sets up VsCoq in a found VSCode installation. The Windows installer likely could also do this. For Mac and snap this woould be harder unless one bundles VSCode (or VSCodium for license reasons), but one can likely supply a script one could call to do the setup.
Do you think this would help teachers?
The technical reasons to keep CoqIDE are separate from the "ease of installation" issues.
Vscode is packaged as a snap (I do install it that way). If a student gets the platform via snap he can also get vscode. Installing the vscoq extension is trivial. Imo, if you have both snaps installed and the extension, things should just work (since coqidetop should be an alias), see https://github.com/coq-community/vscoq/pull/194
@Lasse Blaauwbroek : can you comment on @Enrico Tassi comment? I understood you such that it is not that trivial, but possibly this was about other OSes.
@Michael Soegtrop I have very little experience with vscode myself unfortunately (I use emacs). I would of course welcome anything that makes installation better. However, I should note that in general the problem is not with the "happy path", like what Enrico is describing. The problem is usually that there are many ways to install editors, extensions, plugins and Coq on many OS'es. Many students will have already have vscode installed in some way or another, and want to reuse that installation. Accounting for all of the different possible configurations is very difficult. (Note that this is not about big problems, but as a teacher even spending 10 minutes getting things working for each individual student is a lot.)
On top of this, my experience is that many students somehow manage to completely and utterly screw up their OS installation. I've seen some baffling configurations of laptops both on Windows and Linux where everything is completely upside-down.
As such, I won't be able to offer a much better suggestion than just "try to integrate everything as tightly as possible, minimizing the reliance on external packages and system configurations as much as possible". Sorry, I know that is not very helpful.
(One common issue, that has little to do with Coq Platform is with people who install Coq through Opam and then try to use an external editor. I that case it is usually rather tricky to get the path set up correctly, due to eval $(opam env)
related issues.)
I need to ponder over this a bit. Especially tricky might be the multi version support in Coq Platform - if one goes for VScode, one needs some simple mechanism to select the Coq version VsCoq uses. Possibly this needs some integration work in VsCoq, say VsCoq should look for opam and ask what switches it can offer and present this to the user. The issues is similar with Python, where VsCoq also asks which Python to use.
This is also what the "OCaml Platform" VsCode plugin does.
I did some tests. As it looks currently - as far as I can tell - VsCoq picks up the Coq which was in path when VsCoq was started - which is not that bad.
the ocaml platform extension lets you pick an opam switch, that code can probably be reused in/together vscoq
@Michael Soegtrop that’s the default (which can be configured), but Coq need not be on the PATH that VsCode gets
at least on Mac, I haven’t found a good way to customize the PATH passed to apps, but I have found LOTS of workarounds for e.g. Emacs (not sure if VsCode has something similar)
https://github.com/purcell/exec-path-from-shell#motivation
and I only link that as problem statement, not as a solution, since this does not work transparently, especially if the shell configuration is not reliable — I agree with @Lasse Blaauwbroek that some student laptops have messed-up configs.
Paolo Giarrusso said:
at least on Mac, I haven’t found a good way to customize the PATH passed to apps, but I have found LOTS of workarounds for e.g. Emacs (not sure if VsCode has something similar)
Really? For me (on macOS) vscode always gets whatever is in PATH at start time, but I need to quit it completely and restart after a switch. I don't need to run it from the terminal for this.
EDIT: Ah perhaps, I read too fast and you mean if you want something different from the PATH at launch time.
I only ran across this thread just now. A few thoughts:
Thanks for your contributions, Jim; I think a fair question is whether you'd be interested to contribute to an alternative interface to focus efforts, or not (even if I'm maybe not the one who should ask it!).
I'm not convinced that it would take one person more than a year or so to address a great many weak points if we were better organized.
The point is we probably don't want to invest core developers time on developing CoqIDE-specific things too much, nor on things specific to its current protocol. So moving to a separate repo and having a team of dedicated developers is one way to avoid that, switching to bugfix-only maintenance is another one. I guess they are equally fine. But I doubt we want to stay in the current status quo, where progress on high priority work is very slow and developer time is spent elsewhere.
Well, how many PRs have the core developers submitted for CoqIDE recently? How much time has that been?
Getting "Make" to work in CoqIDE--is that a bug fix or a new feature?
I would love to see an elaboration of what's high priority and what's not. I've been wanting to see that for a long while.
Indeed I think that splitting to a repository both the server and the client would be a good solution.
In fact that would help the separation of concerns, as core Coq APIs should be good enough, but designed a bit independently from a concrete client
Lasse Blaauwbroek said:
I've actually seen this happen first-hand. I'm not saying CoqIDE is especially bad (I use it quite happily), but compared to the aesthetics of VScode or Jetbrains (something many students are used to) it is indeed not very good. In my experience, people are very easily impressed by nice visuals and usability (including myself). I've seen a group of students be extremely impressed by Lean (over Coq) not necessarily for its technical merits, but simply because the IDE looks nice and because it has this feature where Lean's state is automatically synchronized with the location of the caret (I'm personally not sure whether or not that is actually desirable).
Lean's VSCode extension is very good, and I wouldn't be surprised if much of Lean's popularity can be attributed to this. Personally, I think CoqIDE is a lost cause when it comes to attracting new users. I think we need to put real effort into developing an lsp server, and having a lightweight VSCode extension that works with this, similar to Lean's. In comparison to developing and maintaining a full GTK+ GUI, a VSCode extension is _much_ easier to develop and maintain.
Concerning the idea that sometimes changes need to be done both within coq and coqide, and putting them in separate repository would make that harder : that's definitely a strong argument in favor of splitting! Coq should provide a nice, clean and ui-agnostic interface through which all of them should work. As long as coqide gets a free pass to change things, that's not really possible.
Julien Puydt said:
that's definitely a strong argument in favor of splitting!
Unfortunately, that is just wishful thinking. We already have some experience when it comes to splitting a part of Coq to a separate repository: Bignums. Did that reduce the number of breaking changes to the interface of Coq plugins? Not a single bit. Did it make the lives of everyone more miserable? Definitely.
Paolo Giarrusso said:
at least on Mac, I haven’t found a good way to customize the PATH passed to apps, but I have found LOTS of workarounds for e.g. Emacs (not sure if VsCode has something similar)
What I usually do is opam switch in a shell and launch the editor (CoqIDE or VSCode) from there. VsCode is not really meant to be used in this way (more to keep it open all day long), but it is not much of an issue either - usually I end up having several VsCode open.
A note on VsCoq vs. CoqIDE: I yesterday switched to VsCoq for some larger restructuring work and I think in the end I am faster with VsCoq. It doesn't have CoqIDE's parallel proofs (as yet), but on macOS CoqIDE is generally a bit sluggish and recently I have the impression that parsing files (the time the "bar" needs to build up after pressing "run to end") got quite a bit slower. This is instant in VsCoq. Since I frequently do not need to wait for the proofs to check, the faster parsing time of VsCoq makes up for the time I loose in waiting for proofs to finish.
It doesn't have CoqIDE's parallel proofs (as yet)
The UI may display things differently, but behind the scenes it uses the very same tech. It delegated the same proofs, and you can pass coqidetop the same -j options. So They are both slow (or fast), but I don't see how they can behave differently wrt parallel proofs.
I mean, if it is really the case, then it is a bug.
That said, I concur with @Michael Soegtrop about the fact that Coqide seems more sluggish nowadays. With older versions of Coq, it was possible to run to the end of https://gitlab.inria.fr/flocq/flocq/-/raw/master/src/Pff/Pff.v . This is no longer possible. (Granted, this file is a monster that should never have existed. But it is still a good test of the performance of an editor, especially since it is self-contained.)
Jim Fehrle said:
Well, how many PRs have the core developers submitted for CoqIDE recently? How much time has that been?
Getting "Make" to work in CoqIDE--is that a bug fix or a new feature?
I would love to see an elaboration of what's high priority and what's not. I've been wanting to see that for a long while.
We should not forget that submitting PRs is not the only time consuming task. Reviews, discussions during calls, handling of regressions, etc, have also to be taken into account.
As for a clear list of topics that are considered as high priority, I fully agree, we should absolutely make it explicit.
@Enrico Tassi : I guess I am lacking a way to pass the -async-proofs-j 12
option I give to CoqIDE via VsCoq to coqidetop. I would expect that if VsCoq would support it, there would be some thread count setting in the VsCoq plugin settings, but I couldn't find one.
Just to be clear here, we found the way to pass that option: https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/Splitting.20CoqIDE.20.28options.20to.20coqidetop.29
Indeed I don't find it either. I think you can put the option in _CoqProject
as in -arg -async-proofs-j -arg 12
but that is also passed to coqc
in batch mode and it may not like it..
Ah, so it seems the UI does not have a box, but the option is there!
Guillaume Melquiond said:
Julien Puydt said:
that's definitely a strong argument in favor of splitting!
Unfortunately, that is just wishful thinking. We already have some experience when it comes to splitting a part of Coq to a separate repository: Bignums. Did that reduce the number of breaking changes to the interface of Coq plugins? Not a single bit. Did it make the lives of everyone more miserable? Definitely.
I would argue that the number of users and contributors for CoqIDE is far higher than bignums however.
I folks, I see you wrote "knowing that labgtk will go away at some point."
how do you know this?
as far as I know lablgtk is not scheduled to disappear
no, but it's not actively developed, and there is OCaml 5.0 about to wreak havoc
expect fallout
I understand it will be supported in Ocaml 5.0
I can understand people assume lablgtk not being maintained, but last time I talked to Gaguirre it was not the case
IMHO we should be accurate with what write about other projects
it can be a source of misunderstandings
it's maintained, but not actively developed.
also, gtk on osx and windows is a joke. I like gtk, gobject, glib and use gnome. But it is linux only, really.
(plus, I will insist, GtkSourceView does not deserve the name of text editor)
IMHO CoqIDE still get's the job done - it is not beautiful but it is a work horse. Nevertheless I would think the future is in VsCoq as default. I would think it is not that much work to give VsCoq the same installation reliability as CoqIDE.
Another advantage of splitting which I have stated above but will restate: We won't be stuck with using OCaml for GUI. We can choose a language that has much better GUI support since all the OCaml stuff should be the language server (which is coq side). Therefore the "labl will be dead soon" won't matter too much. It's much easier to find maintainers for other GUI languages than OCaml, IMO.
if you're going to reimplement an IDE nearly from scratch in another language, then why even keep the connection to CoqIDE?
There are python/ocaml bridges out there. It could be one way of migrating code from one language to another gradually. (I'm not going to do that, but well...)
is an "IDE from scratch" really worth it? Not even Haskell can pull that off despite its bigger community :-|
it's clear CoqIDE is still needed in some cases today. But if we focused (even more) on VSCoq, that'd be fixable — and at least @Maxime Dénès is already busy on that :-).
we have been able to successfully revive 20+ year old Coq projects, but never revived anything UI related for Coq, to my knowledge. Most UI work bitrots really quickly and is then gone forever
my conclusion from that is that any new UI effort needs to be thought through/analyzed really carefully, since the risk of bitrotting is so high
Good IDEs are also super-time consuming to develop in general, so reusing as much as possible is great.
Plus VSCode development seems pretty accessible — strategically speaking, VSCode plays a role comparable with a younger Emacs.
IMHO we should go with VsCoq - I don't see disadvantages with it. I think we should stop developing new features in CoqIDE and develop new features in VsCoq instead.
The main thing I see missing in VsCoq is a neat way to connect it to installed Coqs. I will create an issue for that.
I think another (known) issue for newcomers is the detection of _CoqProject
which can only detect the one at the root of the open folder (so it does not work for subfolders).
@Théo Winterhalter : good point. I guess we should encourage teachers then to provide a VsCode workspace file which sets up things in an unambiguous way - including the Coq Platform switch name to use.
I created issue (https://github.com/coq-community/vscoq/issues/286) for the "Find Coq" part.
FWIW I think it's unlikely I would want to get involved in GUI development for vsCoq. The debugger work has been been such a slow process. If the group decides not to permit improvements to CoqIDE, then some of the debugger improvements I suggested in my CoqPL talk won't happen. Note that the server side changes should be readily reusable for other IDEs.
Jim Fehrle said:
FWIW I think it's unlikely I would want to get involved in GUI development for vsCoq.
Do reconsider. It's not really GUI development in the traditional sense: all you write is a bit of TypeScript using the VSCode API, and the rest is taken care of. I can't say too many nice things about the VSCoq codebase, but VSCode extension development is, in general, very pleasant. The tooling is very good and the workflow is polished to perfection.
Offtopic, but I'm yet to see a development workflow as smooth and polished as VSCode extension development.
Emacs workflow is pretty nice too, but elisp is way more niche, and the learning curve for emacs is huge
@Jim Fehrle : I think for the time being it is fine to develop features like the debugger in CoqIDE as long as the server protocols are done with porting to other editors in mind. I just fear that CoqIDE is doomed. It would be too much work to bring it to the expectations of todays computer users. I think it doesn't make sense to switch right in the middle of a development like the debugger, but I also think that if it is rounded up in CoqIDE you should consider looking into VsCoq.
@Emilio Jesús Gallego Arias I used Emacs for the longest time, before switching to VSCode. Elisp doesn’t have namespaces: all the variables from all the packages pollute the global namespace, and there’s no way to “unload” an extension, or “revert” a setting; just edit your .emacs, and restart Emacs. Further, Elisp isn’t multi-threaded, and has no concept of promises like ts does; as a result, Emacs hangs on a long-running operation. Besides, Elisp is very slow, while V8 is very fast.
@Ramkumar Ramachandra all of this is correct but I heard that recent emacs versions have made a huge progress on all these fronts
still I agree with you, but I find like emacs can maybe still compete
they are also updating the UI with the native gtk branch
there's hope!
Last updated: Jun 04 2023 at 19:30 UTC