agda-mode syntax highlighting slows down Emacs signficantly

noughtmare commented 5 months ago

Summary

I have noticed that the highlighting of the agda-mode plugin makes my Emacs considerably less responsive. Many operations such as scrolling and inputting text incur a noticeable delay.

Reproducer

For example take the file that is generated by this Haskell script:

template n = 
  [ "foo" ++ show n ++ " : forall {X1 X2 X3 X4 : Set} -> (X1 -> X2 -> X3 -> X4) -> X1 -> X2 -> X3 -> X4"
  , "foo" ++ show n ++ " f x y z = f x y z"
  , ""
  ]

main = writeFile "test.agda" (unlines (concatMap template [1..100 :: Int]))

If I start a clean emacs with emacs -Q and then load agda-mode using this command:

(load-file (let ((coding-system-for-read 'utf-8))
                (shell-command-to-string "agda-mode locate")))

Then open test.agda and check it with C-c C-l. In the resulting highlighted file, scrolling with my mouse wheel or by dragging the scrollbar with my mouse has a very noticeable lag (it also seems to depend on the window size, at very small sizes it is not that noticeable). The lag disappears if I clear the highlighting with M-x agda2-highlight-clear.

I have also tried the same experiment with a highlighted C++ file which I generated by copying and pasting this example 5 times. That seems to have a similar amount of highlighting, but that does not suffer from the performance hit. So this doesn't seem to be inherent to Emacs highlighting.

Version info

OS: macOS Sonoma 14.3
Agda 2.6.4.1
GNU Emacs 29.2 (build 2, x86_64-apple-darwin23.3.0, NS appkit-2487.40 Version 14.3 (Build 23D56)) of 2024-01-27 (with --native-compilation)
- This is emacs-plus installed with:
```
$ brew tap d12frosted/emacs-plus
$ brew install emacs-plus@29 --with-native-comp
```

I can also reproduce this on a different machine with NixOS unstable (but it does seem less noticeable):

OS: NixOS 24.05pre567746.317484b1ead8 (Uakari)
Agda 2.6.4.1
GNU Emacs 29.1 (build 1, x86_64-pc-linux-gnu, X toolkit, cairo version 1.18.0, Xaw3d scroll bars)
- nix-shell -p emacs
Also with: GNU Emacs 28.2 (build 1, x86_64-pc-linux-gnu, GTK+ Version 3.24.38, cairo version 1.18.0)
- Although here dragging the scrollbar is fast, but scrolling with the mouse wheel can completely lock up if I scroll fast enough with my hyperscroll wheel, then it can takes seconds before it works through all the scroll events.
- nix-shell -p emacs28-gtk3

UlfNorell commented 5 months ago

I doesn't reproduce for me. I'm on Sonoma 14.2 (M1), and GNU Emacs 28.1 (don't know how to get the fancy stuff in parentheses). Scrolling has no detectable lag even full screen on a 4k display.

noughtmare commented 5 months ago

don't know how to get the fancy stuff in parentheses

I'm using M-x emacs-version

UlfNorell commented 5 months ago

Fancy stuff: GNU Emacs 28.1 (build 1, aarch64-apple-darwin21.1.0, NS appkit-2113.00 Version 12.0.1 (Build 21A559)) of 2022-05-11

dsheets commented 4 months ago

I have the same issue. I have tried to use emacs's profiling support to track it down to no avail.

OS: macOS Sonoma 14.2.1
Agda 2.6.4.1
GNU Emacs 29.1 (build 1, aarch64-apple-darwin21.6.0, NS appkit-2113.60 Version 12.6.6 (Build 21G646)) of 2023-08-17

dsheets commented 4 months ago

After downgrading to GNU Emacs 28.2 (build 1, aarch64-apple-darwin21.1.0, NS appkit-2113.00 Version 12.0.1 (Build 21A559)) of 2023-02-22 the performance has significantly improved.

The issue with the 29 series seems to be internal to the Emacs process itself and not the agda subprocess.

I run with emacsclient and the default Emacs for OS X builds I use were pointing bin and libexec to the x86_64-10_11 variant and with a 'fat' Emacs binary. I did switch the symlinks to the arm64-11 variant and I used lipo on the Emacs binary to retain only the arm64 executable but these actions seemed to have no noticeable impact on the poor performance.

I think my next task in this investigation would be to use profiling tools external to Emacs and perform a comparative analysis of 28.2 and 29.x to determine what seems to have regressed the UX.

noughtmare commented 4 months ago

It might be slightly faster, but the lag is still very noticeable for me on: GNU Emacs 28.2 (build 2, x86_64-apple-darwin23.3.0, NS appkit-2487.40 Version 14.3 (Build 23D56)) of 2024-02-22 (that's from brew install emacs-plus@28)

dsheets commented 4 months ago

I note that some of the components are still much newer. Could you try https://emacsformacosx.com/emacs-builds/Emacs-28.2-universal.dmg? It should be relatively easy to install/uninstall to/from /Applications and could help give us a differential. You might need to reinstall melpa packages or recompile agda-mode elisp or something, of course.

dsheets commented 4 months ago

I did not have these performance issues with:

OS: Linux 6.5.0-5-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.5.13-1 (2023-11-29) x86_64 GNU/Linux
Agda 2.6.3-b499d12
GNU Emacs 29.1 (build 1, x86_64-pc-linux-gnu, GTK+ Version 3.24.38, cairo version 1.16.0) of 2023-08-30, modified by Debian

andreasabel commented 4 months ago

I also find scrolling in a highlighted Agda file very slow: GNU Emacs 29.1 (build 2, x86_64-apple-darwin21.6.0, NS appkit-2113.60 Version 12.6.7 (Build 21G651)) of 2023-09-04 macOS 12.7.1 (21G920) Monterey Kernel Version: Darwin 21.6.0

noughtmare commented 4 months ago

Could you try https://emacsformacosx.com/emacs-builds/Emacs-28.2-universal.dmg?

Still noticeable lag. It may be slightly faster but it's hard to tell.

It gives me this version: GNU Emacs 28.2 (build 1, x86_64-apple-darwin18.7.0, NS appkit-1671.60 Version 10.14.6 (Build 18G95)) of 2023-02-22

agda / agda