PG
PG copied to clipboard
Extremely long lines stall the processing
I'm not sure whether this is related to: https://github.com/ProofGeneral/PG/issues/427
I have a generated file that contains extremely long one-line definitions (think > 10,000 characters). When these lines are being displayed, the processing of commands gets stalled (commands get locked and go pink, but never go blue).
When those lines are somehow hidden (by resizing the buffer, resizing the window, etc.), suddenly processing makes progress. When those lines are rendered again, the process stalls.
There are other events that help the processing go through (like opening a spacemacs-like menu).
To reproduce:
-
You can download this file which exhibits the problem: https://github.com/GaloisInc/saw-core-coq/blob/master/coq/generated/MEE_CBC.v (don't worry about grabbing the dependencies)
-
Open the file, make sure you can see line 44, and try to evaluate your buffer.
-
Supposedly, your buffer will turn pink, but not process.
-
If that's the case, now find a way to make line 44 not visible (for instance, resize your window and scroll up in the buffer).
There should be a distinct moment at which the processing will finally kick in (and you will get an error message about the files that you don't have).
I'm inclined to blame Emacs' known sluggishness on long lines; do you think it's likely to be something else?
I'm inclined to blame Emacs' known sluggishness on long lines;
Just to clarify: there isn't "the one Emacs sluggishness on long lines". Sadly (it would be easier to address). Instead, there are various problems that can occur in various cases (e.g font-lock, which operates at a line granularity).
I strongly suggest to look at a C backtrace during the "stall" (do it a few times, to get a couple of backtraces), which should pin point pretty quickly the main time-sink (there may be several, tho, so fixing the main one may not be sufficient).