lean4-mode lsp-bridge configuration Error.

[luixiao1223]

I added the following json in langserver

{
"name": "lake",
"languageId": "lean",
"command": [
"lake",
"serve"
],
"settings": {}
}

and followed the introductions at the new language server section. However, I received a "Watchdog error: Cannot read LSP request". the error message is:

Start lsp server (lake) for /Users/bianyixun/Documents/github/mathematics_in_lean

--- [09:12:04.943067] Send initialize request (2735) to 'lake' for project mathematics_in_lean
�[1;34minfo:�[m mathlib: updating repository '././.lake/packages/mathlib' to revision 'd951eef6bb39b3b78cbd1fba9c515c3770a9d20a'
�[1;34minfo:�[m batteries: updating repository '././.lake/packages/batteries' to revision 'cc0bc876eeef0518ddc1c8d3bd6f48cc83e68901'
�[1;34minfo:�[m Qq: updating repository '././.lake/packages/Qq' to revision 'fa3d73a2cf077f4b14c7840352ac7b08aeb6eb41'
�[1;34minfo:�[m aesop: updating repository '././.lake/packages/aesop' to revision 'b20a88676fd00affb90cbc9f1ff004ae588103b3'
�[1;34minfo:�[m proofwidgets: updating repository '././.lake/packages/proofwidgets' to revision 'baa65c6339a56bd22b7292aa4511c54b3cc7a6af'
�[1;34minfo:�[m importGraph: updating repository '././.lake/packages/importGraph' to revision '9b4088ccf0f44ddd7b1132bb1348aef8cf481e12'
Watchdog error: Cannot read LSP request: Unexpected param '{"rootUri":"file:///Users/bianyixun/Documents/github/mathematics_in_lean","rootPath":"/Users/bianyixun/Documents/github/mathematics_in_lean","processId":21216,"initializationOptions":{},"clientInfo":{"version":"lsp-bridge","name":"emacs"},"capabilities":{"workspace":{"symbol":{"resolveSupport":{"properties":[]}},"didChangeWatchedFiles":{"relativePatternSupport":true,"dynamicRegistration":true},"configuration":true},"window":{"workDoneProgress":true},"textDocument":{"rangeFormatting":{"dynamicRegistration":true},"publishDiagnostics":{"versionSupport":true,"tagSupport":{"valueSet":[1,2]},"relatedInformation":true,"dataSupport":true,"codeDescriptionSupport":true},"onTypeFormatting":{"dynamicRegistration":true},"inlayHint":{"dynamicRegistration":false},"hover":{"dynamicRegistration":true,"contentFormat":["markdown","plaintext"]},"formatting":{"dynamicRegistration":true},"completion":{"completionItem":{"tagSupport":{"valueSet":[1]},"snippetSupport":true,"resolveSupport":{"properties":["documentation","detail","additionalTextEdits"]},"deprecatedSupport":true}},"codeAction":{"isPreferredSupport":true,"dynamicRegistration":false,"codeActionLiteralSupport":{"codeActionKind":{"valueSet":["quickfix","refactor","refactor.extract","refactor.inline","refactor.rewrite","source","source.organizeImports"]}}}}}}' for method 'initialize'
Lean.Lsp.ClientCapabilities.workspace?: Lean.Lsp.WorkspaceClientCapabilities.applyEdit: Bool expected
q
--- [09:12:39.171573] LSP server 'lake' exited with code 1
b''

[manateelazycat]

Try below config?

{
  "name": "lake",
  "languageId": "lean",
  "command": [
    "lake",
    "serve"
  ],
  "settings": {},
  "initialization_options": {
    "capabilities": {
      "workspace": {
        "applyEdit": true
      }
    }
  }
}