Stream: Coq users

Topic: PG slower with high res monitor?


view this post on Zulip Yannick Zakowski (Nov 22 2020 at 18:22):

After months working remotely directly on my laptop, I have been enjoying recently a 32'' monitor enjoying some 3840 x 2160 resolution. I've been able to see my whole goal at once, Ô joy.
However, processing files in PG is significantly slower when plugged in the monitor, to the point of being unusable on large files. Would anyone have any idea why that would be, and how to fix it?

view this post on Zulip Fabian Kunze (Nov 22 2020 at 18:34):

I made the observation that PG with company coq gets slower the larger the visible area of the file buffer: when i resize the window to be smaller, the stepping-through the file got faster I did not find any solution and now use vscoq because of this on my 4k screen.
Sorry that this is not what you wanted to hear...

view this post on Zulip Yannick Zakowski (Nov 22 2020 at 18:40):

It's at least reassuring I'm not crazy, thanks for the confirmation :)

view this post on Zulip Théo Winterhalter (Nov 22 2020 at 19:15):

With company-coq, I think someone showed that stepping through while clicking on "File"/"Edit"/... or any contextual menu also sped things up because it was not focusing on refreshing the view or something.

view this post on Zulip Yannick Zakowski (Nov 23 2020 at 08:35):

So that would be specifically an issue with company-coq rather than PG? I'm going to open an issue, I would really love not to have to switch ide

view this post on Zulip Théo Winterhalter (Nov 23 2020 at 08:46):

You can try deactivating company-coq and see if the problem is still there. I suspect that both PG and coompany-coq suffer from inefficiencies.

view this post on Zulip Yannick Zakowski (Nov 23 2020 at 08:49):

Yes I'm going to give a shot at this asap as well out of curiosity, although I would miss my company-coq as well :)

view this post on Zulip Théo Winterhalter (Nov 23 2020 at 08:50):

Yeah I just to make sure which one is the culprit, giving up company-coq would be sad indeed. :)

view this post on Zulip Paolo Giarrusso (Nov 23 2020 at 09:04):

IIRC there are related issues in (one of?) the issue trackers

view this post on Zulip Paolo Giarrusso (Nov 23 2020 at 09:06):

IIRC for some reason, tons of “metadata” get attached to emacs coq buffers, and must be consulted upon redrawing

view this post on Zulip Yannick Zakowski (Nov 23 2020 at 09:08):

I found many issues about slowness, but did not spot one having to do with the amount of code on the screen specifically.

view this post on Zulip Paolo Giarrusso (Nov 23 2020 at 09:10):

ah, https://github.com/cpitclaudel/company-coq/issues/145#issuecomment-268882664 might be relevant

view this post on Zulip Paolo Giarrusso (Nov 23 2020 at 09:11):

yes, it’s “closed”, but a fix was not confirmed

view this post on Zulip Paolo Giarrusso (Nov 23 2020 at 09:11):

Interestingly, the issue seems to be far more severe when emacs is full-screen (tests suggest that it's the size of the window, and not the full-screenness nor whether the frames are displayed vertically vs horizontal split, that matters). In the following, unpatched is on the left, patched is on the right:

view this post on Zulip Yannick Zakowski (Nov 23 2020 at 09:12):

Thanks for the pointer, that could indeed be the same problem!

view this post on Zulip Paolo Giarrusso (Nov 23 2020 at 09:13):

but not sure — some patch _was_ merged, but 4K screens are more common than in 2016?

view this post on Zulip Paolo Giarrusso (Nov 23 2020 at 09:14):

anyway, good luck untangling this.

view this post on Zulip Yannick Forster (Nov 23 2020 at 09:25):

Happy that somebody takes up this issue! This precise problem motivated me to move to VsCoq, but I still miss PG features sometimes. For me, pressing Ctrl+X Ctrl+S (i.e. save file) repeatedly also sped up the compilation process, probably for the same reason why clicking File helps. If I remember correctly @Matthieu Sozeau (or was it somebody else?) recommended a shortcut with only one key with the same result, that might be more muscle-friendly as a quick-fix

view this post on Zulip Yannick Zakowski (Nov 23 2020 at 10:40):

Some first janky tests seem to show that indeed:

Processing a 3.8kloc file on a Mac book pro, starting from a fresh coqtop each time.

No external monitor, 52 lines displayed at once:

 - 2’16 with company-coq while looking at it
 - 1’34 without company-coq while looking at it
 - 0’55 with company-coq without looking at it
 - < 0’30 without company-coq without looking at it

4K monitor, 117 lines displayed at once:
 - ~ 3’25 with company-coq while looking at it
 - ~ 1’40 without company-coq while looking at it
 - ~ 2’05 with company-coq without looking at it
 - ~ 0’50 without company-coq without looking at it

view this post on Zulip Kenji Maillard (Nov 23 2020 at 10:53):

Quantic rooster...

view this post on Zulip Stefan Monnier (Nov 23 2020 at 14:04):

The increased time with more lines as well as the lower time when "not watching" (which I guess means the buffer is not displayed, and not that you're just closing your eyes) point quite directly to Emacs spending all this extra time in the redisplay, hence either redisplaying too often, or redoing too much work at each redisplay, or both.
You can probably reduce the impact of company-coq by disabling its mode-line spinner, but since the slowdown is already significant without company-coq, further investigation is warranted. I suggest you file a bug report against PG, and you'll probably want to include some profiling info (M-x profiler-start RET RET ... M-x profiler-report RET followed by C-u RET to expand the more interesting subtrees).

view this post on Zulip Yannick Zakowski (Nov 23 2020 at 14:12):

Thanks a lot for the information Stefan! I'll run some profiling and feel an issue Tonight or Tomorrow.
And yes indeed my cheeky "without looking" meant basically having the window of my browser opened on top of it. I know nothing in Emacs's display, I do not know if it's equivalent to keeping the window "visible" in screen but having it not in focus, or even keeping the window in focus but in another buffer.

view this post on Zulip Paolo Giarrusso (Nov 23 2020 at 14:19):

About things getting slower, there was IIRC discussion about overlays being “leaked” or simply
having the wrong growth. But I should tag @Clément Pit-Claudel instead

view this post on Zulip Clément Pit-Claudel (Nov 23 2020 at 14:34):

Can you guys try to turn of the spinning rooster thing? It's cute and cheeky and all but in recent Emacsen it seems to make everything slower. Maybe it's time to stop the spin. M-x company-coq-features/spinner

view this post on Zulip Clément Pit-Claudel (Nov 23 2020 at 14:35):

I'm going to be so sad if it's the spinning rooster's fault. That spinning rooster is one of my proudest achievements :P

view this post on Zulip Joshua Grosso (Nov 23 2020 at 19:45):

@Clément Pit-Claudel Hmm, it hadn't occurred to me in my https://github.com/ProofGeneral/PG/issues/524 issue to mention that I'm using a MB Retina monitor... maybe that's the issue after all?
(Also, should I try disabling the spinner even if it's not visible in my modeline?)

view this post on Zulip Clément Pit-Claudel (Nov 23 2020 at 19:46):

Yes, please try disabling it. ELisp performance can be counter-intuitive.

view this post on Zulip Yannick Zakowski (Nov 24 2020 at 13:44):

Ok I need more tests, but my emacs was back to a pathological drag on my monitor, I just deactivated the spinning rooster and it suddenly is extremely fast... I'm a bit suspicious that it can be only circumstantial, but that might be it!
Worst part is that the rootser didn't even display on my emacs, I can't even say it was worth it.

view this post on Zulip Clément Pit-Claudel (Nov 25 2020 at 02:15):

OH NO IT'S THE ROOSTER :fear: :rooster:

view this post on Zulip Clément Pit-Claudel (Nov 25 2020 at 02:16):

Someone please make a PR. (Even better, someone also make a PR to Emacs to make the rooster fast… why would it cost more?)

view this post on Zulip Rudi Grinberg (Dec 07 2020 at 03:56):

@Yannick Zakowski are you on a Mac by chance? This is a known emacs issue that I can reproduce in any mode.

view this post on Zulip Yannick Zakowski (Dec 07 2020 at 07:35):

@Rudi Grinberg I am indeed on Mac. Can you be more specific as to what would be the issue and whether there is a fix for it please?

view this post on Zulip Rudi Grinberg (Dec 07 2020 at 13:36):

Here's an example of doom users running into it. https://github.com/hlissner/doom-emacs/issues/2217 You can see various workarounds such as changing font settings

view this post on Zulip Yannick Zakowski (Dec 07 2020 at 15:52):

Thanks for the pointer!

view this post on Zulip Li-yao (Dec 07 2020 at 15:59):

I was disappointed to find out this is not Doom the game running on emacs.


Last updated: Jan 29 2023 at 01:02 UTC