search

m-fleury / isabelle-emacs

Clone of isabelle, with LSP extensions in seperate branches
Other
25 stars 5 forks source link

isabelle-emacs becomes slower and slower over time #78

Open gh-salt opened 1 year ago

gh-salt commented 1 year ago

Using emacs 28.2 with doom, we observe that everything becomes slower over time. We suspect this is a problem related to the non-deletion of overlays. A potential fix is under investigation:

adding (overlay-put ov 'evaporate t) in lsp-isar-decorations.el line 767.

m-fleury commented 1 year ago

Next time, can you give the output of:

(defun ap/garbage-collect ()
  "Run `garbage-collect' and print stats about memory usage."
  (interactive)
  (message (cl-loop for (type size used free) in (garbage-collect)
                    for used = (* used size)
                    for free = (* (or free 0) size)
                    for total = (file-size-human-readable (+ used free))
                    for used = (file-size-human-readable used)
                    for free = (file-size-human-readable free)
                    concat (format "%s: %s + %s = %s\n" type used free total))))
Mesabloo commented 1 year ago

Here is one run of this function when emacs turns notably slow (it has been for a bit now but it's becoming unmanageable): 

conses: 57.9M + 10.6M = 68.5M
symbols: 6.7M + 0 = 6.7M
strings: 12.2M + 1.2M = 13.3M
string-bytes: 10.3M + 0 = 10.3M
vectors: 11.4M + 0 = 11.4M
vector-slots: 51.1M + 8.6M = 59.7M
floats: 19.5k + 17.3k = 36.8k
intervals: 16.1M + 876.4k = 17M
buffers: 31k + 0 = 31k

Here is the result of a small profiling session I did (for about 5 to 8 minutes):

CPU profiling ``` Samples % Function 15431 30% + quail-input-method 13161 25% + ... 11158 21% + command-execute 3452 6% + timer-event-handler 2392 4% + redisplay_internal (C function) 2122 4% + # 2025 3% + jsonrpc--process-filter 331 0% hl-line-highlight 153 0% + company-post-command 139 0% + lsp-isar-caret-update-caret-position 67 0% + lsp--post-command 43 0% + flycheck-maybe-display-error-at-point-soon 35 0% + eldoc-pre-command-refresh-echo-area 30 0% + jit-lock--antiblink-post-command 29 0% + evil-repeat-post-hook 28 0% + winner-save-old-configurations 19 0% + evil--jump-hook 14 0% + undo-auto--add-boundary 12 0% + tooltip-show-help-non-mode 12 0% + sp--save-pre-command-state 12 0% + gcmh-register-idle-gc 8 0% + evil-normal-post-command 7 0% + which-key--hide-popup 5 0% + evil-repeat-pre-hook 5 0% + transient--post-command 4 0% + lsp-ui-sideline 4 0% yas--post-command-handler 4 0% + transient--pre-command 3 0% + sp--pair-overlay-post-command-handler 2 0% + delete-selection-pre-hook 2 0% + chain-doom-first-input-hook-to-pre-command-hook-h 2 0% company-pre-command 2 0% internal-timer-start-idle 2 0% + clear-transient-map 2 0% + evil-escape-pre-command-hook 2 0% + clear-transient-map 1 0% mouse--click-1-maybe-follows-link 1 0% evil--jump-handle-buffer-crossing 1 0% + substitute-command-keys ```

From that alone, it seems like Quail is at fault here. A detailed few of the functions called:

CPU profiling: Quail ``` Samples % Function 15431 30% - quail-input-method 15315 30% - quail-start-translation 15314 30% - if 15312 30% - let* 15262 30% - while 15247 30% - let* 14938 29% - read-key-sequence 14938 29% - apply 14938 29% - ad-Advice-read-key-sequence 14876 29% - # 1850 3% + # 414 0% + redisplay_internal (C function) 354 0% + jsonrpc--process-filter 269 0% + timer-event-handler 1 0% internal-timer-start-idle 309 0% + if 15 0% + quail-show-guidance 1 0% + or 110 0% # 3 0% + quail-input-string-to-events ```

Also notice that the second entry seems to be the garbage collector itself (although some functions are listed from the code of this package):

CPU profiling: garbage collector ``` Samples % Function 13161 25% - ... 13143 25% Automatic GC 11 0% - # 11 0% - apply 11 0% - # 11 0% - apply 11 0% - # 11 0% - if 11 0% - lsp-isar-kill-word-at-point 11 0% - lsp-isar-kill-thing-at-point 11 0% - let 11 0% - if 11 0% - kill-region 11 0% - filter-buffer-substring 11 0% - buffer-substring--filter 11 0% - # 11 0% - apply 11 0% - # 8 0% - delete-and-extract-region 6 0% - lsp-on-change 6 0% lsp--remove-overlays 2 0% jit-lock-after-change 5 0% - # 5 0% - apply 5 0% - # 5 0% - apply 5 0% - # 5 0% - if 5 0% - lsp-isar-kill-word-at-point 5 0% - lsp-isar-kill-thing-at-point 5 0% - let 5 0% - if 5 0% - kill-region 5 0% - filter-buffer-substring 5 0% - buffer-substring--filter 5 0% - # 5 0% - apply 5 0% # 2 0% + transient--init-objects ```

The third entry (which also seems shocking) comes from me pressing o in normal mode, I guess. I don't really understand why it is that slow though:

CPU profiling: "o" in normal mode ``` Samples % Function 10603 20% - funcall-interactively 4099 8% + evil-open-below 3321 6% + self-insert-command 1130 2% + counsel-M-x 543 1% + evil-ex 378 0% + evil-mouse-drag-region 218 0% + evil-normal-state 185 0% + evil-delete-backward-char-and-join 120 0% + newline-and-indent 78 0% + lsp-isar-insert-sledgehammer-and-call 51 0% + next-line 30 0% + lsp-isar-insert-sledgehammer-proof-1 21 0% + backward-kill-word 11 0% + unicode-tokens-delete-char 3 0% + evil-insert 3 0% + previous-line 2 0% + mouse-drag-region 2 0% evil-backward-char 2 0% + doom/toggle-profiler 351 0% + command-execute 100 0% + quail-input-method 30 0% hl-line-highlight 16 0% + lsp-isar-caret-update-caret-position 5 0% + flycheck-maybe-display-error-at-point-soon 5 0% + lsp--post-command 3 0% winner-save-old-configurations 3 0% + evil-repeat-pre-hook 1 0% + evil--jump-hook 1 0% + jit-lock--antiblink-post-command 1 0% yas--post-command-handler 1 0% + evil-repeat-post-hook 1 0% sp--post-command-hook-handler 1 0% list 1 0% + which-key--hide-popup 1 0% funcall 1 0% + handle-shift-selection ```

As for the memory profiling (same session), here it is:

Memory profiling ``` Bytes % Function 665,969,880 35% + command-execute 641,160,429 33% + # 359,446,115 19% + quail-input-method 106,920,140 5% + timer-event-handler 64,332,387 3% + redisplay_internal (C function) 34,601,117 1% + company-post-command 10,761,088 0% + lsp--post-command 4,354,768 0% + jsonrpc--process-filter 973,168 0% + winner-save-old-configurations 879,920 0% + lsp-isar-caret-update-caret-position 564,181 0% + gcmh-register-idle-gc 238,216 0% + evil-escape-pre-command-hook 197,048 0% + flycheck-maybe-display-error-at-point-soon 132,048 0% + lsp-ui-sideline 78,496 0% + evil-normal-post-command 76,632 0% + transient--post-command 63,424 0% + jit-lock--antiblink-post-command 39,791 0% + substitute-command-keys 18,624 0% + evil-repeat-post-hook 14,424 0% + evil-repeat-pre-hook 12,192 0% + eldoc-pre-command-refresh-echo-area 9,424 0% + sp--save-pre-command-state 7,044 0% + tooltip-show-help-non-mode 6,336 0% + which-key--hide-popup 5,280 0% + ... 5,280 0% + undo-auto--add-boundary 5,280 0% + eldoc-schedule-timer 3,764 0% + transient--pre-command 2,816 0% + sp--pair-overlay-post-command-handler 2,053 0% clear-minibuffer-message 1,056 0% + sp--post-command-hook-handler 392 0% mouse--click-1-maybe-follows-link 232 0% + gui-set-selection 232 0% + deactivate-mark 21 0% + # ```

Here are the two most memory-demanding functions:

Memory profiling: 1 ``` Bytes % Function 665,969,880 35% - command-execute 634,721,224 33% - funcall-interactively 283,357,755 14% - self-insert-command 244,185,340 12% - lsp-on-change 242,811,228 12% - lsp--remove-overlays 156 0% remove-overlays 1,033,912 0% + # 186,424 0% + run-with-idle-timer 148,496 0% + lsp--after-change 38,401,623 2% - sp--post-self-insert-hook-handler 28,950,108 1% - sp-insert-pair 15,478,128 0% - lsp-on-change 15,409,856 0% lsp--remove-overlays 53,224 0% + # 8,712 0% + run-with-idle-timer 6,336 0% + lsp--after-change 7,549,852 0% + delete-char 4,065,448 0% + sp--pair-to-insert 1,284,568 0% + sp--get-closing-regexp 117,616 0% + sp--pair-to-uninsert 20,240 0% + sp--run-hook-with-args 10,512 0% + flycheck-handle-change 2,816 0% + sp--pair-overlay-create 1,056 0% + lsp-before-change 880 0% sp--get-active-overlay 5,287,931 0% + sp-skip-closing-pair 3,716,032 0% + sp--all-pairs-to-insert 368,352 0% + sp-escape-open-delimiter 204,512 0% + flycheck-handle-change 35,776 0% + # 19,824 0% + lsp-before-change 8,288 0% jit-lock-after-change 6,336 0% + electric-indent-post-self-insert-function 432 0% + undo-auto--undoable-change 271,221,083 14% - evil-ex 261,815,228 13% - evil-ex-execute 261,791,620 13% - evil-ex-call-command 261,786,880 13% - funcall-interactively 261,786,880 13% - evil-write 261,786,880 13% - save-buffer 261,786,880 13% + basic-save-buffer 1,056 0% evil-ex-completed-binding 1,024 0% + evil-escape-pre-command-hook 1,024 0% + jit-lock--antiblink-post-command 860 0% + lsp-isar-caret-update-caret-position 120 0% + gcmh-register-idle-gc 80 0% flycheck-maybe-display-error-at-point-soon 21,568 0% + evil-ex-update 3,639,743 0% + # 1,596,444 0% + timer-event-handler 478,170 0% + redisplay_internal (C function) 51,832 0% + command-execute 23,624 0% + evil-ex-remove-default 20,660 0% + minibuffer-inactive-mode 4,144 0% winner-save-unconditionally 576 0% + gcmh-register-idle-gc 378 0% + minibuffer-mode 13,315,830 0% + counsel-M-x 11,710,587 0% + lsp-isar-insert-sledgehammer-and-call 11,566,565 0% + evil-mouse-drag-region 10,688,218 0% + evil-delete-backward-char-and-join 6,335,607 0% + evil-open-below 4,843,300 0% + newline-and-indent 3,512,872 0% + evil-normal-state 3,427,424 0% + doom/toggle-profiler 2,850,328 0% + next-line 2,254,468 0% + lsp-isar-insert-sledgehammer-proof-1 1,709,672 0% + backward-kill-word 1,127,656 0% + lsp-isar-delete-sledgehammer-call 890,928 0% + unicode-tokens-delete-char 64,392 0% + previous-line 40,828 0% + evil-insert 6,336 0% + mouse-drag-region 160 0% + evil-backward-char 29,914,856 1% + command-execute 879,952 0% + lsp--post-command 118,848 0% + winner-save-old-configurations 95,488 0% + quail-input-method 69,280 0% + lsp-isar-caret-update-caret-position 49,888 0% + gcmh-register-idle-gc 32,832 0% + flycheck-maybe-display-error-at-point-soon 30,160 0% + company-post-command 25,776 0% + lsp-ui-sideline 8,184 0% evil-repeat-pre-hook 3,168 0% + jit-lock--antiblink-post-command 1,056 0% + which-key--hide-popup 168 0% + handle-shift-selection ```
Memory profiling: 2 ``` Bytes % Function 641,160,429 33% - # 562,976,070 29% - mapc 562,976,070 29% - # 562,976,070 29% - lsp--parser-on-message 552,151,734 29% - lsp--on-notification 515,522,277 27% - lsp-isar-output-update-state-and-output-buffer 515,520,165 27% - let* 515,520,165 27% - if 515,520,165 27% - if 515,516,997 27% - lsp-isar-output--update-state-and-output-buffer-async 515,512,853 27% - save-excursion 515,509,685 27% - session-async-start 489,982,149 25% - jsonrpc-async-request 489,972,969 25% - jsonrpc--async-request-1 489,896,601 25% - jsonrpc-connection-send 489,896,601 25% - apply 489,892,377 25% + # 72,144 0% + # 1,056 0% list 34,349,139 1% + lsp-isar-decorations-update-and-reprint 1,566,588 0% + lsp-isar-progress--update-buffer 681,274 0% + lsp--on-diagnostics 26,120 0% + lsp--window-log-message 10,824,336 0% + # 21,726,679 1% + apply 548,704 0% + mapcar 35,696 0% + # ```

And then comes Quail:

Memory profiling: Quail (which we most likely can't do anything about) ``` Bytes % Function 359,446,115 19% - quail-input-method 359,386,235 19% - quail-start-translation 359,386,235 19% - if 359,385,187 19% - let* 359,381,043 19% - while 359,373,843 19% - let* 359,306,002 19% - read-key-sequence 359,306,002 19% - apply 359,306,002 19% - ad-Advice-read-key-sequence 238,839,980 12% - # 19,428,306 1% + redisplay_internal (C function) 15,605,620 0% + # 9,626,078 0% + timer-event-handler 1,361,460 0% + jsonrpc--process-filter 62,561 0% + if 6,144 0% + quail-show-guidance 57,768 0% + quail-input-string-to-events ```

I do not quite understand why my Emacs slows down that much (globally, any action takes time, even if seemingly unrelated to the Isabelle buffer), but we should have most of the information we need here.

m-fleury commented 1 year ago

I am wondering if we are seeing here the evil advice or something else:

  14938  29%         - ad-Advice-read-key-sequence
  14876  29%          - #<subr read-key-sequence>
   1850   3%           + #<compiled 0x1d8a69eb401801f9>
    414   0%           + redisplay_internal (C function)
    354   0%           + jsonrpc--process-filter
    269   0%           + timer-event-handler
      1   0%             internal-timer-start-idle

(Advised here: https://github.com/emacs-evil/evil/blob/2b2ba3cbeabe1f239b6b0ebdaddcb68dd158bd1f/evil-repeat.el#L634)

m-fleury commented 1 year ago

Okay here is a try. Right before (defun quail-start-translation (key) from unicode-tokens.el, add the following line:

(fset 'original-read-key-sequence (symbol-function 'read-key-sequence))

and replace all the read-key-sequence by original-read-key-sequence (taken from https://emacs.stackexchange.com/questions/16809/override-a-function-locally-but-allow-calls-to-the-original-function)