Stream: Coq devs & plugin devs

Topic: Splitting CoqIDE


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jul 17 2020 at 16:49):

Does CoqIDE have any dependencies on the Coq version?

view this post on Zulip 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.)

view this post on Zulip 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 ...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Maxime Dénès (Mar 04 2022 at 12:20):

I would totally support this move.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.]

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Mar 04 2022 at 13:15):

Anything adding friction to the CoqIDE development is likely to simply discourage any maintenance.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Mar 04 2022 at 13:16):

Too much hassle.

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Mar 04 2022 at 13:18):

OK, then that's basically the same point that I was making right above.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Théo Zimmermann (Mar 04 2022 at 13:45):

It was stable for years, and then there was 8.15.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 04 2022 at 13:46):

Bundling with Coq would of course be preserved

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 04 2022 at 13:56):

so I dunno

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Mar 04 2022 at 13:57):

neither

view this post on Zulip Emilio Jesús Gallego Arias (Mar 04 2022 at 13:57):

so?

view this post on Zulip Pierre-Marie Pédrot (Mar 04 2022 at 13:57):

it's an argument about the inexorability of death

view this post on Zulip 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)

view this post on Zulip Théo Zimmermann (Mar 04 2022 at 13:58):

What do you mean by "out commit rules"?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 04 2022 at 13:58):

however for the purpose of the split discussion I dunno

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Mar 04 2022 at 13:59):

now the true question is whether we have an "officially supported UI".

view this post on Zulip 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

view this post on Zulip 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?"

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Mar 04 2022 at 14:00):

obviously technical details matter, that's the whole point of this discussion

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 04 2022 at 14:01):

maybe it doesn't

view this post on Zulip Pierre-Marie Pédrot (Mar 04 2022 at 14:01):

because monorepo means more (involuntarily) manpower

view this post on Zulip Emilio Jesús Gallego Arias (Mar 04 2022 at 14:01):

but IMHO we are at the point that trying could be worth it

view this post on Zulip Emilio Jesús Gallego Arias (Mar 04 2022 at 14:01):

hard to know

view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Mar 04 2022 at 14:02):

simply sharing the RM anihilates the need for a separate one

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 04 2022 at 14:02):

RM for CoqIDE is keeping the changes file

view this post on Zulip Emilio Jesús Gallego Arias (Mar 04 2022 at 14:02):

then dune-release

view this post on Zulip Pierre-Marie Pédrot (Mar 04 2022 at 14:02):

@Emilio Jesús Gallego Arias somebody needs to do that at some point

view this post on Zulip Pierre-Marie Pédrot (Mar 04 2022 at 14:03):

even if it's ε > 0, it's still non-null

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Mar 04 2022 at 14:03):

which is ε

view this post on Zulip Emilio Jesús Gallego Arias (Mar 04 2022 at 14:04):

I don't think it has been \eps

view this post on Zulip Pierre-Marie Pédrot (Mar 04 2022 at 14:04):

I've been a RM and didn't suffer from the CoqIDE release

view this post on Zulip Ali Caglayan (Mar 04 2022 at 14:04):

Well the recent development of the debugger has made a bigger splash than usual no?

view this post on Zulip Pierre-Marie Pédrot (Mar 04 2022 at 14:05):

definitely

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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:

My 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.

view this post on Zulip Théo Zimmermann (Mar 04 2022 at 14:57):

Actually, there are sufficiently many types of consequences that this should be a CEP.

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 04 2022 at 15:56):

having a separate repository is meant to enable a different development practice

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?)

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 04 2022 at 16:36):

again that's a more fundamental mono/multi repos

view this post on Zulip Emilio Jesús Gallego Arias (Mar 04 2022 at 16:36):

but also the organization thing

view this post on Zulip Emilio Jesús Gallego Arias (Mar 04 2022 at 16:36):

I dunno

view this post on Zulip 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).

view this post on Zulip 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).

view this post on Zulip Ramkumar Ramachandra (Mar 04 2022 at 19:33):

Yes, I think we should get the LSP stuff merged in-tree.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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!).

view this post on Zulip Paolo Giarrusso (Mar 07 2022 at 11:43):

parallel proofs work in VsCoq with some bugs (maybe more?)

view this post on Zulip 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 :-)

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Mar 07 2022 at 11:51):

and the conflict was on "next statement", even if the conflicting keybinding might be available normally.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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"...

view this post on Zulip 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?

view this post on Zulip Enrico Tassi (Mar 07 2022 at 14:02):

No no, it is a way to unplug it ;-)

view this post on Zulip 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...

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 14:06):

I can see there is some pessimism about the future of CoqIDE

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 14:06):

but it could be well the case that an independent project revitalizes it

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 14:06):

there is story in my village

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 14:07):

they couldn't bury him

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Mar 07 2022 at 14:17):

https://coq.inria.fr/refman/changes.html suggests the Ltac visual debugger is CoqIDE-specific.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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"

view this post on Zulip Maxime Dénès (Mar 07 2022 at 14:20):

@Karl Palmskog Yes, that's exactly what I suggest.

view this post on Zulip Paolo Giarrusso (Mar 07 2022 at 14:20):

I gotta go, but I guess cc @Jim Fehrle

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 14:27):

I don't know

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 14:27):

I know how things have gone so far

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 14:27):

simplify

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 14:28):

these are good questions @Maxime Dénès , I have no idea

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 14:28):

all these issues, etc...

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 14:29):

I am interested in having coq/coq focused in core coq tech

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 14:29):

it was a very frustating discussion tho

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 14:30):

as my feedback is continiously and regularly ignored

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 14:30):

and put in question without the corresponding backing technical arguments

view this post on Zulip Ali Caglayan (Mar 07 2022 at 14:30):

What should be the target of a new feature then?

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Mar 07 2022 at 14:31):

We don't have a central server for editors

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Mar 07 2022 at 14:31):

PG uses coqtop, CoqIDE, coqtail and VSCoq use coqidetop

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 14:31):

the UI group will resume soon and will set up design guidelines

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 14:31):

on this we agree

view this post on Zulip Ali Caglayan (Mar 07 2022 at 14:32):

I never understand this discussion, what is the alternative?

view this post on Zulip Maxime Dénès (Mar 07 2022 at 14:32):

The alternative for what?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 14:32):

@Ali Caglayan it is still open, but for a start LSP

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 14:32):

but there are other issues we need to discuss, hence the UI WG

view this post on Zulip Ali Caglayan (Mar 07 2022 at 14:32):

Right, so they are not obsolete yet

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 14:32):

which will resume soon

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 14:32):

actually Im busy as hell today :/

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 14:32):

I have to leave

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Mar 07 2022 at 14:33):

But we have to have a working alternative that is better in every aspect.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 14:34):

this is consistent with experience in other systems such as Isabelle

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 14:34):

it doesn not

view this post on Zulip Ali Caglayan (Mar 07 2022 at 14:34):

Right, but what other alternative was there?

view this post on Zulip Maxime Dénès (Mar 07 2022 at 14:34):

And it wastes a lot of core dev resources.

view this post on Zulip Ali Caglayan (Mar 07 2022 at 14:34):

There is no central UI server which is the core problem not CoqIDE.

view this post on Zulip 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.

view this post on Zulip Maxime Dénès (Mar 07 2022 at 14:35):

And build a central UI server on solid foundations.

view this post on Zulip Ali Caglayan (Mar 07 2022 at 14:35):

So instead of deprecating CoqIDE I think we should focus on that.

view this post on Zulip Maxime Dénès (Mar 07 2022 at 14:35):

Who said we wanted to deprecate CoqIDE?

view this post on Zulip Maxime Dénès (Mar 07 2022 at 14:35):

(I may have missed some parts of the discussion)

view this post on Zulip Ali Caglayan (Mar 07 2022 at 14:36):

There was some discussion above about that.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 14:36):

I wanted to deprecate coqidetop yes, not coqide

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 14:36):

but that's what I'm thinking, we need to discuss of course

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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"

view this post on Zulip Karl Palmskog (Mar 07 2022 at 14:37):

hmm, I usually read deprecation as being "no longer the future"

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 14:37):

coqidetop is not longer the future

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 14:37):

coqide maybe

view this post on Zulip Maxime Dénès (Mar 07 2022 at 14:37):

The most pressing point IMHO is to stop consuming core development resources on CoqIDE.

view this post on Zulip Ali Caglayan (Mar 07 2022 at 14:38):

Let's take all that effort and stick it into a UI meeting :)

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 14:42):

Each case is specific for me @Karl Palmskog

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 14:42):

CoqIDE can indeed be decided on a call

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Mar 07 2022 at 14:44):

OK let's make a topic for the coqcall?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 14:45):

For now please don't add this topic to the call

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 14:45):

maxime and I will take care asap

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 14:45):

yes coqide yes

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 14:46):

I mean general UI roadmap

view this post on Zulip Maxime Dénès (Mar 07 2022 at 14:46):

The larger topic of interaction with Coq and so on needs more bandwidth, yes.

view this post on Zulip 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

view this post on Zulip 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>

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip Guillaume Melquiond (Mar 08 2022 at 08:01):

The good news is that it was not merged :-).

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Mar 08 2022 at 16:56):

This is also what the "OCaml Platform" VsCode plugin does.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Paolo Giarrusso (Mar 08 2022 at 18:10):

https://github.com/purcell/exec-path-from-shell#motivation

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Jim Fehrle (Mar 08 2022 at 22:22):

I only ran across this thread just now. A few thoughts:

view this post on Zulip 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!).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Mar 09 2022 at 10:15):

I mean, if it is really the case, then it is a bug.

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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..

view this post on Zulip Enrico Tassi (Mar 09 2022 at 12:36):

Ah, so it seems the UI does not have a box, but the option is there!

view this post on Zulip 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.

view this post on Zulip 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."

view this post on Zulip Emilio Jesús Gallego Arias (Mar 09 2022 at 17:47):

how do you know this?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 09 2022 at 17:47):

as far as I know lablgtk is not scheduled to disappear

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Mar 09 2022 at 17:51):

expect fallout

view this post on Zulip Emilio Jesús Gallego Arias (Mar 09 2022 at 17:51):

I understand it will be supported in Ocaml 5.0

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 09 2022 at 17:51):

IMHO we should be accurate with what write about other projects

view this post on Zulip Emilio Jesús Gallego Arias (Mar 09 2022 at 17:52):

it can be a source of misunderstandings

view this post on Zulip Pierre-Marie Pédrot (Mar 09 2022 at 17:52):

it's maintained, but not actively developed.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Mar 09 2022 at 17:54):

(plus, I will insist, GtkSourceView does not deserve the name of text editor)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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...)

view this post on Zulip 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 :-|

view this post on Zulip 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 :-).

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 10 2022 at 16:46):

they are also updating the UI with the native gtk branch

view this post on Zulip Emilio Jesús Gallego Arias (Mar 10 2022 at 16:46):

there's hope!


Last updated: Jun 04 2023 at 19:30 UTC