Performance issues with large coq files and evil vim commands

[m0rphism]

I'm experiencing the following odd behavior:

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

2. Then I check the complete buffer by using proof-goto-point at the buffer end, which causes some normal mode commands like evil-delete-whole-line (pressing dd in 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).

3. I retract the buffer by using proof-goto-point at the buffer beginning, but the slowdown persists.

4. I run proof-shell-restart and 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.

[cpitclaudel]

Can you collect a CPU profile? See https://www.gnu.org/software/emacs/manual/html_node/elisp/Profiling.html

[Matafou]

Does the slowdown happen during the processing of the file or after it?

[anton-trunov]

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%

[m0rphism]

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.

[m0rphism]

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.

[cpitclaudel]

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.

[cpitclaudel]

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)

[monnier]

The problem comes from `evil-narrow-to-field`, which calls `field-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

[anton-trunov]

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?

[m0rphism]

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.

[cpitclaudel]

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             ""

[cpitclaudel]

Does calling overlay-recenter just before the call help (if not, then presumably "the Emacs patch to make overlays faster" won't help either).

It doesn't help.

[Matafou]

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.

[cpitclaudel]

I'll see if we can remove them easily.

Thanks!

[monnier]

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

[Matafou]

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

---

[Matafou]

If the this solves the slowdown, 1 obvious questions:

1. should we remove tooltips from retracted regions? Or is it useful to someone. Certainly not to me.

Another question is:

2. should we simply remove these tooltips menus? Or are they useful to someone? Certainly not to me.

Any opinion?

[monnier]

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?

[cpitclaudel]

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.

[cpitclaudel]

Has it been reported to Emacs yet?

Not by me ^^

[Matafou]

commit 2ada467 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.