Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

CoqIDE will be soon impossible to build in Debian derivatives #7055

Closed
ejgallego opened this issue Mar 22, 2018 · 42 comments

Comments

Projects
None yet
10 participants
@ejgallego
Copy link
Member

commented Mar 22, 2018

The GTK libraries CoqIDE depends will be soon removed from Debian. This means CoqIDE will become much harder to build in these distributions.

For more details, see: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=885677

@gares

This comment has been minimized.

Copy link
Member

commented Mar 23, 2018

Thanks for the heads up.
Maybe it is time to really think about UIs ;-)

@Zimmi48

This comment has been minimized.

Copy link
Member

commented Mar 23, 2018

So what about choosing to drop CoqIDE completely and make VSCode with VSCoq the main interface for people who don't like Emacs?

I didn't personally tested VSCode yet (that's on my TODO list) but it has become the most popular editor among developers according to StackOverflow's 2018 survey (cf. https://insights.stackoverflow.com/survey/2018#technology-most-popular-development-environments).

Moreover, I think it would be saner that the Coq development team stop maintaining, building and distributing (with headaches) an editor on its own. We should focus on what we do best: Coq.

cc @MSoegtropIMC who proposed it on Coq-Club (or Coqdev, I can't remember)
and @siegebell who is the author of VSCoq

PS: @ejgallego you should read the description of the "priority: critical" label (just hover on it). Did you find a proof of False?

@maximedenes

This comment has been minimized.

Copy link
Member

commented Mar 23, 2018

One thing I wanted to explore is to develop first class support for LSP (https://langserver.org/) on the Coq side.

@ppedrot

This comment has been minimized.

Copy link
Member

commented Mar 23, 2018

It was pretty clear this would happen someday... As mentioned in the Debian thread, we're not the only ones in trouble here, we might want to ask LablGTK devs what they believe to be a decent solution (@garrigue ?). Maybe this simply means dropping LablGTK altogether?

@garrigue

This comment has been minimized.

Copy link

commented Mar 23, 2018

Last time we had a discussion on the lablgtk list, the feeling was that gtk3 itself was not an interesting target.
So the question is whether there is sufficient compatibility support in gtk3 so that we could move at little cost.
I haven't checked yet.
If the required effort is the same as moving from gtk1 to gtk2, I'm not sure anybody is ready to do it.

@ejgallego

This comment has been minimized.

Copy link
Member Author

commented Mar 23, 2018

The best option is without any doubt to port lablgtk to gtk3.

LSP by itself is far from being useful to Coq.

@maximedenes

This comment has been minimized.

Copy link
Member

commented Mar 23, 2018

LSP by itself is far from being useful to Coq.

Can you say a bit more?

@Zimmi48

This comment has been minimized.

Copy link
Member

commented Mar 23, 2018

The best option is without any doubt to port lablgtk to gtk3.

Hum. Are you willing to do it? If there is no volunteer to do it, this is ridiculous to pretend it's the best option.

@maximedenes

This comment has been minimized.

Copy link
Member

commented Mar 23, 2018

Hum. Are you willing to do it? If there is no volunteer to do it, this is ridiculous to pretend it's the best option.

Let's not overreact, there could be a "best option" independently of what our resources are, and of what people are willing to do.

@ejgallego I have the feeling that you frustrate a bit your readers (like me) by sending teasers :D We are curious to read a summary of your vision about LSP.

@ejgallego

This comment has been minimized.

Copy link
Member Author

commented Mar 23, 2018

Hum. Are you willing to do it? If there is no volunteer to do it, this is ridiculous to pretend it's the best option.

I have a hard time following your reasoning. There are many other mature tools that depend on lablgtk so for sure the best for all users is to port lablgtk to GTK3 as the only option otherwise is to review quite a few hundredth thousand lines of code from scratch.

@siegebell

This comment has been minimized.

Copy link
Contributor

commented Mar 23, 2018

@ejgallego I'd like to hear more about the issues you see with using LSP for Coq.

FWIW, I think writing an LSP server from scratch (especially if you can base it off of Hack's OCaml implementation of LSP) is not significantly more work than porting CoqIDE. And there's the long-term payoff of not having to maintain your own editor...

@ejgallego

This comment has been minimized.

Copy link
Member Author

commented Mar 23, 2018

@ejgallego I'd like to hear more about the issues you see with using LSP for Coq.

AFAICT LSP doesn't fit into the interactive paradigm used in Coq development, at best, it fits partially, so you still have a to implement a lot of custom operations in order for the server to be usable. The most mature implementation in that setting is Isabelle's LSP support [financed by Imandra IMUIC]. Anyways, you know better than I do about LSP / Coq.

That being said a LSP server for Coq will appear some day [see ejgallego/coq-serapi#26]

@maximedenes

This comment has been minimized.

Copy link
Member

commented Mar 23, 2018

doesn't fit into the interactive paradigm used in Coq development

Concretely, what feature(s) do you mean doesn't (don't) fit?

@ejgallego

This comment has been minimized.

Copy link
Member Author

commented Mar 23, 2018

Concretely, what feature do you mean doesn't fit?

For instance, where is the LSP part dealing with goals and goal display?

@gares

This comment has been minimized.

Copy link
Member

commented Mar 23, 2018

@siegebell used external html files to print the goal (and I guess VS code can display them nicely)

@gares

This comment has been minimized.

Copy link
Member

commented Mar 23, 2018

@siegebell I've a question: you had a MITM speaking XML on one side and LSP on the other. Is the MITM generating the html out of a Goals XML call?

@herbelin

This comment has been minimized.

Copy link
Member

commented Mar 23, 2018

In parallel to following the good alternative initiatives mentioned in the thread, regarding CoqIDE in particular, are there technical reasons from Debian to drop support for gtk2 libs or is it before all a political decision. If before all a political decision, could Debian be sensitive to a collective request from lablgtk2 users (alt-ergo, frama-c, laby, marionnet, why3) friendly asking for maintaining the support, considering the high cost of migration to gtk3, and the great loss it would imply for these softwares?

@ejgallego

This comment has been minimized.

Copy link
Member Author

commented Mar 23, 2018

@herbelin it is a purely technical decision as the library is un maintained. Unfortunately I don't see a way back as they are right about deprecating the whole GNOME 2 infrastructure [I wish they would deprecate GNOME 3 too, but that's a different story XD]

@gares

This comment has been minimized.

Copy link
Member

commented Mar 23, 2018

Unless I'm mistaken Debian is not removing gtk2, it is removing gtksourceview2, that we use for syntax highlighting (and is an optional module of lablgtk2 as far as I know).
https://lists.debian.org/debian-devel/2018/02/msg00169.html

@MSoegtropIMC

This comment has been minimized.

Copy link
Contributor

commented Mar 23, 2018

Just a note: the Windows build scripts can build everything CoqIDE needs on top of basic C / OCaml libraries from sources (GTK including renderers like cairo and pango, a ton of support libraries, ...). It wouldn't be difficult to do the same for Linux. Just it takes a while to build (45 minutes or so), so one might want to split off the CoqIDE build from the main Coq build (and possibly also the GIT) to avoid a sluggish CI.

Mid term I think switching to VS Code might be the better option, but I think we should do this when we think it is a good time, and not when Debian thinks it is a good time.

So if gtk2 or lablgtk support is the only issue, I can provide Linux build scripts for CoqIDE which solve this, based on the Windows scripts (preferably using the same scripts for CoqIDE). Since the is really based on only very basic stuff, it should be low maintenance effort for quite some time.

Best regards,

Michael

@herbelin

This comment has been minimized.

Copy link
Member

commented Mar 23, 2018

it is a purely technical decision as the library is un maintained

Unless I'm mistaken Debian is not removing gtk2, it is removing gtksourceview2,

Ah, ok, I see better. Does this mean that if we propose ourselves as maintainer, gtksourceview2 could be kept (and why3 and others being able to take benefit of it also)?

[I don't feel competent about @MSoegtropIMC's proposal, but that seems to be otherwise a solution too.]

@Zimmi48

This comment has been minimized.

Copy link
Member

commented Mar 23, 2018

When you say "ourselves"? Who do you mean exactly? It can't be a collective pledge and I certainly would never pledge to be this maintainer.

@herbelin

This comment has been minimized.

Copy link
Member

commented Mar 23, 2018

"ourselves"?

= one person among the lablgtk2 users (in the worst case me for instance).

@gares

This comment has been minimized.

Copy link
Member

commented Mar 23, 2018

I think we should talk with the Debian people, they are nice guys.

The bug report has an email address, I just wrote a message to see if we can keep lablgtk2 without the gnome specific part of it (that we don't use) and gtksourceview (that we use, but could be removed from CoqIDE as a last resort).

@ppedrot

This comment has been minimized.

Copy link
Member

commented Mar 23, 2018

gtksourceview (that we use, but could be removed from CoqIDE as a last resort)

CoqIDE is already a pretty crappy text editor, hence removing gtksourceview would be essentially a death sentence...

@MSoegtropIMC

This comment has been minimized.

Copy link
Contributor

commented Mar 23, 2018

The version of gtksourceview we use (2.11) is from 2010 and unchanged since then. What I suggested is that if someone decides to stop delivering binaries for gtksourceview 2.11, we can just build it from sources. I don't see a substantial maintenance effort coming from building a library from sources which hasn't been touched for almost 8 years. Of cause it likely has all sorts of security vulnerabilities and things like that, which is likely why Debian wants to get rid of it, but I don't know if this is a substantial issue for CoqIDE. In any case it doesn't get any worse than it is now.

I would prefer to come up with a proactive plan (e.g. migration to VS Code, possibly with a native language server in Coq) rather than with forced reactions.

Best regards,

Michael

@MSoegtropIMC

This comment has been minimized.

Copy link
Contributor

commented Mar 23, 2018

P.S.: this applies recursively. As far as I understood Debian doesn't want to get rid of this because this stuff doesn't work or creates a lot of maintenance effort. It is just old and for this reason likely way insecure. This might not be much of an issue for CoqIDE (it would be e.g. for a banking app).

@siegebell

This comment has been minimized.

Copy link
Contributor

commented Mar 24, 2018

@gares the MITM is just converting the goals to json and passing them to the client (vscode extension). The client then displays a webpage in an editor page, and there is a script in the webpage part that converts it to HTML.

@siegebell

This comment has been minimized.

Copy link
Contributor

commented Mar 24, 2018

@ejgallego there are a bunch of methods that LSP itself does not define (step-forward, show-goals, etc.). But LSP is easily extended.

Assuming Coq supported LSP and the additional methods, blindly plugging the LSP into an editor will get you syntax-error reporting/highlighting, symbol/definition lookup, code-completion, etc. In vscode, at least, extensions/plugins are responsible for managing the LSP connection, so it's extremely easy to add support for the extended methods.

@ejgallego

This comment has been minimized.

Copy link
Member Author

commented Mar 24, 2018

plugging the LSP into an editor will get you syntax-error reporting/highlighting, symbol/definition lookup, code-completion, etc.

Coq cannot do completion well for technical reasons, syntax-error reporting is also fairly complicated to support properly with the current execution/document method, but that should become much easier once PLoF lands.

So yeah, most of the interesting bits still seem custom to me. This is what happened in LSP/Isabelle too.

@gares

This comment has been minimized.

Copy link
Member

commented Mar 24, 2018

@siegebell does LSP include messages to drive a debugger? The typical interaction with Coq is much closer to the one an editor has with a debugger than the one it has with a type checker.

@andres-erbsen

This comment has been minimized.

Copy link
Contributor

commented Mar 24, 2018

I would like to share my perspective on the ide-coq interaction, as it seems to be fairly different from how people are thinking on this thread. I hope you will find it interesting if not useful.

In my opinion, the most similar established model of interaction to coq editors is that of LaTeX. For a low-tech example, I edit LaTeX documents using three separate windows in the same layout as coqide: the .tex source in vim/mg, a pdf viewer displaying the work-in-progress document ("goals"), and a terminal running while : ; do make ; inotifywait -e modify *.tex ; done for error messages. The analogy can be extended to ProofGeneral commands: the entire document is processed when it is saved (C-c C-b -> C-x C-s), only a part of it is processed if I cut it off (C-c C-ret -> \end{document} C-x C-s), and moving the delimiter one line down allows for processing up to that line.

More generally, stepping forward in a document and cutting it short correspond to incremental compilation. If a new sentence has appeared at the end of the document, it can be processed on top of the existing state. If only the first half of the sentences in the file are the same as during the previous compilation, the compilation loop would cut the document only to that point and then (re-)add the following sentences (and process them in parallel). This approach does not require the editor to understand Coq sentences for processing them, though language-server-style editing aids can of course be very useful regardless. Note that this proposal is distinctly different from a "step forward, step back" debugger-style API.

I actually spent a couple of hours trying to implement an incremental compilation loop like this for Coq; I got stuck at reliable sentence parsing (coqide sentence parsing code, which I had been planning to use, turns out to depend on gtk). That can be overcome, though. Separately, there is the question of how to actually display the goals, but the xmlprotocol debug prints already look mostly readable, and it probably wouldn't be that difficult to render something more fancy in unicode/vt100+/HTML/LaTeX/etc. Depending on whether the editor (emacs?) or the window manager (xmonad?) is better suited for maintaining the layout, this display could be treated as an editor buffer or a separate window.

Despite the failure of my attempt to implement this, I think a low-tech frontend that works with any editor would be valuable for new users (enabling them to get their feet wet quickly) and as a low-tech option for when the favorite IDE of the day is not available.

@ejgallego

This comment has been minimized.

Copy link
Member Author

commented Mar 24, 2018

@andres-erbsen one has to be careful about taking away too much control as in some cases a single Coq sentence can take minutes (if not hours) to execute. Other than that the model your propose is OK and I'm generally moving towards it with my own work [for example the only thing holding jsCoq of working like that is the dreaded StackOverflows we get in JavaScript].

On the other hand, you are IMO using the wrong tool for splitting, you may want to check SerAPI out, in fact at some point full document incremental support will land there, as I am just done with the document model I want for a first version [due to holes not being easy to model].

@siegebell

This comment has been minimized.

Copy link
Contributor

commented Mar 25, 2018

@gares LSP does not have commands to drive the proof-interaction; I extended the protocol with my own commands (this was easy to do). Vscode also has an open debugger protocol, but I don't think it's any better than simply extending the LSP.

@gares

This comment has been minimized.

Copy link
Member

commented Mar 26, 2018

I see, I guess I should look more closely to LSP. Thanks for your insights @siegebell

@garrigue

This comment has been minimized.

Copy link

commented Mar 27, 2018

Quick follow-up on porting lablgtk2 to gtk3: after a quick look, it does not seem that hard.
LablGTK depends heavily on glib2 for its internals, but gtk3 is still built on glib2, so there should be no problem there.
So if the goal is just to be able to build lablgtk2 with gtk3 as backend, this shouldn't be too hard.
The list of API changes in the porting manual is pretty short.
The only major component that is lost is the old X11 based drawing primitives, but I don't think that any project uses them heavily. Cairo is to be used as a replacement, and there are already ocaml bindings to Cairo.
So the question is how much time we have to do the upgrade, to decide where to put the effort.

(Of course, there are many new things in gtk3, but we don't need to bind them to run legacy software. There are also niceties: it seems that gtk3 revives the GtkGlArea widget, which was lost in gtk2.)

@ejgallego

This comment has been minimized.

Copy link
Member Author

commented Mar 27, 2018

Quick follow-up on porting lablgtk2 to gtk3: after a quick look, it does not seem that hard.

Thanks @garrigue for the heads up. IMHO that's the most sensible choice, I could certainly help a bit with lablgtk3, maybe this would be a good moment to move the repository to github/gitlab ?

@garrigue

This comment has been minimized.

Copy link

commented Mar 27, 2018

There is already a repository garrigue/lablgtk on GitHub, since ocamlcore is now read-only.
I'll add you as developer. But I have first to cut a branch.

@ejgallego

This comment has been minimized.

Copy link
Member Author

commented Mar 27, 2018

Cool thanks! Let's open an issue there then to track porting progress.

@ejgallego

This comment has been minimized.

Copy link
Member Author

commented Mar 27, 2018

Oh, there is already an issue tracking it: garrigue/lablgtk#2

@garrigue

This comment has been minimized.

Copy link

commented Apr 2, 2018

See the above issue for progress on this port.
At this point the lablgtk2on3 branch compiles and links, but much functionality is lost.

@ejgallego

This comment has been minimized.

Copy link
Member Author

commented Feb 13, 2019

This can be closed once #9279 is merged.

@herbelin herbelin referenced this issue Feb 13, 2019

Merged

CoqIDE on lablgtk3 #9279

4 of 5 tasks complete

@ejgallego ejgallego added the part: IDE label Mar 19, 2019

@Zimmi48 Zimmi48 added this to the 8.10+beta1 milestone Mar 19, 2019

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.