LSP not compatible with Kate

[nishanthkarthik]

Prerequisites

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

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• 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

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

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

3. 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 6d22e0e, Release)

[nishanthkarthik]

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

[mhuisi]

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

[nishanthkarthik]

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.

lean4/src/Lean/Data/Lsp/InitShutdown.lean

Line 58 in 85f2213

structure InitializeParams where

/- 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]

4.14 rc2 works for me!