PG
PG copied to clipboard
ProofGeneral
Performance issues with large coq files and evil vim commands
I'm experiencing the following odd behavior:
-
I open a fresh emacs instance with a large coq file (example file below) and every edit operation is fast as expected - independently of where the cursor is located in the buffer.
-
Then I check the complete buffer by using
proof-goto-pointat the buffer end, which causes some normal mode commands likeevil-delete-whole-line(pressingddin normal mode) to take multiple seconds to finish, but regular editing commands in insert mode are still fast (in particular deleting a line break with backspace). -
I retract the buffer by using
proof-goto-pointat the buffer beginning, but the slowdown persists. -
I run
proof-shell-restartand all commands are fast again.
I'm using the Coq spacemacs layer (without company-coq), but I don't think the behavior is caused by the layer, so I'm posting the issue here. Unfortunately, I'm not familiar enough with plain emacs to quickly test a pure evil mode + proof general setup.
This example file triggers the behavior on my machine and simply repeats the following code for 4000 lines:
Goal forall n1 n2, n1 + S n2 = S n1 + n2.
induction n1; intros; eauto.
simpl. rewrite IHn1. simpl. reflexivity.
Qed.
Can you collect a CPU profile? See https://www.gnu.org/software/emacs/manual/html_node/elisp/Profiling.html
I'm experiencing this same issue. I tried on a minimal Emacs configuration, the one recommended by PG's website:
(require 'package)
(let* ((no-ssl (and (memq system-type '(windows-nt ms-dos))
(not (gnutls-available-p))))
(proto (if no-ssl "http" "https")))
(add-to-list 'package-archives
(cons "melpa" (concat proto "://melpa.org/packages/")) t))
(package-initialize)
(custom-set-variables
'(package-selected-packages (quote (evil proof-general))))
I installed two packages from MELPA, PG and Evil and that's it, nothing more.
After processing the whole linked file, I invoked M-x evil-delete-whole-line on the last line and can confirm that the delay is substantial, about 1-2 seconds.
Here is cpu+mem profiler reports:
CPU Profiler Report
- command-execute 1458 96%
- call-interactively 1458 96%
- funcall-interactively 1054 70%
- execute-extended-command 1054 70%
- execute-extended-command--shorter 678 45%
- completion-try-completion 585 38%
- completion--nth-completion 585 38%
- completion--some 536 35%
- #<compiled 0x42f935f1> 536 35%
- completion-pcm-try-completion 441 29%
- completion-pcm--find-all-completions 411 27%
completion-pcm--all-completions 410 27%
+ completion-pcm--merge-try 30 1%
completion-basic-try-completion 95 6%
+ execute-extended-command--shorter-1 1 0%
- command-execute 273 18%
- call-interactively 273 18%
- byte-code 267 17%
- evil-operator-range 267 17%
evil-motion-range 267 17%
+ funcall-interactively 6 0%
+ sit-for 85 5%
- byte-code 404 26%
- read-extended-command 404 26%
- completing-read 404 26%
- completing-read-default 404 26%
- read-from-minibuffer 116 7%
+ command-execute 71 4%
+ redisplay_internal (C function) 2 0%
+ ... 46 3%
Memory Profiler Report
- command-execute 17,184,824 100%
- call-interactively 17,184,824 100%
- funcall-interactively 14,938,459 86%
- execute-extended-command 14,938,459 86%
- execute-extended-command--shorter 7,817,605 45%
- completion-try-completion 7,669,989 44%
- completion--nth-completion 7,665,789 44%
- completion--some 7,665,789 44%
- #<compiled 0x42f935f1> 7,665,789 44%
- completion-pcm-try-completion 7,656,553 44%
- completion-pcm--merge-try 7,314,467 42%
- completion-pcm--merge-completions 1,294,119 7%
- completion-pcm--pattern->regex 31,244 0%
- mapconcat 30,196 0%
#<compiled 0x42ede921> 12,576 0%
string-match 5,464 0%
try-completion 831 0%
completion-pcm--pattern->string 5,240 0%
+ completion-pcm--find-all-completions 327,366 1%
+ execute-extended-command--shorter-1 147,616 0%
- command-execute 5,876,755 34%
- call-interactively 5,876,755 34%
- funcall-interactively 4,435,827 25%
- profiler-report 4,433,779 25%
- profiler-report-cpu 2,538,483 14%
profiler-cpu-profile 1,837,392 10%
+ profiler-report-profile-other-window 701,091 4%
+ profiler-report-memory 1,895,296 11%
+ evil-delete-whole-line 2,048 0%
+ byte-code 1,440,896 8%
+ sit-for 199,130 1%
commandp 5,023 0%
+ byte-code 2,246,365 13%
... 0 0%
Can you collect a CPU profile? See https://www.gnu.org/software/emacs/manual/html_node/elisp/Profiling.html
Sure. Here are my profile reports for deleting 24 lines from the test document by repeatedly pressing dd.
When the slowdown occured, I got:
- command-execute 132599 98%
- call-interactively 132596 98%
- byte-code 132253 98%
- evil-operator-range 132015 98%
- evil-motion-range 131775 98%
+ evil-expand-range 37 0%
+ evil-normalize 1 0%
+ call-interactively 1 0%
+ evil-read-motion 200 0%
+ evil-change-state 22 0%
+ #<compiled 0x1b7d49d> 13 0%
+ evil-get-command-property 2 0%
+ helm-M-x-read-extended-command 237 0%
+ evil-yank-handler 1 0%
+ funcall-interactively 343 0%
whereas without the slowdown, I got:
- command-execute 1436 57%
- call-interactively 1434 57%
- byte-code 1158 46%
- evil-operator-range 922 36%
- evil-motion-range 438 17%
+ evil-expand-range 19 0%
+ call-interactively 4 0%
+ evil-type 2 0%
+ #<compiled 0x1b79929> 1 0%
+ evil-read-motion 396 15%
+ evil-change-state 58 2%
+ #<compiled 0x1b7d49d> 17 0%
+ evil-get-command-property 5 0%
evil-extract-count 3 0%
+ helm-M-x-read-extended-command 236 9%
- funcall-interactively 264 10%
+ next-line 109 4%
+ evil-delete 45 1%
+ evil-previous-line 28 1%
+ evil-normal-state 27 1%
+ list 9 0%
The slowdown in cpu cycles by a factor of ~100 is consistent with the slowdown in real time.
Does the slowdown happen during the processing of the file or after it?
Both. The slowdown increases proportionally to how much progress proof-goto-point made, and once processing finishes, the slowdown persists - even if the buffer gets retracted by running proof-goto-point at the beginning of the buffer.
The problem comes from evil-narrow-to-field, which calls field-beginning; calling just that function takes multiple seconds on my machine.
field-beginning is slow because of the large number of overlays, but I don't know how much we could do about this. There is a variable inhibit-field-text-motion that evil doesn't respect; if it did, setting this to t might be a good work-around (this may be worth a bug report on the evil side; then PG could set that variable by default in Coq buffers).
Alternatively, reviving the Emacs patch to make overlays faster might help with this issue. It's on branch feature/noverlay of the Emacs tree.
I think the following should work as a workaround, but obviously it's not a fix.
(defun ~/evil-motion-range--wrapper (fn &rest args)
"Like `evil-motion-range', but override field-beginning for performance.
See URL `https://github.com/ProofGeneral/PG/issues/427'."
(cl-letf (((symbol-function 'field-beginning)
(lambda (&rest args) 1)))
(apply fn args)))
(advice-add #'evil-motion-range :around #'~/evil-motion-range--wrapper)
The problem comes from
evil-narrow-to-field, which callsfield-beginning; calling just that function takes multiple seconds on my machine.
Sounds like a bug worth reporting to Emacs.
Does calling overlay-recenter just before the call help (if not, then
presumably "the Emacs patch to make overlays faster" won't help either).
Stefan
Out of curiosity -- if that function is unconditionally slow, why does the slowdown happen only if a large chunk of a big file is typechecked?
Thanks! The workaround works, indeed.
But it still seems odd to me, that checking the whole buffer and then retracting it (running proof-goto-point on the buffer begin), does affect the overlays at all. Shouldn't these operations act as inverses, and hence leave any state the same as in the beginning? In particular, there is no visual difference between the initial state and the state after checking & retracting again, so it seems odd that anything overlay related takes 100 times longer.
Out of curiosity -- if that function is unconditionally slow, why does the slowdown happen only if a large chunk of a big file is typechecked?
I think it's not unconditionally slow; only if there's many overlays.
But it still seems odd to me, that checking the whole buffer and then retracting it (running proof-goto-point on the buffer begin), does affect the overlays at all.
Yes, I'm not sure why PG leaves overlays after retracting. @Matafou ? Here's an example:
There are 2 overlays here:
From 121878 to 122000
keymap nil
modification-hooks (span-delete-self-modification-hook)
pg-span t
pghelp t
response ""
From 121922 to 121995
keymap nil
modification-hooks (span-delete-self-modification-hook)
pg-span t
pghelp t
response ""
Does calling
overlay-recenterjust before the call help (if not, then presumably "the Emacs patch to make overlays faster" won't help either).
It doesn't help.
AFAIK there is no reason why overlays remain after retracting. Except performance maybe. But on the other hand dealing with hundreds of overlays (maybe a few thousand) should not be such a problem. Should it? I'll see if we can remove them easily.
AFAIK there is no reason why overlays remain after retracting. Except performance maybe. But on the other hand dealing with hundreds of overlays (maybe a few thousand) should not be such a problem. Should it?
Indeed, it shouldn't be a problem. It's probably an algorithmic problem somewhere in the fields code.
Stefan
I found the reason why there are spans left in the buffer after retracting: 'pghelp spans are not removed. I think this is on purpose: these overlays are for the contextual tooltips popups and one may want to have them even if the region is retracted.
Since I cannot reproduce the bug on my laptop, @m0rphism can you try to apply this modification to you pg and see if the slow down disappears please?
file generic/proof-script.el line 405: replace the proof-script-delete-spans function by this one:
(defun proof-script-delete-spans (beg end)
"Delete primary spans between BEG and END. Secondary 'pghelp spans are left."
(span-delete-spans beg end 'type)
(span-delete-spans beg end 'idiom)
(span-delete-spans beg end 'pg-span)
)
If the this solves the slowdown, 1 obvious questions:
- should we remove tooltips from retracted regions? Or is it useful to someone. Certainly not to me.
Another question is:
- should we simply remove these tooltips menus? Or are they useful to someone? Certainly not to me.
Any opinion?
Since I cannot reproduce the bug on my laptop, @m0rphism can you try to apply this modification to you pg and see if the slow down disappears please?
While we'll probably need a workaround in Proof-General, the problem
seems to be fundamentally in field-beginning.
Has it been reported to Emacs yet?
should we remove tooltips from retracted regions? Or is it useful to someone. Certainly not to me.
Yes, let's remove them
should we simply remove these tooltips menus? Or are they useful to someone? Certainly not to me.
Not to me either. In fact, company-coq disables them.
commit 2ada467c2c2964a605659714f2a267db2c915952 removes pghelp spans when retracting a buffer. Let us discuss this further (and wait for @m0rphism to submit a bug to emacs) before really closing this bug.