LSP Support

[gbaranski]

Hello, in features in README there is information about LSP support, but I can't find any more information about this, is it working? By the way, awesome project, I'm really looking into replacing neovim in future.

[vamolessa]

LSP support is there. Although only a subset of it. Currently we have:

• symbol hover
• signature help
• go to definition
• list symbol references
• symbol rename
• code actions
• list document symbols
• search workspace symbol
• document formatting
• code completion

Which is complete for my needs.

Usually, to start a lsp server, you want to do it automatically depending on the file extension of the active buffer. So there's a command for that. The way it works is by putting this in your init config.

# rust lsp
lsp "**/*.rs" "rust-analyzer" -log=rust-analyzer-log

# C# lsp
lsp "**/*.cs" "omnisharp -lsp --encoding utf-8" -log=omnisharp-log

# C/C++ lsp, not confirmed to work yet
# lsp "**/*.{c,h,cpp,hpp}" "clangd --offset-encoding=utf-8 --log=verbose" -log=clangd-log

For now, I only tested these language servers:

• rust-analyzer
• omnisharp
• clangd (I've only used it once and it worked, but I'll test it more once I resume my Unreal project)

Please let me know if you get it working on other lsp servers!

[leahneukirchen]

I tried it with lean4, and basic features work but it seems to lose connection with it. I'll look into that.

[leahneukirchen]

One minor thing: UTF-8 in the json responses is not decoded correctly, e.g. lean4 sends \342\206\222 which is an arrow, but pepper prints somelike like á.

[leahneukirchen]

I can't make much sense of the traces here, but it seems that lean sends after some point:

write(6, "Content-Length: 33\r\n\r\n{\"method\":\"exit\",\"jsonrpc\":\"2.0\"}", 55) = 55
...
write(2, "Watchdog error: Got outdated version number\n", 44) = 44

It seems lean expects the version number to increase with each edit, but pepper always sends 0 according to my traces?

[vamolessa]

I don't know that lsp server, would you mind linking a download/about page?

That json sequence seems weird, from looking the json specification it does not allow \ followed by some numbers. It does allow something like \uxxxx where x are hex digits, though, which should be supported. Event https://jsonlint.com/ tells that a json like { "a": "\342\206\222" } is invalid. Could you send the log or the full error you got from the lsp server?

It was true that the first version number was 0, so I just changed it to start from 1. Now I'm not sure how it would be stuck on 0. At least with rust-analyzer it increments as expected. Did you notice a textDocument/didChange notification in the logs? Something like:

send notification
method: 'textDocument/didChange'
params:
{"textDocument":{"uri":"file:///C:/Users/mathe/workspace/pepper/src/buffer.rs","version":1},"contentChanges":[{"range":{"start":{"line":10,"character":0},"end":{"line":10,"character":0}},"text":"a"}]}

[leahneukirchen]

It's a proof assistant, I used the binary here: https://github.com/leanprover/lean4/releases/tag/v4.0.0-m2

Run with ./bin/lean --server

As a small example you can use

def add3 (n m o : Nat) : Nat := 
  n + m + o 

#eval add3 6 7 8 

Hovering over #eval will show 21. Edit the line a bit and it will trigger the issue.

The version is actually hardcoded in https://github.com/vamolessa/pepper/blob/master/src/lsp/client.rs#L2368

Ah, I think I got the string from strace, so this is actually the raw bytes, no \. Run lsp-hover on the add3 in the #eval line to trigger that bug.

[vamolessa]

Just found the issue. We were checking the wrong server capability when checking if we should send document changes, also, fixed some other minor issues regarding when the lsp server log buffer is updated, the buffer versioning and some kind of "memory leak" where a versioned buffer would indefinitely accumulate pending edits.

Will close since it appears that the lean lsp server works as intended.

[gbaranski]

Awesome, does it support displaying errors? Something like that

[vamolessa]

Yes! When the server sends diagnostics, they're displayed in the statusbar when hovered with the main cursor: