Stream: Coq users

Topic: CoqIDE slowness on macOS


view this post on Zulip Théo Zimmermann (Jul 29 2020 at 10:02):

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.

view this post on Zulip Michael Soegtrop (Jul 29 2020 at 10:15):

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

view this post on Zulip Théo Zimmermann (Jul 29 2020 at 10:31):

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.

view this post on Zulip Ori Lahav (Jul 29 2020 at 10:33):

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)

view this post on Zulip Théo Zimmermann (Jul 29 2020 at 10:39):

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.

view this post on Zulip Ori Lahav (Jul 29 2020 at 10:47):

(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).

view this post on Zulip Théo Zimmermann (Jul 29 2020 at 10:54):

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)

view this post on Zulip Théo Zimmermann (Jul 29 2020 at 10:55):

BTW, I'm going to move this part of the discussion in a more appropriate location.

view this post on Zulip Notification Bot (Jul 29 2020 at 10:56):

This topic was moved here from #VsCoq devs & users > Search/SearchAbout by Théo Zimmermann

view this post on Zulip Ori Lahav (Jul 29 2020 at 11:06):

"-noinit" doesn't seem to change anything. I can try previous versions and reply here later.

view this post on Zulip Ori Lahav (Jul 29 2020 at 12:28):

checked 8.11.2. I think it is much better.

view this post on Zulip Théo Zimmermann (Jul 29 2020 at 12:32):

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.

view this post on Zulip Ori Lahav (Jul 29 2020 at 14:23):

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.

view this post on Zulip Ori Lahav (Jul 29 2020 at 14:26):

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)

view this post on Zulip Michael Soegtrop (Jul 29 2020 at 14:38):

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

view this post on Zulip Ori Lahav (Jul 29 2020 at 14:44):

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.

view this post on Zulip Théo Zimmermann (Jul 29 2020 at 14:49):

Yes, the version of GTK was upgraded from GTK2 to GTK3 in Coq 8.10.

view this post on Zulip David Nowak (Jul 29 2020 at 17:39):

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

view this post on Zulip Ori Lahav (Jul 30 2020 at 07:04):

Opening in "Low Resolution" using "Get Info" on the CoqIDE application really helps (in the price of a poor resolution).

view this post on Zulip Enrico Tassi (Jul 30 2020 at 11:45):

Hum, then maybe it's GTK related issue (CC @Jacques Garrigue )

view this post on Zulip Michael Soegtrop (Jul 30 2020 at 12:03):

Did someone compare the quartz vs X11 versions of GTK3 on macOS?

view this post on Zulip Jacques Garrigue (Jul 30 2020 at 12:09):

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

view this post on Zulip Enrico Tassi (Jul 30 2020 at 12:10):

CoqIDE is one process and Coq another one, they chat XML on a pipe. So guess it is not the GC

view this post on Zulip Ori Lahav (Jul 30 2020 at 12:21):

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.

view this post on Zulip Ori Lahav (Jul 30 2020 at 12:22):

Michael Soegtrop said:

Did someone compare the quartz vs X11 versions of GTK3 on macOS?

I am not sure how.

view this post on Zulip Michael Soegtrop (Jul 30 2020 at 13:59):

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.

view this post on Zulip Enrico Tassi (Jul 30 2020 at 14:39):

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

view this post on Zulip Enrico Tassi (Jul 30 2020 at 14:43):

The commit log says GTK 3.24.11

view this post on Zulip Enrico Tassi (Jul 30 2020 at 14:51):

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)

view this post on Zulip Ori Lahav (Jul 31 2020 at 08:13):

Added an issue:
https://github.com/coq/coq/issues/12779


Last updated: Mar 29 2024 at 09:02 UTC