Feel free to also report the slowness issues of CoqIDE to https://github.com/coq/coq/issues. I'm not sure that CoqIDE maintainers are aware of them. It might also be system-specific.
(used and liked Coqide before but it became so slow with recent updates...).
@Ori Lahav : Can you say which platform you use? I observed that on macOS it is indeed quite slow - not sure about other platforms. This might also depend on choices like GTK3 on quartz or on X.
The macOS slowness issue was reported once https://github.com/coq/coq/issues/11178, attributed to native-compute, and not really discussed anymore in the context of the IDE specifically. Apparently, the workaround is simply to recompile Coq without native compute support. In principle, this should already be the case in the provided macOS installer.
indeed macOS. I am not sure what to report, it is a general slowness feeling...
I installed via OPAM, so I think I am using GTK3. Are you saying there is another option?
(I had 8.9 before, so I am not saying it is related to 8.12)
I just checked and while native compute was disabled for 8.11.1 and 8.11.2 on opam, it wasn't anymore for 8.12.0 so it could be related to this bug.
(If it helps, the slowness I feel is even when opening a new "scratch" and just typing, no need to really invoke Coq.)
Let me know if there is something I can check on my side (with my minimal technical understanding of such issues).
Does it happen also if you run CoqIDE with -noinit
? Does it happen with Coq 8.11.2 ? And with Coq 8.11.0 ? (installed through opam)
BTW, I'm going to move this part of the discussion in a more appropriate location.
This topic was moved here from #VsCoq devs & users > Search/SearchAbout by Théo Zimmermann
"-noinit" doesn't seem to change anything. I can try previous versions and reply here later.
checked 8.11.2. I think it is much better.
OK now the final test would be to check whether it's again slow with 8.11.0. In which case, this would really mean that it is the native compute issue, but what is strange to me is that it is slow even if you haven't yet loaded anything in Coq.
Sorry, let me take my words back.
I did some super naive testing- open CoqIDE; maximize the window; open a Coq file; execute first line; go to line 300; and press the up-arrow and roughly measure the time it takes to reach line 1.
8.12: ~30sec
8.11.2: ~30sec
8.9.1: ~12sec (my beloved version + nice old colors :))
To me everything feels much faster with 8.9.1 (scrolling with the mouse, opening files, etc.)
So, not sure if it is at all related to the previous issue you mentioned.
I get these warnings (just once) when using 8.11.2 and 8.12 (but not 8.9.1) (shooting in the dark here)
(coqide:51218): Gtk-WARNING **: 17:09:53.362: Drawing a gadget with negative dimensions. Did you forget to allocate a size? (node header owner GtkNotebook)
(coqide:51218): Gtk-WARNING **: 17:09:53.362: Drawing a gadget with negative dimensions. Did you forget to allocate a size? (node tabs owner GtkNotebook)
(coqide:51218): Gtk-WARNING **: 17:09:53.362: Drawing a gadget with negative dimensions. Did you forget to allocate a size? (node tab owner GtkNotebook)
@Ori Lahav : How did you install GTK3? With opam depext? But even then I would think it needs either homebrew or MacPorts.
On macOS with MacPorts there are two variants of GTK3 - one uses quartz as backend and one uses X. One can choose this when one installs GTK3 via MacPorts. So far I only tested the quartz variant. This is indeed a bit slugish - at the edge of beeing usable. I don't think this has anything to do with native compute or so. It is a pure window issue. The macOS window manager consumes considerable amounts of CPU time when CoqIDE is running. I can't tell what it is - it must be worse than rerednering the complete window image for every keypress.
On Windows it looks quite OK, by contrast.
I used only opam, didn't need anything else.
Does 8.9 also use GTK3 or it uses a previous GTK version? Maybe GTK3 causes the slowdown.
For me CoqIDE becomes unusable :(
another much more minor difference (maybe fixable?): Home and End buttons that worked well in 8.9.1 do not work in the newer versions.
Yes, the version of GTK was upgraded from GTK2 to GTK3 in Coq 8.10.
Ori Lahav said:
indeed macOS. I am not sure what to report, it is a general slowness feeling...
I had exactly the same "feeling" when updating to 8.11, starting from 8.9. At first, CoqIDE was unusable. Disabling 'native compute' somehow alleviated this but it still feels slower than in 8.9 (as far as my memory is reliable).
Opening in "Low Resolution" using "Get Info" on the CoqIDE application really helps (in the price of a poor resolution).
Hum, then maybe it's GTK related issue (CC @Jacques Garrigue )
Did someone compare the quartz vs X11 versions of GTK3 on macOS?
This may be a GTK problem (but it completely depends on the widgets used, and I have no idea), or it may be a GC problem if Coq and LablGtk run in the same process. In that case you may look into adjusting the GC speed (see the README).
CoqIDE is one process and Coq another one, they chat XML on a pipe. So guess it is not the GC
I tried to "detach" the "Messages", "Jobs", "Errors" panels, so they are not shown in the same window. Although they are constantly empty in my test, this somehow really helps with the performance. So the problem may be for the widgets used to create these tables.
Michael Soegtrop said:
Did someone compare the quartz vs X11 versions of GTK3 on macOS?
I am not sure how.
Ori Lahav [said](https://coq.zulipchat.com/#narrow/stream/237977-Coq-
I am not sure how.
Although you said you didn't install it, you must have installed GTK3 somehow - either with homebrew, MacPorts, opam depext, manually or by other means. Maybe the output of pkg-config --cflags gtk+-3.0
sheds some light on where it comes from.
As far as I know the OSX .app bundles everything. I think it is generated by CI: https://github.com/coq/coq/blame/v8.12/azure-pipelines.yml#L63-L74 but I'm not 100% sure
The commit log says GTK 3.24.11
The changelog (of GTK) https://github.com/GNOME/gtk/blob/gtk-3-24/NEWS does not mention anything striking on OSX between .11 and .21 (which seems the most recent)
Added an issue:
https://github.com/coq/coq/issues/12779
Last updated: Oct 13 2024 at 01:02 UTC