Syntax highlighting is slow

[jthulhu]

Contrary to most major modes, syntax highlighting in lean4-mode is not instantaneous, in the sense that if I start typing def a : Nat :=, it won't syntax highlight until I have paused my typing, and even then there is a small delay. I haven't read the source code, but this behavior looks like as if syntax highlighting was actually performed by the language server, and passed through lsp, which I suspect is because parsing lean actually requires (at least partially) understanding what is parsed, due to the possible instructions to modify the parsing behavior.

Yet, this feels pretty annoying, and I was wondering if it was possible to make it more snappy.

[jthulhu]

After some research, I found that this was specifically due to the semantic tokens feature of LSP. Disabling it makes syntax highlighting much more snappy, even though the highlighting of tactics doesn't work anymore.

[mekeor]

this was specifically due to the semantic tokens feature of LSP

I suggest to close this issue as a consequence of this fact.

[jthulhu]

I mean, it's a workaround to simply disable the semantic tokens feature, but otherwise, this hasn't been "fixed". Fully-featured syntax highlighting is still slow.

[mekeor]

I see, alright. I was able to reproduce it and see the problem. I wonder how to find out whether the language server needs too long for this, or if it's due to lsp-mode, or if there's something we can do about this.

[mekeor]

I enabled LSP logging with M-: (setopt lsp-log-io t) and opened the logs in a lean4-mode-managed buffer with M-x lsp-switch-to-io-log-buffer. Then I inserted def a : Nat := a into the buffer and was then able to see that it takes quite a while until the semantic-token-related logs in reaction to this change occur in the log-buffer.

I now wonder if it's possible to make lean4-mode use font-lock fontification as soon as code is inserted and we're still waiting for the semantic-token-fontification.

[jthulhu]

I wonder how to find out whether the language server needs too long for this, or if it's due to lsp-mode

I asked someone with a VS Code setup to reproduce this issue, and they have the same problem, so presumably the slowness comes from the server. Yet, the Emacs plugin should still be capable of working around their slowness. For instance:

make lean4-mode use font-lock fontification as soon as code is inserted and we're still waiting for the semantic-token-fontification.

However, I am quite the elisp noob, so I wouldn't know where to start to make this happen.

An other option would be to raise this issue at the server side, to see if it's possible / reasonably easy to optimise this on their end, which would solve the problem at the root.