Semantic Tokens

Stream: Emacs

[Lua Viana Reis]

Hi all,

I have now finished a package supporting semantic tokens in Eglot. It creates a new server class eglot-semtok-server which can be used in a user configuration or another package.

https://github.com/estradilua/eglot-semtok

[Lua Viana Reis]

I'm also working on a tree-sitter grammar and mode (but they may take some time to finish)

https://github.com/estradilua/tree-sitter-lean
https://github.com/estradilua/lean-ts-mode

[Richard Copley]

Lua Viana Reis said:

Mekeor Melire if you (or anyone else here) are working on Lean + Eglot, I have now finished a package supporting semantic tokens in Eglot. It creates a new server class eglot-semtok-server which can be used in a user configuration or another package.

https://github.com/estradilua/eglot-semtok

Hi @Lua Viana Reis,

I use a fork of lean4-mode adapted to Eglot.

The server class is registered in eglot-server-programs as follows (we delay constructing the LSP server command until the server is started, because it depends which version of Lake Elan selects):

(defun lean4--server-cmd ()
  "Return Lean server command.
If found lake version at least 3.1.0, then return '/path/to/lake serve',
otherwise return '/path/to/lean --server'."
  (condition-case nil
      (if (string-version-lessp (car (process-lines (lean4-get-executable "lake") "--version")) "3.1.0")
          `(,(lean4-get-executable lean4-executable-name) "--server")
        `(,(lean4-get-executable "lake") "serve"))
    (error `(,(lean4-get-executable lean4-executable-name) "--server"))))

;; Eglot init
(defun lean4--server-class-init (&optional _interactive)
  (cons 'lean4-eglot-lsp-server (lean4--server-cmd)))

(push (cons 'lean4-mode #'lean4--server-class-init) eglot-server-programs)

I'm not sure how to insert eglot-semtok-server. I tried replacing the init function lean4--server-class-init, like this [edited]:

    (require 'eglot-semtok)
    (defun my/lean4-server-class-init (&optional _interactive _project)
      `(eglot-semtok-server lean4-eglot-lsp-server ,@(lean4--server-cmd)))
    (push (cons 'lean4-mode #'my/lean4-server-class-init) eglot-server-programs)

It doesn't work. The message "[eglot] (warning) Wrong type argument: processp, nil" is printed and the LSP server is not started. Maybe I slipped up, or maybe this approach is doomed to fail. Before I try to debug, do you have any advice?

[Richard Copley]

Oh. Your README doesn't claim what I thought it claims. I think I need to change lean4-eglot-lsp-server to inherit from or delegate to eglot-semtok-server. I might try that some time.

[Lua Viana Reis]

Hi @Richard Copley,

as you realize, you have to change a line in lean4-mode.el:

- (defclass lean4-eglot-lsp-server (eglot-lsp-server) nil
+ (defclass lean4-eglot-lsp-server (eglot-semtok-server) nil

I have not tested this, but perhaps you can do that in your config too, i.e., redefine

(defclass lean4-eglot-lsp-server (eglot-semtok-server) nil
  :documentation "Eglot LSP server subclass for the Lean 4 server.")

after loading your package

[Lua Viana Reis]

after this, eglot should take care of initializing eglot-semtok-mode if the server supports it

[Lua Viana Reis]

Lua Viana Reis said:

after loading your package

if it doesn't work after, then I think there is a good chance it would work if you redefine before

[Richard Copley]

Lua Viana Reis said:

as you realize, you just have to change a line in lean4-mode.el:

- (defclass lean4-eglot-lsp-server (eglot-lsp-server) nil
+ (defclass lean4-eglot-lsp-server (eglot-semtok-server) nil

Great, thank you. I thought it would be harder! Looks very nice.

[Lua Viana Reis]

please report any semantic tokens issues you have, as there is a possibility that this could be upstreamed to eglot

[Notification Bot]

9 messages were moved here from #Emacs > ✔ Development: Maintainership by Richard Copley.

[Mekeor Melire]

There's also a package by Harald Kirsch that extends Eglot by semantic token support: https://codeberg.org/harald/eglot-supplements#semantic-tokens

[Lua Viana Reis]

@Mekeor Melire I did try what was available before writing something else.
But their implementation is problematic starting from the fact it hardcodes the colors for the tokens. It also completely replaces the major-mode fontification instead of extending it, and does not support delta requests.

[Lua Viana Reis]

also, a lot of "FIXME"s in there, and it won't request new data after buffer changes or will make requests too often, e.g. when scrolling the buffer

[Lua Viana Reis]

The semantic tokens feature has been merged into Eglot!

Unfortunately, João decided not to include the semanticTokens/refresh handler for now; this means that when a file takes a long time to elaborate (more than jsonrpc-default-request-timeout), the tokens will be missing, because they only become available after that. The Lean server then sends this notification (for instance, see this topic — only that unlike VSCode, Eglot would not eventually catch up with the highlighting).

[Lua Viana Reis]

(in fact, our Eglot implementation prompted lsp-mode to "fix" theirs; only that they fixed it in the wrong way, and unless I'm mistaken — I have only read, not tested their code — the lsp-mode tokens will blink every time you edit a file)

[Lua Viana Reis]

Lua Viana Reis said:

Unfortunately, João decided not to include the semanticTokens/refresh handler for now

That said, this can be fixed in the {lean-ts,nael}-mode side by implementing the handler ourselves. I still want to investigate the best way to do this, and after that I can send it here, or to upstream Eglot if that makes sense.

[Mekeor Melire]

@Lua Viana Reis, this is freaking awesome, congratulations!

[Mekeor Melire]

From my beginner's perspective, I agree that Eglot should have merged the handler for semanticTokens/refresh, too.

Without looking into it, I'd guess Lean major modes can define their own subclass of Eglot language servers and define a method on them? Similar to rocq-mode, for example: https://codeberg.org/jpoiret/rocq-mode.el/src/branch/main/rocq-mode.el

[Lua Viana Reis]

@Mekeor Melire this should suffice for now:

(cl-defmethod eglot-handle-request
  ((server nael-eglot-lsp-server) (_method (eql workspace/semanticTokens/refresh)))
  "Handle a semanticTokens/refresh request from SERVER."
  (dolist (buffer (eglot--managed-buffers server))
    (eglot--when-live-buffer buffer
      (setf (plist-get eglot--semtok-state :docver) nil)
      (eglot--widening (font-lock-flush)))))

but unfortunately, sometimes it does not! I have been testing the file examples/custom-genre/SimplePage/Demo.lean of the verso repository, and even in VSCode it sometimes looks like this:

image.png

but if I do Lean 4 Server: Restart Server, it looks like this instead:

image.png

[Lua Viana Reis]

until you edit something, and then it updates properly (and Eglot too)

[Lua Viana Reis]

Actually, in this specific example this is a bug in Verso. It is doing its own LSP request handling

[Mekeor Melire]

Thanks! I'll try out the snippet some time.