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?
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...
It's at least reassuring I'm not crazy, thanks for the confirmation :)
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.
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
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.
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 :)
Yeah I just to make sure which one is the culprit, giving up company-coq would be sad indeed. :)
IIRC there are related issues in (one of?) the issue trackers
IIRC for some reason, tons of “metadata” get attached to emacs coq buffers, and must be consulted upon redrawing
I found many issues about slowness, but did not spot one having to do with the amount of code on the screen specifically.
ah, https://github.com/cpitclaudel/company-coq/issues/145#issuecomment-268882664 might be relevant
yes, it’s “closed”, but a fix was not confirmed
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:
Thanks for the pointer, that could indeed be the same problem!
but not sure — some patch _was_ merged, but 4K screens are more common than in 2016?
anyway, good luck untangling this.
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
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
Quantic rooster...
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).
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.
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
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
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
@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?)
Yes, please try disabling it. ELisp performance can be counter-intuitive.
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.
OH NO IT'S THE ROOSTER :fear: :rooster:
Someone please make a PR. (Even better, someone also make a PR to Emacs to make the rooster fast… why would it cost more?)
@Yannick Zakowski are you on a Mac by chance? This is a known emacs issue that I can reproduce in any mode.
@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?
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
Thanks for the pointer!
I was disappointed to find out this is not Doom the game running on emacs.
Last updated: Oct 13 2024 at 01:02 UTC