LSP not compatible with Kate

nishanthkarthik commented 1 week ago

Prerequisites

Please put an X between the brackets as you perform the following steps:

[x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
[x] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
[x] Test your test case against the latest nightly release, for example on https://live.lean-lang.org/#project=lean-nightly (You can also use the settings there to switch to “Lean nightly”)

Description

Lean4 LSP does not work with Kate's LSP plugin. I understand Lean does not officially support all text editors, but I expected using lean --server to work. Kate works with about 20 other LSP servers, so I assume something's odd here.

Watchdog error: Cannot read LSP request: Unexpected param '{"workspaceFolders":[],"rootUri":"file:///home/user","rootPath":"/home/user","processId":13066,"capabilities":{"workspace":{"workspaceFolders":true},"window":{"workDoneProgress":true,"showMessage":{"messageActionItem":{"additionalPropertiesSupport":true}}},"textDocument":{"synchronization":{"didSave":true},"semanticTokens":{"tokenTypes":["namespace","type","class","enum","interface","struct","typeParameter","parameter","variable","property","enumMember","event","function","method","macro","keyword","modifier","comment","string","number","regexp","operator"],"tokenModifiers":[],"requests":{"range":true,"full":{"delta":true}},"formats":["relative"]},"selectionRange":{"dynamicRegistration":false},"publishDiagnostics":{"relatedInformation":true},"inlayHint":{"dynamicRegistration":false},"hover":{"contentFormat":["markdown","plaintext"]},"documentSymbol":{"hierarchicalDocumentSymbolSupport":true},"completion":{"completionItem":{"snippetSupport":true,"resolveSupport":{"properties":["additionalTextEdits","documentation"]}}},"codeAction":{"codeActionLiteralSupport":{"codeActionKind":{"valueSet":["quickfix","refactor","source"]}}}}}}' for method 'initialize'

Context

I am trying to use Lean LSP with new text editors

Steps to Reproduce

Add a custom file type called Lean for *.lean
Configure a LSP backend for Lean using the LSP plugin in Kate

    "lean": {
      "command": ["lean", "--server"],
      "highlightingModeRegex": "^Lean$"
    }

Open a Lean file

Expected behavior: LSP server works and highlights code

Actual behavior: LSP server crashes

Versions

Lean (version 4.13.0, x86_64-unknown-linux-gnu, commit 6d22e0e5cc5a, Release)

nishanthkarthik commented 1 week ago

The LSP spec supports most of the parameters used in initialization. Does lean lsp not like a particular field in the payload?

mhuisi commented 1 week ago

Could you try this on v4.14.0-rc2 as well?

nishanthkarthik commented 1 week ago

I think I see what's wrong. rootPath is not supported anymore, so I am not sure if the Lean LSP throws an error instead of silently discarding unknown keys. The following commit is almost HEAD on master.

https://github.com/leanprover/lean4/blob/85f2213d5a9a5e8cf09a5a61501576848ae8d144/src/Lean/Data/Lsp/InitShutdown.lean#L58

/- Many of these params can be null instead of not present.
    For ease of implementation, we're liberal:
    missing params, wrong json types and null all map to none,
    even if LSP sometimes only allows some subset of these.
    In cases where LSP makes a meaningful distinction
    between different kinds of missing values, we'll
    follow accordingly. -/

I'll try the binary build from https://github.com/leanprover/lean4/releases/tag/v4.14.0-rc2 and post an update

nishanthkarthik commented 1 week ago

4.14 rc2 works for me!

leanprover / lean4