Emilio Jesús Gallego Arias (Jul 17 2020 at 09:34): Emilio Jesús Gallego Arias (Jul 17 2020 at 09:34):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?
Karl Palmskog (Jul 17 2020 at 11:55):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.
Paolo Giarrusso (Jul 17 2020 at 16:49):Does CoqIDE have any dependencies on the Coq version?
Paolo Giarrusso (Jul 17 2020 at 16:50):(Currently wondering if Coq 8.12.0 could reuse CoqIDE 8.11.2 as-is, but I feel I've exhausted my hack quota.)
Michael Soegtrop (Jul 17 2020 at 16:56):In opam cpqide is already a separate package. Maybe one could try what happen if one relaxes the version restrictions ...
Enrico Tassi (Jul 17 2020 at 19:43):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.
Théo Zimmermann (Jul 18 2020 at 18:10):Other IDEs working with the XML protocol already manage to support several versions. The XML protocol is very stable.
Emilio Jesús Gallego Arias (Mar 04 2022 at 09:45):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.
Ali Caglayan (Mar 04 2022 at 11:54):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?
Ali Caglayan (Mar 04 2022 at 11:56):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.
Paolo Giarrusso (Mar 04 2022 at 12:07):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.
Karl Palmskog (Mar 04 2022 at 12:09):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...
Maxime Dénès (Mar 04 2022 at 12:20):I would totally support this move.
Théo Zimmermann (Mar 04 2022 at 12:58):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.
Pierre-Marie Pédrot (Mar 04 2022 at 12:59):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.
Théo Zimmermann (Mar 04 2022 at 13:00):[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.]
Théo Zimmermann (Mar 04 2022 at 13:01):@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.
Guillaume Melquiond (Mar 04 2022 at 13:11):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.
Pierre-Marie Pédrot (Mar 04 2022 at 13:15):@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.
Pierre-Marie Pédrot (Mar 04 2022 at 13:15):Anything adding friction to the CoqIDE development is likely to simply discourage any maintenance.
Pierre-Marie Pédrot (Mar 04 2022 at 13:16):@Guillaume Melquiond I'm an official maintainer as per github teams, but I won't be candidate for release management.
Pierre-Marie Pédrot (Mar 04 2022 at 13:16):Too much hassle.
Pierre-Marie Pédrot (Mar 04 2022 at 13:18):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.
Théo Zimmermann (Mar 04 2022 at 13:18):OK, then that's basically the same point that I was making right above.
Emilio Jesús Gallego Arias (Mar 04 2022 at 13:44):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.
Emilio Jesús Gallego Arias (Mar 04 2022 at 13:45):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!
Théo Zimmermann (Mar 04 2022 at 13:45):It was stable for years, and then there was 8.15.
Emilio Jesús Gallego Arias (Mar 04 2022 at 13:46):Bundling with Coq would of course be preserved
Théo Zimmermann (Mar 04 2022 at 13:47):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.
Théo Zimmermann (Mar 04 2022 at 13:47):Bundling with Coq would of course be preserved
This point is easy to achieve, especially now with the Coq Platform.
Emilio Jesús Gallego Arias (Mar 04 2022 at 13:49):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
Emilio Jesús Gallego Arias (Mar 04 2022 at 13:49):of course would be split coqide it would still remain an official coq project, and on the coq organization
Emilio Jesús Gallego Arias (Mar 04 2022 at 13:51):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
Théo Zimmermann (Mar 04 2022 at 13:54):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.
Emilio Jesús Gallego Arias (Mar 04 2022 at 13:55):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
Emilio Jesús Gallego Arias (Mar 04 2022 at 13:56):also there is the point of some Coq (not coqide) maintainers willing the move to happen
Emilio Jesús Gallego Arias (Mar 04 2022 at 13:56):so I dunno
Pierre-Marie Pédrot (Mar 04 2022 at 13:56):lablgtk is in a zombie state, you can't develop an UI atop of that that is not itself in zombie state...
Emilio Jesús Gallego Arias (Mar 04 2022 at 13:57):certainly we are now in a mono repos but out commit rules can't work for a mono repos
Emilio Jesús Gallego Arias (Mar 04 2022 at 13:57):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?
Pierre-Marie Pédrot (Mar 04 2022 at 13:57):neither
Emilio Jesús Gallego Arias (Mar 04 2022 at 13:57):so?
Pierre-Marie Pédrot (Mar 04 2022 at 13:57):it's an argument about the inexorability of death
Emilio Jesús Gallego Arias (Mar 04 2022 at 13:58):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)
Théo Zimmermann (Mar 04 2022 at 13:58):What do you mean by "out commit rules"?
Emilio Jesús Gallego Arias (Mar 04 2022 at 13:58):however for the purpose of the split discussion I dunno
Pierre-Marie Pédrot (Mar 04 2022 at 13:58):my point is that if you split, it's dead now. if you don't it might survive a bit.
Emilio Jesús Gallego Arias (Mar 04 2022 at 13:59):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
Pierre-Marie Pédrot (Mar 04 2022 at 13:59):now the true question is whether we have an "officially supported UI".
Emilio Jesús Gallego Arias (Mar 04 2022 at 13:59):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
Ali Caglayan (Mar 04 2022 at 13:59):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?"
Emilio Jesús Gallego Arias (Mar 04 2022 at 14:00):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
Pierre-Marie Pédrot (Mar 04 2022 at 14:00):obviously technical details matter, that's the whole point of this discussion
Emilio Jesús Gallego Arias (Mar 04 2022 at 14:00):@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
Emilio Jesús Gallego Arias (Mar 04 2022 at 14:01):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
Emilio Jesús Gallego Arias (Mar 04 2022 at 14:01):My point is that for community development, a more focused repository will improve community interaction
Emilio Jesús Gallego Arias (Mar 04 2022 at 14:01):maybe it doesn't
Pierre-Marie Pédrot (Mar 04 2022 at 14:01):because monorepo means more (involuntarily) manpower
Emilio Jesús Gallego Arias (Mar 04 2022 at 14:01):but IMHO we are at the point that trying could be worth it
Emilio Jesús Gallego Arias (Mar 04 2022 at 14:01):hard to know
Emilio Jesús Gallego Arias (Mar 04 2022 at 14:02):Pierre-Marie Pédrot said:
because monorepo means more (involuntarily) manpower
That's an interesting hypothesis, how have you measured that?
Pierre-Marie Pédrot (Mar 04 2022 at 14:02):simply sharing the RM anihilates the need for a separate one
Ali Caglayan (Mar 04 2022 at 14:02):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.
Emilio Jesús Gallego Arias (Mar 04 2022 at 14:02):RM for CoqIDE is keeping the changes file
Emilio Jesús Gallego Arias (Mar 04 2022 at 14:02):then dune-release
Pierre-Marie Pédrot (Mar 04 2022 at 14:02):@Emilio Jesús Gallego Arias somebody needs to do that at some point
Pierre-Marie Pédrot (Mar 04 2022 at 14:03):even if it's ε > 0, it's still non-null
Emilio Jesús Gallego Arias (Mar 04 2022 at 14:03):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
Emilio Jesús Gallego Arias (Mar 04 2022 at 14:03):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
Pierre-Marie Pédrot (Mar 04 2022 at 14:03):which is ε
Emilio Jesús Gallego Arias (Mar 04 2022 at 14:04):I don't think it has been \eps
Pierre-Marie Pédrot (Mar 04 2022 at 14:04):I've been a RM and didn't suffer from the CoqIDE release
Ali Caglayan (Mar 04 2022 at 14:04):Well the recent development of the debugger has made a bigger splash than usual no?
Pierre-Marie Pédrot (Mar 04 2022 at 14:05):definitely
Pierre-Marie Pédrot (Mar 04 2022 at 14:05):but in this case it's not so much release than just the fact everything is subtly broken
Ali Caglayan (Mar 04 2022 at 14:05):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.
Pierre-Marie Pédrot (Mar 04 2022 at 14:06):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
Pierre-Marie Pédrot (Mar 04 2022 at 14:06):(not even taking into account the fact that a new Ltac features is adding tactic insult to UI injury)
Théo Zimmermann (Mar 04 2022 at 14:13):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...
Pierre-Marie Pédrot (Mar 04 2022 at 14:14):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
Enrico Tassi (Mar 04 2022 at 14:39):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.
Théo Zimmermann (Mar 04 2022 at 14:57):Actually, there are sufficiently many types of consequences that this should be a CEP.
Lasse Blaauwbroek (Mar 04 2022 at 15:35):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. Emilio Jesús Gallego Arias (Mar 04 2022 at 15:56):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
Emilio Jesús Gallego Arias (Mar 04 2022 at 15:56):having a separate repository is meant to enable a different development practice
Emilio Jesús Gallego Arias (Mar 04 2022 at 15:57):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
Emilio Jesús Gallego Arias (Mar 04 2022 at 15:57):@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
Lasse Blaauwbroek (Mar 04 2022 at 16:19):@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?
Emilio Jesús Gallego Arias (Mar 04 2022 at 16:26):@Lasse there are many approaches to have that work, a submodule, but even an auto-checkout
Ali Caglayan (Mar 04 2022 at 16:31):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?)
Emilio Jesús Gallego Arias (Mar 04 2022 at 16:35):@Ali Caglayan for that we'd need to improve our overlay workflow a bit
Emilio Jesús Gallego Arias (Mar 04 2022 at 16:36):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"
Emilio Jesús Gallego Arias (Mar 04 2022 at 16:36):I do have a lot of notes for improving the overlay workflow for plugins
Emilio Jesús Gallego Arias (Mar 04 2022 at 16:36):again that's a more fundamental mono/multi repos
Emilio Jesús Gallego Arias (Mar 04 2022 at 16:36):but also the organization thing
Emilio Jesús Gallego Arias (Mar 04 2022 at 16:36):I dunno
Paolo Giarrusso (Mar 04 2022 at 19:07):@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).
Paolo Giarrusso (Mar 04 2022 at 19:10):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).
Ramkumar Ramachandra (Mar 04 2022 at 19:33):Yes, I think we should get the LSP stuff merged in-tree.
Ramkumar Ramachandra (Mar 04 2022 at 19:34):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.
Paolo Giarrusso (Mar 04 2022 at 20:05):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).
Lasse Blaauwbroek (Mar 04 2022 at 23:37):@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.
Maxime Dénès (Mar 05 2022 at 09:47):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.
Michael Soegtrop (Mar 07 2022 at 11:42):@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!).
Paolo Giarrusso (Mar 07 2022 at 11:43):parallel proofs work in VsCoq with some bugs (maybe more?)
Paolo Giarrusso (Mar 07 2022 at 11:45):@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 :-)
Paolo Giarrusso (Mar 07 2022 at 11:49):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.
Paolo Giarrusso (Mar 07 2022 at 11:51):and the conflict was on "next statement", even if the conflicting keybinding might be available normally.
Paolo Giarrusso (Mar 07 2022 at 11:52):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.
Michael Soegtrop (Mar 07 2022 at 12:41):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?
Paolo Giarrusso (Mar 07 2022 at 13:33):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"...
Julien Puydt (Mar 07 2022 at 13:43):If coqIDE is to be ditched eventually, then it doesn't make sense to split it out, does it?
Enrico Tassi (Mar 07 2022 at 14:02):No no, it is a way to unplug it ;-)
Pierre-Marie Pédrot (Mar 07 2022 at 14:04):Despite totally agreeing on the rational level, I will still be sad the day that happens...
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:06):I can see there is some pessimism about the future of CoqIDE
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:06):but it could be well the case that an independent project revitalizes it
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:06):there is story in my village
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:07):there was an old man, "un hermano" as they are called there in sign of respect
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:07):they couldn't bury him
Maxime Dénès (Mar 07 2022 at 14:11):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.
Guillaume Melquiond (Mar 07 2022 at 14:14):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.)
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:17):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
Paolo Giarrusso (Mar 07 2022 at 14:17):https://coq.inria.fr/refman/changes.html suggests the Ltac visual debugger is CoqIDE-specific.
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:17):Paolo Giarrusso said:
https://coq.inria.fr/refman/changes.html suggests the Ltac visual debugger is CoqIDE-specific.
it is in principle not
Karl Palmskog (Mar 07 2022 at 14:19):shouldn't the meaning of "maintenance only" be something like: we don't accept PRs with features, only bugfixes
Maxime Dénès (Mar 07 2022 at 14:19):@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?
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:20):@Karl Palmskog could be like this, or just "it is on a separate repos which we won't touch except for overlays"
Maxime Dénès (Mar 07 2022 at 14:20):@Karl Palmskog Yes, that's exactly what I suggest.
Paolo Giarrusso (Mar 07 2022 at 14:20):I gotta go, but I guess cc @Jim Fehrle
Karl Palmskog (Mar 07 2022 at 14:21):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
Karl Palmskog (Mar 07 2022 at 14:22):otherwise the most efficient way to do bugfix-based maintenance seems to be in the coq repo...
Maxime Dénès (Mar 07 2022 at 14:23):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).
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:25):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
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:26):There is a loop here: we make contributing hard, so people don't contribute
Guillaume Melquiond (Mar 07 2022 at 14:26):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.
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:26):and we don't make contributing easier as there is not a lot of people interested in contributing
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:26):so the hypothesis at play here is whether splitting would have a positive or negative effect
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:27):I don't know
Maxime Dénès (Mar 07 2022 at 14:27):but isn't it also that we think CoqIDE is basically a technological dead-end?
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:27):I know how things have gone so far
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:27):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
Maxime Dénès (Mar 07 2022 at 14:27):do we really want to attract development forces to work on text editting features over GTK?
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:27):for example, would we have done the splitting in 2017 I would have used ppx to simplity a lot of the stuff
Maxime Dénès (Mar 07 2022 at 14:27):or do we want to attract contributors on more core aspects to the Coq project?
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:27):simplify
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:28):these are good questions @Maxime Dénès , I have no idea
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:28):I like the fact that I don't have to see CoqIDE related stuff in the coq repos
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:28):all these issues, etc...
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:28):I'd be happy as a developer to see them moved to a different bug tracker
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:29):I am interested in having coq/coq focused in core coq tech
Maxime Dénès (Mar 07 2022 at 14:29):I havent' followed the details, what other UI than CoqIDE supports the visual Ltac debugguer?
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:29):and that the tech that is in coq/coq is better specified than the current ad-hoc ide stuff
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:29):that also misleads a lot of people, who come and see that's an standard
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:29):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
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:29):it was a very frustating discussion tho
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:30):as my feedback is continiously and regularly ignored
Maxime Dénès (Mar 07 2022 at 14:30):So maybe we should extend this notion of maintenance-only mode. A new feature should not have CoqIDE as its primary target.
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:30):and put in question without the corresponding backing technical arguments
Ali Caglayan (Mar 07 2022 at 14:30):What should be the target of a new feature then?
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:30):for example for the debugger, I requested for the protocol to conform to dap
Ali Caglayan (Mar 07 2022 at 14:31):We don't have a central server for editors
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:31):we have some standards, they are not the best, but we certainly have targets
Ali Caglayan (Mar 07 2022 at 14:31):PG uses coqtop, CoqIDE, coqtail and VSCoq use coqidetop
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:31):the UI group will resume soon and will set up design guidelines
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:31):Ali Caglayan said:
PG uses coqtop, CoqIDE, coqtail and VSCoq use coqidetop
all that is obsolete
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:31):on this we agree
Ali Caglayan (Mar 07 2022 at 14:32):I never understand this discussion, what is the alternative?
Maxime Dénès (Mar 07 2022 at 14:32):The alternative for what?
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:32):@Ali Caglayan it is still open, but for a start LSP
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:32):but there are other issues we need to discuss, hence the UI WG
Ali Caglayan (Mar 07 2022 at 14:32):Right, so they are not obsolete yet
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:32):which will resume soon
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:32):actually Im busy as hell today :/
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:32):I have to leave
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:33):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
Maxime Dénès (Mar 07 2022 at 14:33):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.
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:33):as this is what other systems have done, so there is a lot of backing experience
Ali Caglayan (Mar 07 2022 at 14:33):But we have to have a working alternative that is better in every aspect.
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:33):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
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:34):this is consistent with experience in other systems such as Isabelle
Maxime Dénès (Mar 07 2022 at 14:34):Implementing a major UI-oriented feature that primarly targets CoqIDE doesn't seem to make a lot of sense.
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:34):it doesn not
Ali Caglayan (Mar 07 2022 at 14:34):Right, but what other alternative was there?
Maxime Dénès (Mar 07 2022 at 14:34):And it wastes a lot of core dev resources.
Ali Caglayan (Mar 07 2022 at 14:34):There is no central UI server which is the core problem not CoqIDE.
Maxime Dénès (Mar 07 2022 at 14:34):The alternative is to focus on non-UI oriented features, on the Coq side, as I wrote.
Maxime Dénès (Mar 07 2022 at 14:35):And build a central UI server on solid foundations.
Ali Caglayan (Mar 07 2022 at 14:35):So instead of deprecating CoqIDE I think we should focus on that.
Maxime Dénès (Mar 07 2022 at 14:35):Who said we wanted to deprecate CoqIDE?
Maxime Dénès (Mar 07 2022 at 14:35):(I may have missed some parts of the discussion)
Ali Caglayan (Mar 07 2022 at 14:36):There was some discussion above about that.
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:36):I wanted to deprecate coqidetop yes, not coqide
Karl Palmskog (Mar 07 2022 at 14:36):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
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:36):but that's what I'm thinking, we need to discuss of course
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:36):As I said, replacing coqide top with somethin like serapi (a bit of ppx) is very easy
Maxime Dénès (Mar 07 2022 at 14:37):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.
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:37):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"
Karl Palmskog (Mar 07 2022 at 14:37):hmm, I usually read deprecation as being "no longer the future"
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:37):coqidetop is not longer the future
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:37):coqide maybe
Maxime Dénès (Mar 07 2022 at 14:37):The most pressing point IMHO is to stop consuming core development resources on CoqIDE.
Ali Caglayan (Mar 07 2022 at 14:38):Let's take all that effort and stick it into a UI meeting :)
Karl Palmskog (Mar 07 2022 at 14:38):right, I think you can call that [no longer consuming resources] as deprecation or something else, as long as the meaning is clear...
Maxime Dénès (Mar 07 2022 at 14:39):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.
Karl Palmskog (Mar 07 2022 at 14:40):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.
Maxime Dénès (Mar 07 2022 at 14:41):I have the feeling that Function does not steal as much time from Pierre-Marie and Emilio (for example), but I may be wrong.
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:42):Each case is specific for me @Karl Palmskog
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:42):CoqIDE can indeed be decided on a call
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:42):however core Coq stuff needs to a meeting i think, but we will see on the way
Pierre-Marie Pédrot (Mar 07 2022 at 14:42):Funind is indeed a PITA when you have to do architectural changes (e.g. removal of the legacy tactic engine)
Pierre-Marie Pédrot (Mar 07 2022 at 14:43):but thankfully it's effectively legacy code that is not touched and thus cannot regress
Ali Caglayan (Mar 07 2022 at 14:43):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?
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:43):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
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:43):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
Ali Caglayan (Mar 07 2022 at 14:44):OK let's make a topic for the coqcall?
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:44):there are many details to figure out, and UI design is not an exact science
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:44):Ali Caglayan said:
OK let's make a topic for the coqcall?
a UI working group is being formed as we speak
Karl Palmskog (Mar 07 2022 at 14:44):@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 (Mar 07 2022 at 14:44):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
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:45):For now please don't add this topic to the call
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:45):maxime and I will take care asap
Maxime Dénès (Mar 07 2022 at 14:45):I think we should add it to the call, if we talk specifically about switching CoqIDE to maintenance-only.
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:45):yes coqide yes
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:46):I mean general UI roadmap
Maxime Dénès (Mar 07 2022 at 14:46):The larger topic of interaction with Coq and so on needs more bandwidth, yes.
Emilio Jesús Gallego Arias (Mar 07 2022 at 14:46):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
Michael Soegtrop (Mar 07 2022 at 15:04):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>
Wolf Honore (Mar 07 2022 at 16:29):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.
Théo Zimmermann (Mar 07 2022 at 16:41):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.
Lasse Blaauwbroek (Mar 07 2022 at 21:47):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).
Maxime Dénès (Mar 08 2022 at 07:32):@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
Guillaume Melquiond (Mar 08 2022 at 08:01):The good news is that it was not merged :-).
Michael Soegtrop (Mar 08 2022 at 08:48):@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.
Enrico Tassi (Mar 08 2022 at 09:38):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
Michael Soegtrop (Mar 08 2022 at 09:42):@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.
Lasse Blaauwbroek (Mar 08 2022 at 13:02):@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.
Lasse Blaauwbroek (Mar 08 2022 at 13:06):(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.)
Michael Soegtrop (Mar 08 2022 at 13:21):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.
Théo Zimmermann (Mar 08 2022 at 16:56):This is also what the "OCaml Platform" VsCode plugin does.
Michael Soegtrop (Mar 08 2022 at 17:54):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.
Enrico Tassi (Mar 08 2022 at 18:06):the ocaml platform extension lets you pick an opam switch, that code can probably be reused in/together vscoq
Paolo Giarrusso (Mar 08 2022 at 18:08):@Michael Soegtrop that’s the default (which can be configured), but Coq need not be on the PATH that VsCode gets
Paolo Giarrusso (Mar 08 2022 at 18:10):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)
Paolo Giarrusso (Mar 08 2022 at 18:10):https://github.com/purcell/exec-path-from-shell#motivation
Paolo Giarrusso (Mar 08 2022 at 18:14):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.
Théo Winterhalter (Mar 08 2022 at 18:26):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.
Jim Fehrle (Mar 08 2022 at 22:22):I only ran across this thread just now. A few thoughts:
Paolo Giarrusso (Mar 08 2022 at 23:38):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!).
Maxime Dénès (Mar 08 2022 at 23:45):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.
Jim Fehrle (Mar 09 2022 at 00:31):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.
Emilio Jesús Gallego Arias (Mar 09 2022 at 00:48):Indeed I think that splitting to a repository both the server and the client would be a good solution.
Emilio Jesús Gallego Arias (Mar 09 2022 at 00:49):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
Ramkumar Ramachandra (Mar 09 2022 at 05:12):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.
Julien Puydt (Mar 09 2022 at 06:43):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.
Guillaume Melquiond (Mar 09 2022 at 06:49):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.
Michael Soegtrop (Mar 09 2022 at 07:35):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.
Michael Soegtrop (Mar 09 2022 at 09:24):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.
Enrico Tassi (Mar 09 2022 at 10:15):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.
Enrico Tassi (Mar 09 2022 at 10:15):I mean, if it is really the case, then it is a bug.
Guillaume Melquiond (Mar 09 2022 at 10:24):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.)
Maxime Dénès (Mar 09 2022 at 10:31):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.
Michael Soegtrop (Mar 09 2022 at 10:31):@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.
Ali Caglayan (Mar 09 2022 at 10:56):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
Enrico Tassi (Mar 09 2022 at 12:35):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..
Enrico Tassi (Mar 09 2022 at 12:36):Ah, so it seems the UI does not have a box, but the option is there!
Ali Caglayan (Mar 09 2022 at 12:40):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.
Emilio Jesús Gallego Arias (Mar 09 2022 at 17:47):I folks, I see you wrote "knowing that labgtk will go away at some point."
Emilio Jesús Gallego Arias (Mar 09 2022 at 17:47):how do you know this?
Emilio Jesús Gallego Arias (Mar 09 2022 at 17:47):as far as I know lablgtk is not scheduled to disappear
Pierre-Marie Pédrot (Mar 09 2022 at 17:50):no, but it's not actively developed, and there is OCaml 5.0 about to wreak havoc
Pierre-Marie Pédrot (Mar 09 2022 at 17:51):expect fallout
Emilio Jesús Gallego Arias (Mar 09 2022 at 17:51):I understand it will be supported in Ocaml 5.0
Emilio Jesús Gallego Arias (Mar 09 2022 at 17:51):I can understand people assume lablgtk not being maintained, but last time I talked to Gaguirre it was not the case
Emilio Jesús Gallego Arias (Mar 09 2022 at 17:51):IMHO we should be accurate with what write about other projects
Emilio Jesús Gallego Arias (Mar 09 2022 at 17:52):it can be a source of misunderstandings
Pierre-Marie Pédrot (Mar 09 2022 at 17:52):it's maintained, but not actively developed.
Enrico Tassi (Mar 09 2022 at 17:54):also, gtk on osx and windows is a joke. I like gtk, gobject, glib and use gnome. But it is linux only, really.
Pierre-Marie Pédrot (Mar 09 2022 at 17:54):(plus, I will insist, GtkSourceView does not deserve the name of text editor)
Michael Soegtrop (Mar 09 2022 at 18:35):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.
Ali Caglayan (Mar 09 2022 at 18:48):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.
Karl Palmskog (Mar 09 2022 at 19:00):if you're going to reimplement an IDE nearly from scratch in another language, then why even keep the connection to CoqIDE?
Enrico Tassi (Mar 09 2022 at 19:06):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...)
Paolo Giarrusso (Mar 09 2022 at 22:28):is an "IDE from scratch" really worth it? Not even Haskell can pull that off despite its bigger community :-|
Paolo Giarrusso (Mar 09 2022 at 22:32):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 :-).
Karl Palmskog (Mar 09 2022 at 22:32):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
Karl Palmskog (Mar 09 2022 at 22:33):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
Paolo Giarrusso (Mar 09 2022 at 22:38):Good IDEs are also super-time consuming to develop in general, so reusing as much as possible is great.
Paolo Giarrusso (Mar 09 2022 at 22:39):Plus VSCode development seems pretty accessible — strategically speaking, VSCode plays a role comparable with a younger Emacs.
Michael Soegtrop (Mar 10 2022 at 07:17):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.
Théo Winterhalter (Mar 10 2022 at 07:26):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).
Michael Soegtrop (Mar 10 2022 at 07:34):@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.
Jim Fehrle (Mar 10 2022 at 08:50):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.
Ramkumar Ramachandra (Mar 10 2022 at 09:23):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.
Ramkumar Ramachandra (Mar 10 2022 at 09:27):Offtopic, but I'm yet to see a development workflow as smooth and polished as VSCode extension development.
Emilio Jesús Gallego Arias (Mar 10 2022 at 09:32):Emacs workflow is pretty nice too, but elisp is way more niche, and the learning curve for emacs is huge
Michael Soegtrop (Mar 10 2022 at 10:17):@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.
Ramkumar Ramachandra (Mar 10 2022 at 10:33):@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.
Emilio Jesús Gallego Arias (Mar 10 2022 at 16:46):@Ramkumar Ramachandra all of this is correct but I heard that recent emacs versions have made a huge progress on all these fronts
Emilio Jesús Gallego Arias (Mar 10 2022 at 16:46):still I agree with you, but I find like emacs can maybe still compete
Emilio Jesús Gallego Arias (Mar 10 2022 at 16:46):they are also updating the UI with the native gtk branch
Emilio Jesús Gallego Arias (Mar 10 2022 at 16:46):there's hope!
Last updated: Dec 06 2023 at 13:01 UTC