lean language server ignoring default options

[danjenson]

Summary

I am using the lean language server for Lean 4, however, none of the options listed here: https://github.com/leanprover/vscode-lean appear to be working. In particular, I'd like it to replace commands like \to with unicode symbols. I even added

[[language]]
name = "lean"
config = { lean.input.eagerReplacementEnabled = true }  # should already be the default

to my languages.toml, but it seems to have no effect.

Reproduction Steps

1. Install elan: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
2. Update elan: elan self update
3. Install Lean 4, set as default: elan default leanprover/lean4:stable
4. Edit a file: hx t.lean
5. Try to type anything, i.e. a \to b, where \to should be replaced with right arrow.

Helix log

2023-03-22T11:22:08.157 helix_loader [DEBUG] Located configuration folders: ["/data/repos/lean/.helix"]
2023-03-22T11:22:08.174 helix_view::clipboard [DEBUG] Using xclip to interact with the system and selection (primary) clipboard
2023-03-22T11:22:08.548 mio::poll [TRACE] registering event source with poller: token=Token(0), interests=READABLE | WRITABLE
2023-03-22T11:22:08.548 mio::poll [TRACE] registering event source with poller: token=Token(1), interests=READABLE | WRITABLE
2023-03-22T11:22:08.548 mio::poll [TRACE] registering event source with poller: token=Token(2), interests=READABLE | WRITABLE
2023-03-22T11:22:08.548 helix_view::editor [DEBUG] editor status: Loaded 1 file.
2023-03-22T11:22:08.548 helix_lsp::client [INFO] Using custom LSP config: {"lean":{"input":{"eagerReplacementEnabled":true}}}
2023-03-22T11:22:08.548 mio::poll [TRACE] registering event source with poller: token=Token(3), interests=READABLE | WRITABLE
2023-03-22T11:22:08.548 mio::poll [TRACE] registering event source with poller: token=Token(4), interests=READABLE | WRITABLE
2023-03-22T11:22:08.548 helix_lsp::transport [INFO] -> {"jsonrpc":"2.0","method":"initialize","params":{"capabilities":{"general":{"positionEncodings":["utf-32","utf-8","utf-16"]},"textDocument":{"codeAction":{"codeActionLiteralSupport":{"codeActionKind":{"valueSet":["","quickfix","refactor","refactor.extract","refactor.inline","refactor.rewrite","source","source.organizeImports"]}}},"completion":{"completionItem":{"deprecatedSupport":true,"insertReplaceSupport":true,"resolveSupport":{"properties":["documentation","detail","additionalTextEdits"]},"snippetSupport":true,"tagSupport":{"valueSet":[1]}},"completionItemKind":{}},"hover":{"contentFormat":["markdown"]},"inlayHint":{"dynamicRegistration":false},"publishDiagnostics":{"versionSupport":true},"rename":{"dynamicRegistration":false,"honorsChangeAnnotations":false,"prepareSupport":true},"signatureHelp":{"signatureInformation":{"activeParameterSupport":true,"documentationFormat":["markdown"],"parameterInformation":{"labelOffsetSupport":true}}}},"window":{"workDoneProgress":true},"workspace":{"applyEdit":true,"configuration":true,"didChangeConfiguration":{"dynamicRegistration":false},"executeCommand":{"dynamicRegistration":false},"inlayHint":{"refreshSupport":false},"symbol":{"dynamicRegistration":false},"workspaceEdit":{"documentChanges":true,"failureHandling":"abort","normalizesLineEndings":false,"resourceOperations":["create","rename","delete"]},"workspaceFolders":true}},"clientInfo":{"name":"helix","version":"22.12 (05e7862e)"},"initializationOptions":{"lean":{"input":{"eagerReplacementEnabled":true}}},"processId":20960,"rootPath":"/data/repos/lean","rootUri":"file:///data/repos/lean","workspaceFolders":[{"name":"lean","uri":"file:///data/repos/lean"}]},"id":0}
2023-03-22T11:22:08.548 mio::poll [TRACE] registering event source with poller: token=Token(0), interests=READABLE
2023-03-22T11:22:08.548 mio::poll [TRACE] registering event source with poller: token=Token(1), interests=READABLE
2023-03-22T11:22:08.548 helix_tui::backend::crossterm [DEBUG] The keyboard enhancement protocol is not supported in this terminal (checked in 226.985µs)
2023-03-22T11:22:08.549 helix_view::document [DEBUG] id 1 modified - last saved: 0, current: 0
2023-03-22T11:22:08.575 helix_term::application [DEBUG] received editor event: IdleTimer
2023-03-22T11:22:08.880 helix_lsp::transport [INFO] <- {"result":{"serverInfo":{"version":"0.1.1","name":"Lean 4 Server"},"capabilities":{"workspaceSymbolProvider":true,"typeDefinitionProvider":true,"textDocumentSync":{"willSaveWaitUntil":false,"willSave":false,"openClose":true,"change":2},"semanticTokensProvider":{"range":true,"legend":{"tokenTypes":["keyword","variable","property","function","namespace","type","class","enum","interface","struct","typeParameter","parameter","enumMember","event","method","macro","modifier","comment","string","number","regexp","operator","decorator"],"tokenModifiers":["declaration","definition","readonly","static","deprecated","abstract","async","modification","documentation","defaultLibrary"]},"full":true},"referencesProvider":true,"hoverProvider":true,"foldingRangeProvider":true,"documentSymbolProvider":true,"documentHighlightProvider":true,"definitionProvider":true,"declarationProvider":true,"completionProvider":{"triggerCharacters":["."],"resolveProvider":false}}},"jsonrpc":"2.0","id":0}
2023-03-22T11:22:08.880 helix_lsp::transport [INFO] <- {"capabilities":{"completionProvider":{"resolveProvider":false,"triggerCharacters":["."]},"declarationProvider":true,"definitionProvider":true,"documentHighlightProvider":true,"documentSymbolProvider":true,"foldingRangeProvider":true,"hoverProvider":true,"referencesProvider":true,"semanticTokensProvider":{"full":true,"legend":{"tokenModifiers":["declaration","definition","readonly","static","deprecated","abstract","async","modification","documentation","defaultLibrary"],"tokenTypes":["keyword","variable","property","function","namespace","type","class","enum","interface","struct","typeParameter","parameter","enumMember","event","method","macro","modifier","comment","string","number","regexp","operator","decorator"]},"range":true},"textDocumentSync":{"change":2,"openClose":true,"willSave":false,"willSaveWaitUntil":false},"typeDefinitionProvider":true,"workspaceSymbolProvider":true},"serverInfo":{"name":"Lean 4 Server","version":"0.1.1"}}
2023-03-22T11:22:08.880 helix_lsp::transport [INFO] <- {"params":{"registrations":[{"registerOptions":{"watchers":[{"kind":null,"globPattern":"**/*.ilean"}]},"method":"workspace/didChangeWatchedFiles","id":"ilean_watcher"}]},"method":"client/registerCapability","jsonrpc":"2.0","id":"register_ilean_watcher"}
2023-03-22T11:22:08.880 helix_lsp::transport [INFO] -> {"jsonrpc":"2.0","method":"initialized","params":{}}
2023-03-22T11:22:08.880 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, MethodCall(MethodCall { jsonrpc: Some(V2), method: "client/registerCapability", params: Map({"registrations": Array [Object {"id": String("ilean_watcher"), "method": String("workspace/didChangeWatchedFiles"), "registerOptions": Object {"watchers": Array [Object {"globPattern": String("**/*.ilean"), "kind": Null}]}}]}), id: Str("register_ilean_watcher") })))
2023-03-22T11:22:08.880 helix_term::application [WARN] Ignoring a client/registerCapability request because dynamic capability registration is not enabled. Please report this upstream to the language server
2023-03-22T11:22:08.880 helix_lsp::transport [INFO] -> {"jsonrpc":"2.0","result":null,"id":"register_ilean_watcher"}
2023-03-22T11:22:08.880 helix_view::document [DEBUG] id 1 modified - last saved: 0, current: 0
2023-03-22T11:22:08.880 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: None, method: "initialized", params: None })))
2023-03-22T11:22:08.880 helix_lsp::transport [INFO] -> {"jsonrpc":"2.0","method":"workspace/didChangeConfiguration","params":{"settings":{"lean":{"input":{"eagerReplacementEnabled":true}}}}}
2023-03-22T11:22:08.880 helix_lsp::transport [INFO] -> {"jsonrpc":"2.0","method":"textDocument/didOpen","params":{"textDocument":{"languageId":"lean","text":"theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p :=\n  fun hpq : p ∧ q =>\n  have hp : p := And.left hpq\n  have hq : q := And.right hpq\n  p \\to q\n  show q ∧ p from And.intro hq hp\n","uri":"file:///data/repos/lean/t.lean","version":0}}}
2023-03-22T11:22:08.882 helix_lsp::transport [ERROR] err <- "Got unsupported notification: workspace/didChangeConfiguration\n"
2023-03-22T11:22:08.882 helix_lsp::transport [INFO] <- {"params":{"textDocument":{"version":0,"uri":"file:///data/repos/lean/t.lean"},"processing":[{"range":{"start":{"line":0,"character":0},"end":{"line":6,"character":0}},"kind":1}]},"method":"$/lean/fileProgress","jsonrpc":"2.0"}
2023-03-22T11:22:08.882 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "$/lean/fileProgress", params: Map({"processing": Array [Object {"kind": Number(1), "range": Object {"end": Object {"character": Number(0), "line": Number(6)}, "start": Object {"character": Number(0), "line": Number(0)}}}], "textDocument": Object {"uri": String("file:///data/repos/lean/t.lean"), "version": Number(0)}}) })))
2023-03-22T11:22:08.882 helix_term::application [ERROR] received malformed notification from Language Server: Unhandled
2023-03-22T11:22:08.976 helix_lsp::transport [INFO] <- {"params":{"version":0,"uri":"file:///data/repos/lean/t.lean","diagnostics":[]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}
2023-03-22T11:22:08.976 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "textDocument/publishDiagnostics", params: Map({"diagnostics": Array [], "uri": String("file:///data/repos/lean/t.lean"), "version": Number(0)}) })))
2023-03-22T11:22:08.977 helix_view::document [DEBUG] id 1 modified - last saved: 0, current: 0
2023-03-22T11:22:08.982 helix_lsp::transport [INFO] <- {"params":{"textDocument":{"version":0,"uri":"file:///data/repos/lean/t.lean"},"processing":[{"range":{"start":{"line":0,"character":0},"end":{"line":6,"character":0}},"kind":1}]},"method":"$/lean/fileProgress","jsonrpc":"2.0"}
2023-03-22T11:22:08.982 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "$/lean/fileProgress", params: Map({"processing": Array [Object {"kind": Number(1), "range": Object {"end": Object {"character": Number(0), "line": Number(6)}, "start": Object {"character": Number(0), "line": Number(0)}}}], "textDocument": Object {"uri": String("file:///data/repos/lean/t.lean"), "version": Number(0)}}) })))
2023-03-22T11:22:08.982 helix_term::application [ERROR] received malformed notification from Language Server: Unhandled
2023-03-22T11:22:08.987 helix_lsp::transport [INFO] <- {"params":{"version":0,"uri":"file:///data/repos/lean/t.lean","diagnostics":[{"source":"Lean 4","severity":1,"range":{"start":{"line":4,"character":2},"end":{"line":4,"character":3}},"message":"type mismatch\n  p\nhas type\n  Prop : Type\nbut is expected to have type\n  q ∧ p : Prop","fullRange":{"start":{"line":4,"character":2},"end":{"line":4,"character":3}}}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}
2023-03-22T11:22:08.987 helix_lsp::transport [INFO] <- {"params":{"textDocument":{"version":0,"uri":"file:///data/repos/lean/t.lean"},"processing":[{"range":{"start":{"line":4,"character":4},"end":{"line":6,"character":0}},"kind":1}]},"method":"$/lean/fileProgress","jsonrpc":"2.0"}
2023-03-22T11:22:08.987 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "textDocument/publishDiagnostics", params: Map({"diagnostics": Array [Object {"fullRange": Object {"end": Object {"character": Number(3), "line": Number(4)}, "start": Object {"character": Number(2), "line": Number(4)}}, "message": String("type mismatch\n  p\nhas type\n  Prop : Type\nbut is expected to have type\n  q ∧ p : Prop"), "range": Object {"end": Object {"character": Number(3), "line": Number(4)}, "start": Object {"character": Number(2), "line": Number(4)}}, "severity": Number(1), "source": String("Lean 4")}], "uri": String("file:///data/repos/lean/t.lean"), "version": Number(0)}) })))
2023-03-22T11:22:08.987 helix_lsp::transport [INFO] <- {"params":{"version":0,"uri":"file:///data/repos/lean/t.lean","diagnostics":[{"source":"Lean 4","severity":1,"range":{"start":{"line":4,"character":2},"end":{"line":4,"character":3}},"message":"type mismatch\n  p\nhas type\n  Prop : Type\nbut is expected to have type\n  q ∧ p : Prop","fullRange":{"start":{"line":4,"character":2},"end":{"line":4,"character":3}}},{"source":"Lean 4","severity":1,"range":{"start":{"line":4,"character":4},"end":{"line":4,"character":4}},"message":"expected token","fullRange":{"start":{"line":4,"character":4},"end":{"line":4,"character":4}}}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}
2023-03-22T11:22:08.987 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "$/lean/fileProgress", params: Map({"processing": Array [Object {"kind": Number(1), "range": Object {"end": Object {"character": Number(0), "line": Number(6)}, "start": Object {"character": Number(4), "line": Number(4)}}}], "textDocument": Object {"uri": String("file:///data/repos/lean/t.lean"), "version": Number(0)}}) })))
2023-03-22T11:22:08.987 helix_term::application [ERROR] received malformed notification from Language Server: Unhandled
2023-03-22T11:22:08.987 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "textDocument/publishDiagnostics", params: Map({"diagnostics": Array [Object {"fullRange": Object {"end": Object {"character": Number(3), "line": Number(4)}, "start": Object {"character": Number(2), "line": Number(4)}}, "message": String("type mismatch\n  p\nhas type\n  Prop : Type\nbut is expected to have type\n  q ∧ p : Prop"), "range": Object {"end": Object {"character": Number(3), "line": Number(4)}, "start": Object {"character": Number(2), "line": Number(4)}}, "severity": Number(1), "source": String("Lean 4")}, Object {"fullRange": Object {"end": Object {"character": Number(4), "line": Number(4)}, "start": Object {"character": Number(4), "line": Number(4)}}, "message": String("expected token"), "range": Object {"end": Object {"character": Number(4), "line": Number(4)}, "start": Object {"character": Number(4), "line": Number(4)}}, "severity": Number(1), "source": String("Lean 4")}], "uri": String("file:///data/repos/lean/t.lean"), "version": Number(0)}) })))
2023-03-22T11:22:08.988 helix_lsp::transport [INFO] <- {"params":{"version":0,"uri":"file:///data/repos/lean/t.lean","diagnostics":[{"source":"Lean 4","severity":1,"range":{"start":{"line":4,"character":2},"end":{"line":4,"character":3}},"message":"type mismatch\n  p\nhas type\n  Prop : Type\nbut is expected to have type\n  q ∧ p : Prop","fullRange":{"start":{"line":4,"character":2},"end":{"line":4,"character":3}}},{"source":"Lean 4","severity":1,"range":{"start":{"line":4,"character":4},"end":{"line":4,"character":4}},"message":"expected token","fullRange":{"start":{"line":4,"character":4},"end":{"line":4,"character":4}}}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}
2023-03-22T11:22:08.988 helix_lsp::transport [INFO] <- {"params":{"textDocument":{"version":0,"uri":"file:///data/repos/lean/t.lean"},"processing":[]},"method":"$/lean/fileProgress","jsonrpc":"2.0"}
2023-03-22T11:22:08.988 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "textDocument/publishDiagnostics", params: Map({"diagnostics": Array [Object {"fullRange": Object {"end": Object {"character": Number(3), "line": Number(4)}, "start": Object {"character": Number(2), "line": Number(4)}}, "message": String("type mismatch\n  p\nhas type\n  Prop : Type\nbut is expected to have type\n  q ∧ p : Prop"), "range": Object {"end": Object {"character": Number(3), "line": Number(4)}, "start": Object {"character": Number(2), "line": Number(4)}}, "severity": Number(1), "source": String("Lean 4")}, Object {"fullRange": Object {"end": Object {"character": Number(4), "line": Number(4)}, "start": Object {"character": Number(4), "line": Number(4)}}, "message": String("expected token"), "range": Object {"end": Object {"character": Number(4), "line": Number(4)}, "start": Object {"character": Number(4), "line": Number(4)}}, "severity": Number(1), "source": String("Lean 4")}], "uri": String("file:///data/repos/lean/t.lean"), "version": Number(0)}) })))
2023-03-22T11:22:08.988 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "$/lean/fileProgress", params: Map({"processing": Array [], "textDocument": Object {"uri": String("file:///data/repos/lean/t.lean"), "version": Number(0)}}) })))
2023-03-22T11:22:08.988 helix_term::application [ERROR] received malformed notification from Language Server: Unhandled
2023-03-22T11:22:09.458 helix_view::document [DEBUG] id 1 modified - last saved: 0, current: 0
2023-03-22T11:22:09.619 helix_view::document [DEBUG] id 1 modified - last saved: 0, current: 0
2023-03-22T11:22:09.783 helix_view::document [DEBUG] id 1 modified - last saved: 0, current: 0
2023-03-22T11:22:09.955 helix_view::document [DEBUG] id 1 modified - last saved: 0, current: 0
2023-03-22T11:22:10.357 helix_term::application [DEBUG] received editor event: IdleTimer
2023-03-22T11:22:10.906 helix_view::document [DEBUG] id 1 modified - last saved: 0, current: 0
2023-03-22T11:22:11.082 helix_lsp::transport [INFO] -> {"jsonrpc":"2.0","method":"textDocument/didChange","params":{"contentChanges":[{"range":{"end":{"character":0,"line":5},"start":{"character":0,"line":4}},"text":""}],"textDocument":{"uri":"file:///data/repos/lean/t.lean","version":1}}}
2023-03-22T11:22:11.082 helix_view::document [DEBUG] id 1 modified - last saved: 0, current: 1
2023-03-22T11:22:11.272 helix_view::document [DEBUG] id 1 modified - last saved: 0, current: 1
2023-03-22T11:22:11.286 helix_lsp::transport [INFO] <- {"params":{"textDocument":{"version":1,"uri":"file:///data/repos/lean/t.lean"},"processing":[{"range":{"start":{"line":0,"character":0},"end":{"line":5,"character":0}},"kind":1}]},"method":"$/lean/fileProgress","jsonrpc":"2.0"}
2023-03-22T11:22:11.287 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "$/lean/fileProgress", params: Map({"processing": Array [Object {"kind": Number(1), "range": Object {"end": Object {"character": Number(0), "line": Number(5)}, "start": Object {"character": Number(0), "line": Number(0)}}}], "textDocument": Object {"uri": String("file:///data/repos/lean/t.lean"), "version": Number(1)}}) })))
2023-03-22T11:22:11.287 helix_term::application [ERROR] received malformed notification from Language Server: Unhandled
2023-03-22T11:22:11.288 helix_view::document [DEBUG] id 1 modified - last saved: 0, current: 1
2023-03-22T11:22:11.291 helix_lsp::transport [INFO] <- {"params":{"version":1,"uri":"file:///data/repos/lean/t.lean","diagnostics":[]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}
2023-03-22T11:22:11.291 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "textDocument/publishDiagnostics", params: Map({"diagnostics": Array [], "uri": String("file:///data/repos/lean/t.lean"), "version": Number(1)}) })))
2023-03-22T11:22:11.291 helix_lsp::transport [INFO] <- {"params":{"textDocument":{"version":1,"uri":"file:///data/repos/lean/t.lean"},"processing":[{"range":{"start":{"line":5,"character":0},"end":{"line":5,"character":0}},"kind":1}]},"method":"$/lean/fileProgress","jsonrpc":"2.0"}
2023-03-22T11:22:11.291 helix_lsp::transport [INFO] <- {"params":{"version":1,"uri":"file:///data/repos/lean/t.lean","diagnostics":[]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}
2023-03-22T11:22:11.292 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "$/lean/fileProgress", params: Map({"processing": Array [Object {"kind": Number(1), "range": Object {"end": Object {"character": Number(0), "line": Number(5)}, "start": Object {"character": Number(0), "line": Number(5)}}}], "textDocument": Object {"uri": String("file:///data/repos/lean/t.lean"), "version": Number(1)}}) })))
2023-03-22T11:22:11.292 helix_term::application [ERROR] received malformed notification from Language Server: Unhandled
2023-03-22T11:22:11.292 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "textDocument/publishDiagnostics", params: Map({"diagnostics": Array [], "uri": String("file:///data/repos/lean/t.lean"), "version": Number(1)}) })))
2023-03-22T11:22:11.292 helix_lsp::transport [INFO] <- {"params":{"version":1,"uri":"file:///data/repos/lean/t.lean","diagnostics":[]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}
2023-03-22T11:22:11.292 helix_lsp::transport [INFO] <- {"params":{"textDocument":{"version":1,"uri":"file:///data/repos/lean/t.lean"},"processing":[]},"method":"$/lean/fileProgress","jsonrpc":"2.0"}
2023-03-22T11:22:11.292 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "textDocument/publishDiagnostics", params: Map({"diagnostics": Array [], "uri": String("file:///data/repos/lean/t.lean"), "version": Number(1)}) })))
2023-03-22T11:22:11.292 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "$/lean/fileProgress", params: Map({"processing": Array [], "textDocument": Object {"uri": String("file:///data/repos/lean/t.lean"), "version": Number(1)}}) })))
2023-03-22T11:22:11.292 helix_term::application [ERROR] received malformed notification from Language Server: Unhandled
2023-03-22T11:22:11.460 helix_lsp::transport [INFO] -> {"jsonrpc":"2.0","method":"textDocument/didChange","params":{"contentChanges":[{"range":{"end":{"character":30,"line":3},"start":{"character":30,"line":3}},"text":"\n  "}],"textDocument":{"uri":"file:///data/repos/lean/t.lean","version":2}}}
2023-03-22T11:22:11.460 helix_view::document [DEBUG] id 1 modified - last saved: 0, current: 1
2023-03-22T11:22:11.664 helix_lsp::transport [INFO] <- {"params":{"textDocument":{"version":2,"uri":"file:///data/repos/lean/t.lean"},"processing":[{"range":{"start":{"line":0,"character":0},"end":{"line":6,"character":0}},"kind":1}]},"method":"$/lean/fileProgress","jsonrpc":"2.0"}
2023-03-22T11:22:11.664 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "$/lean/fileProgress", params: Map({"processing": Array [Object {"kind": Number(1), "range": Object {"end": Object {"character": Number(0), "line": Number(6)}, "start": Object {"character": Number(0), "line": Number(0)}}}], "textDocument": Object {"uri": String("file:///data/repos/lean/t.lean"), "version": Number(2)}}) })))
2023-03-22T11:22:11.664 helix_term::application [ERROR] received malformed notification from Language Server: Unhandled
2023-03-22T11:22:11.665 helix_view::document [DEBUG] id 1 modified - last saved: 0, current: 1
2023-03-22T11:22:11.668 helix_lsp::transport [INFO] <- {"params":{"version":2,"uri":"file:///data/repos/lean/t.lean","diagnostics":[]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}
2023-03-22T11:22:11.669 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "textDocument/publishDiagnostics", params: Map({"diagnostics": Array [], "uri": String("file:///data/repos/lean/t.lean"), "version": Number(2)}) })))
2023-03-22T11:22:11.669 helix_lsp::transport [INFO] <- {"params":{"textDocument":{"version":2,"uri":"file:///data/repos/lean/t.lean"},"processing":[{"range":{"start":{"line":6,"character":0},"end":{"line":6,"character":0}},"kind":1}]},"method":"$/lean/fileProgress","jsonrpc":"2.0"}
2023-03-22T11:22:11.669 helix_lsp::transport [INFO] <- {"params":{"version":2,"uri":"file:///data/repos/lean/t.lean","diagnostics":[]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}
2023-03-22T11:22:11.669 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "$/lean/fileProgress", params: Map({"processing": Array [Object {"kind": Number(1), "range": Object {"end": Object {"character": Number(0), "line": Number(6)}, "start": Object {"character": Number(0), "line": Number(6)}}}], "textDocument": Object {"uri": String("file:///data/repos/lean/t.lean"), "version": Number(2)}}) })))
2023-03-22T11:22:11.669 helix_term::application [ERROR] received malformed notification from Language Server: Unhandled
2023-03-22T11:22:11.669 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "textDocument/publishDiagnostics", params: Map({"diagnostics": Array [], "uri": String("file:///data/repos/lean/t.lean"), "version": Number(2)}) })))
2023-03-22T11:22:11.669 helix_lsp::transport [INFO] <- {"params":{"version":2,"uri":"file:///data/repos/lean/t.lean","diagnostics":[]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}
2023-03-22T11:22:11.669 helix_lsp::transport [INFO] <- {"params":{"textDocument":{"version":2,"uri":"file:///data/repos/lean/t.lean"},"processing":[]},"method":"$/lean/fileProgress","jsonrpc":"2.0"}
2023-03-22T11:22:11.669 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "textDocument/publishDiagnostics", params: Map({"diagnostics": Array [], "uri": String("file:///data/repos/lean/t.lean"), "version": Number(2)}) })))
2023-03-22T11:22:11.669 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "$/lean/fileProgress", params: Map({"processing": Array [], "textDocument": Object {"uri": String("file:///data/repos/lean/t.lean"), "version": Number(2)}}) })))
2023-03-22T11:22:11.669 helix_term::application [ERROR] received malformed notification from Language Server: Unhandled
2023-03-22T11:22:11.743 helix_core::auto_pairs [TRACE] autopairs hook selection: Selection {
    ranges: [
        Range {
            anchor: 140,
            head: 141,
            old_visual_position: None,
        },
    ],
    primary_index: 0,
}
2023-03-22T11:22:11.744 helix_lsp::transport [INFO] -> {"jsonrpc":"2.0","method":"textDocument/didChange","params":{"contentChanges":[{"range":{"end":{"character":2,"line":4},"start":{"character":2,"line":4}},"text":"p"}],"textDocument":{"uri":"file:///data/repos/lean/t.lean","version":3}}}
2023-03-22T11:22:11.745 helix_view::document [DEBUG] id 1 modified - last saved: 0, current: 1
2023-03-22T11:22:11.948 helix_lsp::transport [INFO] <- {"params":{"textDocument":{"version":3,"uri":"file:///data/repos/lean/t.lean"},"processing":[{"range":{"start":{"line":0,"character":0},"end":{"line":6,"character":0}},"kind":1}]},"method":"$/lean/fileProgress","jsonrpc":"2.0"}
2023-03-22T11:22:11.949 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "$/lean/fileProgress", params: Map({"processing": Array [Object {"kind": Number(1), "range": Object {"end": Object {"character": Number(0), "line": Number(6)}, "start": Object {"character": Number(0), "line": Number(0)}}}], "textDocument": Object {"uri": String("file:///data/repos/lean/t.lean"), "version": Number(3)}}) })))
2023-03-22T11:22:11.949 helix_term::application [ERROR] received malformed notification from Language Server: Unhandled
2023-03-22T11:22:11.950 helix_view::document [DEBUG] id 1 modified - last saved: 0, current: 1
2023-03-22T11:22:11.968 helix_lsp::transport [INFO] <- {"params":{"version":3,"uri":"file:///data/repos/lean/t.lean","diagnostics":[{"source":"Lean 4","severity":1,"range":{"start":{"line":4,"character":2},"end":{"line":4,"character":3}},"message":"type mismatch\n  p\nhas type\n  Prop : Type\nbut is expected to have type\n  q ∧ p : Prop","fullRange":{"start":{"line":4,"character":2},"end":{"line":4,"character":3}}}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}
2023-03-22T11:22:11.968 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "textDocument/publishDiagnostics", params: Map({"diagnostics": Array [Object {"fullRange": Object {"end": Object {"character": Number(3), "line": Number(4)}, "start": Object {"character": Number(2), "line": Number(4)}}, "message": String("type mismatch\n  p\nhas type\n  Prop : Type\nbut is expected to have type\n  q ∧ p : Prop"), "range": Object {"end": Object {"character": Number(3), "line": Number(4)}, "start": Object {"character": Number(2), "line": Number(4)}}, "severity": Number(1), "source": String("Lean 4")}], "uri": String("file:///data/repos/lean/t.lean"), "version": Number(3)}) })))
2023-03-22T11:22:11.969 helix_lsp::transport [INFO] <- {"params":{"textDocument":{"version":3,"uri":"file:///data/repos/lean/t.lean"},"processing":[{"range":{"start":{"line":5,"character":2},"end":{"line":6,"character":0}},"kind":1}]},"method":"$/lean/fileProgress","jsonrpc":"2.0"}
2023-03-22T11:22:11.969 helix_view::document [DEBUG] id 1 modified - last saved: 0, current: 1
2023-03-22T11:22:11.969 helix_lsp::transport [INFO] <- {"params":{"version":3,"uri":"file:///data/repos/lean/t.lean","diagnostics":[{"source":"Lean 4","severity":1,"range":{"start":{"line":4,"character":2},"end":{"line":4,"character":3}},"message":"type mismatch\n  p\nhas type\n  Prop : Type\nbut is expected to have type\n  q ∧ p : Prop","fullRange":{"start":{"line":4,"character":2},"end":{"line":4,"character":3}}},{"source":"Lean 4","severity":1,"range":{"start":{"line":5,"character":2},"end":{"line":5,"character":2}},"message":"expected command","fullRange":{"start":{"line":5,"character":2},"end":{"line":5,"character":2}}}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}
2023-03-22T11:22:11.970 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "$/lean/fileProgress", params: Map({"processing": Array [Object {"kind": Number(1), "range": Object {"end": Object {"character": Number(0), "line": Number(6)}, "start": Object {"character": Number(2), "line": Number(5)}}}], "textDocument": Object {"uri": String("file:///data/repos/lean/t.lean"), "version": Number(3)}}) })))
2023-03-22T11:22:11.970 helix_term::application [ERROR] received malformed notification from Language Server: Unhandled
2023-03-22T11:22:11.970 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "textDocument/publishDiagnostics", params: Map({"diagnostics": Array [Object {"fullRange": Object {"end": Object {"character": Number(3), "line": Number(4)}, "start": Object {"character": Number(2), "line": Number(4)}}, "message": String("type mismatch\n  p\nhas type\n  Prop : Type\nbut is expected to have type\n  q ∧ p : Prop"), "range": Object {"end": Object {"character": Number(3), "line": Number(4)}, "start": Object {"character": Number(2), "line": Number(4)}}, "severity": Number(1), "source": String("Lean 4")}, Object {"fullRange": Object {"end": Object {"character": Number(2), "line": Number(5)}, "start": Object {"character": Number(2), "line": Number(5)}}, "message": String("expected command"), "range": Object {"end": Object {"character": Number(2), "line": Number(5)}, "start": Object {"character": Number(2), "line": Number(5)}}, "severity": Number(1), "source": String("Lean 4")}], "uri": String("file:///data/repos/lean/t.lean"), "version": Number(3)}) })))
2023-03-22T11:22:11.971 helix_lsp::transport [INFO] <- {"params":{"version":3,"uri":"file:///data/repos/lean/t.lean","diagnostics":[{"source":"Lean 4","severity":1,"range":{"start":{"line":4,"character":2},"end":{"line":4,"character":3}},"message":"type mismatch\n  p\nhas type\n  Prop : Type\nbut is expected to have type\n  q ∧ p : Prop","fullRange":{"start":{"line":4,"character":2},"end":{"line":4,"character":3}}},{"source":"Lean 4","severity":1,"range":{"start":{"line":5,"character":2},"end":{"line":5,"character":2}},"message":"expected command","fullRange":{"start":{"line":5,"character":2},"end":{"line":5,"character":2}}}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}
2023-03-22T11:22:11.971 helix_lsp::transport [INFO] <- {"params":{"textDocument":{"version":3,"uri":"file:///data/repos/lean/t.lean"},"processing":[]},"method":"$/lean/fileProgress","jsonrpc":"2.0"}
2023-03-22T11:22:11.971 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "textDocument/publishDiagnostics", params: Map({"diagnostics": Array [Object {"fullRange": Object {"end": Object {"character": Number(3), "line": Number(4)}, "start": Object {"character": Number(2), "line": Number(4)}}, "message": String("type mismatch\n  p\nhas type\n  Prop : Type\nbut is expected to have type\n  q ∧ p : Prop"), "range": Object {"end": Object {"character": Number(3), "line": Number(4)}, "start": Object {"character": Number(2), "line": Number(4)}}, "severity": Number(1), "source": String("Lean 4")}, Object {"fullRange": Object {"end": Object {"character": Number(2), "line": Number(5)}, "start": Object {"character": Number(2), "line": Number(5)}}, "message": String("expected command"), "range": Object {"end": Object {"character": Number(2), "line": Number(5)}, "start": Object {"character": Number(2), "line": Number(5)}}, "severity": Number(1), "source": String("Lean 4")}], "uri": String("file:///data/repos/lean/t.lean"), "version": Number(3)}) })))
2023-03-22T11:22:11.971 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "$/lean/fileProgress", params: Map({"processing": Array [], "textDocument": Object {"uri": String("file:///data/repos/lean/t.lean"), "version": Number(3)}}) })))
2023-03-22T11:22:11.971 helix_term::application [ERROR] received malformed notification from Language Server: Unhandled
2023-03-22T11:22:12.145 helix_term::application [DEBUG] received editor event: IdleTimer
2023-03-22T11:22:12.146 helix_view::document [DEBUG] id 1 modified - last saved: 0, current: 1
2023-03-22T11:22:12.279 helix_core::auto_pairs [TRACE] autopairs hook selection: Selection {
    ranges: [
        Range {
            anchor: 141,
            head: 142,
            old_visual_position: None,
        },
    ],
    primary_index: 0,
}
2023-03-22T11:22:12.280 helix_lsp::transport [INFO] -> {"jsonrpc":"2.0","method":"textDocument/didChange","params":{"contentChanges":[{"range":{"end":{"character":3,"line":4},"start":{"character":3,"line":4}},"text":" "}],"textDocument":{"uri":"file:///data/repos/lean/t.lean","version":4}}}
2023-03-22T11:22:12.281 helix_view::document [DEBUG] id 1 modified - last saved: 0, current: 1
2023-03-22T11:22:12.481 helix_lsp::transport [INFO] <- {"params":{"textDocument":{"version":4,"uri":"file:///data/repos/lean/t.lean"},"processing":[{"range":{"start":{"line":0,"character":0},"end":{"line":6,"character":0}},"kind":1}]},"method":"$/lean/fileProgress","jsonrpc":"2.0"}
2023-03-22T11:22:12.482 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "$/lean/fileProgress", params: Map({"processing": Array [Object {"kind": Number(1), "range": Object {"end": Object {"character": Number(0), "line": Number(6)}, "start": Object {"character": Number(0), "line": Number(0)}}}], "textDocument": Object {"uri": String("file:///data/repos/lean/t.lean"), "version": Number(4)}}) })))
2023-03-22T11:22:12.482 helix_term::application [ERROR] received malformed notification from Language Server: Unhandled
2023-03-22T11:22:12.482 helix_view::document [DEBUG] id 1 modified - last saved: 0, current: 1
2023-03-22T11:22:12.486 helix_lsp::transport [INFO] <- {"params":{"version":4,"uri":"file:///data/repos/lean/t.lean","diagnostics":[{"source":"Lean 4","severity":1,"range":{"start":{"line":4,"character":2},"end":{"line":4,"character":3}},"message":"type mismatch\n  p\nhas type\n  Prop : Type\nbut is expected to have type\n  q ∧ p : Prop","fullRange":{"start":{"line":4,"character":2},"end":{"line":4,"character":3}}}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}
2023-03-22T11:22:12.486 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "textDocument/publishDiagnostics", params: Map({"diagnostics": Array [Object {"fullRange": Object {"end": Object {"character": Number(3), "line": Number(4)}, "start": Object {"character": Number(2), "line": Number(4)}}, "message": String("type mismatch\n  p\nhas type\n  Prop : Type\nbut is expected to have type\n  q ∧ p : Prop"), "range": Object {"end": Object {"character": Number(3), "line": Number(4)}, "start": Object {"character": Number(2), "line": Number(4)}}, "severity": Number(1), "source": String("Lean 4")}], "uri": String("file:///data/repos/lean/t.lean"), "version": Number(4)}) })))
2023-03-22T11:22:12.486 helix_lsp::transport [INFO] <- {"params":{"textDocument":{"version":4,"uri":"file:///data/repos/lean/t.lean"},"processing":[{"range":{"start":{"line":5,"character":2},"end":{"line":6,"character":0}},"kind":1}]},"method":"$/lean/fileProgress","jsonrpc":"2.0"}
2023-03-22T11:22:12.487 helix_lsp::transport [INFO] <- {"params":{"version":4,"uri":"file:///data/repos/lean/t.lean","diagnostics":[{"source":"Lean 4","severity":1,"range":{"start":{"line":4,"character":2},"end":{"line":4,"character":3}},"message":"type mismatch\n  p\nhas type\n  Prop : Type\nbut is expected to have type\n  q ∧ p : Prop","fullRange":{"start":{"line":4,"character":2},"end":{"line":4,"character":3}}},{"source":"Lean 4","severity":1,"range":{"start":{"line":5,"character":2},"end":{"line":5,"character":2}},"message":"expected command","fullRange":{"start":{"line":5,"character":2},"end":{"line":5,"character":2}}}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}
2023-03-22T11:22:12.487 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "$/lean/fileProgress", params: Map({"processing": Array [Object {"kind": Number(1), "range": Object {"end": Object {"character": Number(0), "line": Number(6)}, "start": Object {"character": Number(2), "line": Number(5)}}}], "textDocument": Object {"uri": String("file:///data/repos/lean/t.lean"), "version": Number(4)}}) })))
2023-03-22T11:22:12.487 helix_term::application [ERROR] received malformed notification from Language Server: Unhandled
2023-03-22T11:22:12.487 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "textDocument/publishDiagnostics", params: Map({"diagnostics": Array [Object {"fullRange": Object {"end": Object {"character": Number(3), "line": Number(4)}, "start": Object {"character": Number(2), "line": Number(4)}}, "message": String("type mismatch\n  p\nhas type\n  Prop : Type\nbut is expected to have type\n  q ∧ p : Prop"), "range": Object {"end": Object {"character": Number(3), "line": Number(4)}, "start": Object {"character": Number(2), "line": Number(4)}}, "severity": Number(1), "source": String("Lean 4")}, Object {"fullRange": Object {"end": Object {"character": Number(2), "line": Number(5)}, "start": Object {"character": Number(2), "line": Number(5)}}, "message": String("expected command"), "range": Object {"end": Object {"character": Number(2), "line": Number(5)}, "start": Object {"character": Number(2), "line": Number(5)}}, "severity": Number(1), "source": String("Lean 4")}], "uri": String("file:///data/repos/lean/t.lean"), "version": Number(4)}) })))
2023-03-22T11:22:12.487 helix_lsp::transport [INFO] <- {"params":{"version":4,"uri":"file:///data/repos/lean/t.lean","diagnostics":[{"source":"Lean 4","severity":1,"range":{"start":{"line":4,"character":2},"end":{"line":4,"character":3}},"message":"type mismatch\n  p\nhas type\n  Prop : Type\nbut is expected to have type\n  q ∧ p : Prop","fullRange":{"start":{"line":4,"character":2},"end":{"line":4,"character":3}}},{"source":"Lean 4","severity":1,"range":{"start":{"line":5,"character":2},"end":{"line":5,"character":2}},"message":"expected command","fullRange":{"start":{"line":5,"character":2},"end":{"line":5,"character":2}}}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}
2023-03-22T11:22:12.487 helix_lsp::transport [INFO] <- {"params":{"textDocument":{"version":4,"uri":"file:///data/repos/lean/t.lean"},"processing":[]},"method":"$/lean/fileProgress","jsonrpc":"2.0"}
2023-03-22T11:22:12.487 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "textDocument/publishDiagnostics", params: Map({"diagnostics": Array [Object {"fullRange": Object {"end": Object {"character": Number(3), "line": Number(4)}, "start": Object {"character": Number(2), "line": Number(4)}}, "message": String("type mismatch\n  p\nhas type\n  Prop : Type\nbut is expected to have type\n  q ∧ p : Prop"), "range": Object {"end": Object {"character": Number(3), "line": Number(4)}, "start": Object {"character": Number(2), "line": Number(4)}}, "severity": Number(1), "source": String("Lean 4")}, Object {"fullRange": Object {"end": Object {"character": Number(2), "line": Number(5)}, "start": Object {"character": Number(2), "line": Number(5)}}, "message": String("expected command"), "range": Object {"end": Object {"character": Number(2), "line": Number(5)}, "start": Object {"character": Number(2), "line": Number(5)}}, "severity": Number(1), "source": String("Lean 4")}], "uri": String("file:///data/repos/lean/t.lean"), "version": Number(4)}) })))
2023-03-22T11:22:12.487 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "$/lean/fileProgress", params: Map({"processing": Array [], "textDocument": Object {"uri": String("file:///data/repos/lean/t.lean"), "version": Number(4)}}) })))
2023-03-22T11:22:12.487 helix_term::application [ERROR] received malformed notification from Language Server: Unhandled
2023-03-22T11:22:12.534 helix_core::auto_pairs [TRACE] autopairs hook selection: Selection {
    ranges: [
        Range {
            anchor: 142,
            head: 143,
            old_visual_position: None,
        },
    ],
    primary_index: 0,
}
2023-03-22T11:22:12.534 helix_lsp::transport [INFO] -> {"jsonrpc":"2.0","method":"textDocument/didChange","params":{"contentChanges":[{"range":{"end":{"character":4,"line":4},"start":{"character":4,"line":4}},"text":"\\"}],"textDocument":{"uri":"file:///data/repos/lean/t.lean","version":5}}}
2023-03-22T11:22:12.535 helix_view::document [DEBUG] id 1 modified - last saved: 0, current: 1
2023-03-22T11:22:12.738 helix_lsp::transport [INFO] <- {"params":{"textDocument":{"version":5,"uri":"file:///data/repos/lean/t.lean"},"processing":[{"range":{"start":{"line":0,"character":0},"end":{"line":6,"character":0}},"kind":1}]},"method":"$/lean/fileProgress","jsonrpc":"2.0"}
2023-03-22T11:22:12.738 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "$/lean/fileProgress", params: Map({"processing": Array [Object {"kind": Number(1), "range": Object {"end": Object {"character": Number(0), "line": Number(6)}, "start": Object {"character": Number(0), "line": Number(0)}}}], "textDocument": Object {"uri": String("file:///data/repos/lean/t.lean"), "version": Number(5)}}) })))
2023-03-22T11:22:12.738 helix_term::application [ERROR] received malformed notification from Language Server: Unhandled
2023-03-22T11:22:12.739 helix_view::document [DEBUG] id 1 modified - last saved: 0, current: 1
2023-03-22T11:22:12.757 helix_lsp::transport [INFO] <- {"params":{"version":5,"uri":"file:///data/repos/lean/t.lean","diagnostics":[{"source":"Lean 4","severity":1,"range":{"start":{"line":4,"character":2},"end":{"line":4,"character":3}},"message":"type mismatch\n  p\nhas type\n  Prop : Type\nbut is expected to have type\n  q ∧ p : Prop","fullRange":{"start":{"line":4,"character":2},"end":{"line":4,"character":3}}}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}
2023-03-22T11:22:12.758 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "textDocument/publishDiagnostics", params: Map({"diagnostics": Array [Object {"fullRange": Object {"end": Object {"character": Number(3), "line": Number(4)}, "start": Object {"character": Number(2), "line": Number(4)}}, "message": String("type mismatch\n  p\nhas type\n  Prop : Type\nbut is expected to have type\n  q ∧ p : Prop"), "range": Object {"end": Object {"character": Number(3), "line": Number(4)}, "start": Object {"character": Number(2), "line": Number(4)}}, "severity": Number(1), "source": String("Lean 4")}], "uri": String("file:///data/repos/lean/t.lean"), "version": Number(5)}) })))
2023-03-22T11:22:12.758 helix_lsp::transport [INFO] <- {"params":{"textDocument":{"version":5,"uri":"file:///data/repos/lean/t.lean"},"processing":[{"range":{"start":{"line":4,"character":4},"end":{"line":6,"character":0}},"kind":1}]},"method":"$/lean/fileProgress","jsonrpc":"2.0"}
2023-03-22T11:22:12.759 helix_view::document [DEBUG] id 1 modified - last saved: 0, current: 1
2023-03-22T11:22:12.759 helix_lsp::transport [INFO] <- {"params":{"version":5,"uri":"file:///data/repos/lean/t.lean","diagnostics":[{"source":"Lean 4","severity":1,"range":{"start":{"line":4,"character":2},"end":{"line":4,"character":3}},"message":"type mismatch\n  p\nhas type\n  Prop : Type\nbut is expected to have type\n  q ∧ p : Prop","fullRange":{"start":{"line":4,"character":2},"end":{"line":4,"character":3}}},{"source":"Lean 4","severity":1,"range":{"start":{"line":4,"character":4},"end":{"line":4,"character":4}},"message":"expected token","fullRange":{"start":{"line":4,"character":4},"end":{"line":4,"character":4}}}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}
2023-03-22T11:22:12.759 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "$/lean/fileProgress", params: Map({"processing": Array [Object {"kind": Number(1), "range": Object {"end": Object {"character": Number(0), "line": Number(6)}, "start": Object {"character": Number(4), "line": Number(4)}}}], "textDocument": Object {"uri": String("file:///data/repos/lean/t.lean"), "version": Number(5)}}) })))
2023-03-22T11:22:12.759 helix_term::application [ERROR] received malformed notification from Language Server: Unhandled
2023-03-22T11:22:12.759 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "textDocument/publishDiagnostics", params: Map({"diagnostics": Array [Object {"fullRange": Object {"end": Object {"character": Number(3), "line": Number(4)}, "start": Object {"character": Number(2), "line": Number(4)}}, "message": String("type mismatch\n  p\nhas type\n  Prop : Type\nbut is expected to have type\n  q ∧ p : Prop"), "range": Object {"end": Object {"character": Number(3), "line": Number(4)}, "start": Object {"character": Number(2), "line": Number(4)}}, "severity": Number(1), "source": String("Lean 4")}, Object {"fullRange": Object {"end": Object {"character": Number(4), "line": Number(4)}, "start": Object {"character": Number(4), "line": Number(4)}}, "message": String("expected token"), "range": Object {"end": Object {"character": Number(4), "line": Number(4)}, "start": Object {"character": Number(4), "line": Number(4)}}, "severity": Number(1), "source": String("Lean 4")}], "uri": String("file:///data/repos/lean/t.lean"), "version": Number(5)}) })))
2023-03-22T11:22:12.760 helix_lsp::transport [INFO] <- {"params":{"version":5,"uri":"file:///data/repos/lean/t.lean","diagnostics":[{"source":"Lean 4","severity":1,"range":{"start":{"line":4,"character":2},"end":{"line":4,"character":3}},"message":"type mismatch\n  p\nhas type\n  Prop : Type\nbut is expected to have type\n  q ∧ p : Prop","fullRange":{"start":{"line":4,"character":2},"end":{"line":4,"character":3}}},{"source":"Lean 4","severity":1,"range":{"start":{"line":4,"character":4},"end":{"line":4,"character":4}},"message":"expected token","fullRange":{"start":{"line":4,"character":4},"end":{"line":4,"character":4}}}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}
2023-03-22T11:22:12.760 helix_lsp::transport [INFO] <- {"params":{"textDocument":{"version":5,"uri":"file:///data/repos/lean/t.lean"},"processing":[]},"method":"$/lean/fileProgress","jsonrpc":"2.0"}
2023-03-22T11:22:12.760 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "textDocument/publishDiagnostics", params: Map({"diagnostics": Array [Object {"fullRange": Object {"end": Object {"character": Number(3), "line": Number(4)}, "start": Object {"character": Number(2), "line": Number(4)}}, "message": String("type mismatch\n  p\nhas type\n  Prop : Type\nbut is expected to have type\n  q ∧ p : Prop"), "range": Object {"end": Object {"character": Number(3), "line": Number(4)}, "start": Object {"character": Number(2), "line": Number(4)}}, "severity": Number(1), "source": String("Lean 4")}, Object {"fullRange": Object {"end": Object {"character": Number(4), "line": Number(4)}, "start": Object {"character": Number(4), "line": Number(4)}}, "message": String("expected token"), "range": Object {"end": Object {"character": Number(4), "line": Number(4)}, "start": Object {"character": Number(4), "line": Number(4)}}, "severity": Number(1), "source": String("Lean 4")}], "uri": String("file:///data/repos/lean/t.lean"), "version": Number(5)}) })))
2023-03-22T11:22:12.760 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "$/lean/fileProgress", params: Map({"processing": Array [], "textDocument": Object {"uri": String("file:///data/repos/lean/t.lean"), "version": Number(5)}}) })))
2023-03-22T11:22:12.760 helix_term::application [ERROR] received malformed notification from Language Server: Unhandled
2023-03-22T11:22:12.827 helix_core::auto_pairs [TRACE] autopairs hook selection: Selection {
    ranges: [
        Range {
            anchor: 143,
            head: 144,
            old_visual_position: None,
        },
    ],
    primary_index: 0,
}
2023-03-22T11:22:12.828 helix_lsp::transport [INFO] -> {"jsonrpc":"2.0","method":"textDocument/didChange","params":{"contentChanges":[{"range":{"end":{"character":5,"line":4},"start":{"character":5,"line":4}},"text":"t"}],"textDocument":{"uri":"file:///data/repos/lean/t.lean","version":6}}}
2023-03-22T11:22:12.829 helix_view::document [DEBUG] id 1 modified - last saved: 0, current: 1
2023-03-22T11:22:12.929 helix_core::auto_pairs [TRACE] autopairs hook selection: Selection {
    ranges: [
        Range {
            anchor: 144,
            head: 145,
            old_visual_position: None,
        },
    ],
    primary_index: 0,
}
2023-03-22T11:22:12.931 helix_lsp::transport [INFO] -> {"jsonrpc":"2.0","method":"textDocument/didChange","params":{"contentChanges":[{"range":{"end":{"character":6,"line":4},"start":{"character":6,"line":4}},"text":"o"}],"textDocument":{"uri":"file:///data/repos/lean/t.lean","version":7}}}
2023-03-22T11:22:12.932 helix_view::document [DEBUG] id 1 modified - last saved: 0, current: 1
2023-03-22T11:22:13.086 helix_core::auto_pairs [TRACE] autopairs hook selection: Selection {
    ranges: [
        Range {
            anchor: 145,
            head: 146,
            old_visual_position: None,
        },
    ],
    primary_index: 0,
}
2023-03-22T11:22:13.087 helix_lsp::transport [INFO] -> {"jsonrpc":"2.0","method":"textDocument/didChange","params":{"contentChanges":[{"range":{"end":{"character":7,"line":4},"start":{"character":7,"line":4}},"text":" "}],"textDocument":{"uri":"file:///data/repos/lean/t.lean","version":8}}}
2023-03-22T11:22:13.087 helix_view::document [DEBUG] id 1 modified - last saved: 0, current: 1
2023-03-22T11:22:13.292 helix_lsp::transport [INFO] <- {"params":{"textDocument":{"version":8,"uri":"file:///data/repos/lean/t.lean"},"processing":[{"range":{"start":{"line":4,"character":4},"end":{"line":6,"character":0}},"kind":1}]},"method":"$/lean/fileProgress","jsonrpc":"2.0"}
2023-03-22T11:22:13.293 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "$/lean/fileProgress", params: Map({"processing": Array [Object {"kind": Number(1), "range": Object {"end": Object {"character": Number(0), "line": Number(6)}, "start": Object {"character": Number(4), "line": Number(4)}}}], "textDocument": Object {"uri": String("file:///data/repos/lean/t.lean"), "version": Number(8)}}) })))
2023-03-22T11:22:13.300 helix_term::application [ERROR] received malformed notification from Language Server: Unhandled
2023-03-22T11:22:13.293 helix_lsp::transport [INFO] <- {"params":{"version":8,"uri":"file:///data/repos/lean/t.lean","diagnostics":[{"source":"Lean 4","severity":1,"range":{"start":{"line":4,"character":2},"end":{"line":4,"character":3}},"message":"type mismatch\n  p\nhas type\n  Prop : Type\nbut is expected to have type\n  q ∧ p : Prop","fullRange":{"start":{"line":4,"character":2},"end":{"line":4,"character":3}}},{"source":"Lean 4","severity":1,"range":{"start":{"line":4,"character":4},"end":{"line":4,"character":4}},"message":"expected token","fullRange":{"start":{"line":4,"character":4},"end":{"line":4,"character":4}}}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}
2023-03-22T11:22:13.300 helix_lsp::transport [INFO] <- {"params":{"version":8,"uri":"file:///data/repos/lean/t.lean","diagnostics":[{"source":"Lean 4","severity":1,"range":{"start":{"line":4,"character":2},"end":{"line":4,"character":3}},"message":"type mismatch\n  p\nhas type\n  Prop : Type\nbut is expected to have type\n  q ∧ p : Prop","fullRange":{"start":{"line":4,"character":2},"end":{"line":4,"character":3}}},{"source":"Lean 4","severity":1,"range":{"start":{"line":4,"character":4},"end":{"line":4,"character":4}},"message":"expected token","fullRange":{"start":{"line":4,"character":4},"end":{"line":4,"character":4}}}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}
2023-03-22T11:22:13.300 helix_lsp::transport [INFO] <- {"params":{"textDocument":{"version":8,"uri":"file:///data/repos/lean/t.lean"},"processing":[]},"method":"$/lean/fileProgress","jsonrpc":"2.0"}
2023-03-22T11:22:13.301 helix_view::document [DEBUG] id 1 modified - last saved: 0, current: 1
2023-03-22T11:22:13.301 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "textDocument/publishDiagnostics", params: Map({"diagnostics": Array [Object {"fullRange": Object {"end": Object {"character": Number(3), "line": Number(4)}, "start": Object {"character": Number(2), "line": Number(4)}}, "message": String("type mismatch\n  p\nhas type\n  Prop : Type\nbut is expected to have type\n  q ∧ p : Prop"), "range": Object {"end": Object {"character": Number(3), "line": Number(4)}, "start": Object {"character": Number(2), "line": Number(4)}}, "severity": Number(1), "source": String("Lean 4")}, Object {"fullRange": Object {"end": Object {"character": Number(4), "line": Number(4)}, "start": Object {"character": Number(4), "line": Number(4)}}, "message": String("expected token"), "range": Object {"end": Object {"character": Number(4), "line": Number(4)}, "start": Object {"character": Number(4), "line": Number(4)}}, "severity": Number(1), "source": String("Lean 4")}], "uri": String("file:///data/repos/lean/t.lean"), "version": Number(8)}) })))
2023-03-22T11:22:13.302 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "textDocument/publishDiagnostics", params: Map({"diagnostics": Array [Object {"fullRange": Object {"end": Object {"character": Number(3), "line": Number(4)}, "start": Object {"character": Number(2), "line": Number(4)}}, "message": String("type mismatch\n  p\nhas type\n  Prop : Type\nbut is expected to have type\n  q ∧ p : Prop"), "range": Object {"end": Object {"character": Number(3), "line": Number(4)}, "start": Object {"character": Number(2), "line": Number(4)}}, "severity": Number(1), "source": String("Lean 4")}, Object {"fullRange": Object {"end": Object {"character": Number(4), "line": Number(4)}, "start": Object {"character": Number(4), "line": Number(4)}}, "message": String("expected token"), "range": Object {"end": Object {"character": Number(4), "line": Number(4)}, "start": Object {"character": Number(4), "line": Number(4)}}, "severity": Number(1), "source": String("Lean 4")}], "uri": String("file:///data/repos/lean/t.lean"), "version": Number(8)}) })))
2023-03-22T11:22:13.302 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "$/lean/fileProgress", params: Map({"processing": Array [], "textDocument": Object {"uri": String("file:///data/repos/lean/t.lean"), "version": Number(8)}}) })))
2023-03-22T11:22:13.302 helix_term::application [ERROR] received malformed notification from Language Server: Unhandled
2023-03-22T11:22:13.409 helix_core::auto_pairs [TRACE] autopairs hook selection: Selection {
    ranges: [
        Range {
            anchor: 146,
            head: 147,
            old_visual_position: None,
        },
    ],
    primary_index: 0,
}
2023-03-22T11:22:13.410 helix_lsp::transport [INFO] -> {"jsonrpc":"2.0","method":"textDocument/didChange","params":{"contentChanges":[{"range":{"end":{"character":8,"line":4},"start":{"character":8,"line":4}},"text":"q"}],"textDocument":{"uri":"file:///data/repos/lean/t.lean","version":9}}}
2023-03-22T11:22:13.411 helix_view::document [DEBUG] id 1 modified - last saved: 0, current: 1
2023-03-22T11:22:13.616 helix_lsp::transport [INFO] <- {"params":{"textDocument":{"version":9,"uri":"file:///data/repos/lean/t.lean"},"processing":[{"range":{"start":{"line":4,"character":4},"end":{"line":6,"character":0}},"kind":1}]},"method":"$/lean/fileProgress","jsonrpc":"2.0"}
2023-03-22T11:22:13.616 helix_lsp::transport [INFO] <- {"params":{"version":9,"uri":"file:///data/repos/lean/t.lean","diagnostics":[{"source":"Lean 4","severity":1,"range":{"start":{"line":4,"character":2},"end":{"line":4,"character":3}},"message":"type mismatch\n  p\nhas type\n  Prop : Type\nbut is expected to have type\n  q ∧ p : Prop","fullRange":{"start":{"line":4,"character":2},"end":{"line":4,"character":3}}},{"source":"Lean 4","severity":1,"range":{"start":{"line":4,"character":4},"end":{"line":4,"character":4}},"message":"expected token","fullRange":{"start":{"line":4,"character":4},"end":{"line":4,"character":4}}}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}
2023-03-22T11:22:13.616 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "$/lean/fileProgress", params: Map({"processing": Array [Object {"kind": Number(1), "range": Object {"end": Object {"character": Number(0), "line": Number(6)}, "start": Object {"character": Number(4), "line": Number(4)}}}], "textDocument": Object {"uri": String("file:///data/repos/lean/t.lean"), "version": Number(9)}}) })))
2023-03-22T11:22:13.616 helix_term::application [ERROR] received malformed notification from Language Server: Unhandled
2023-03-22T11:22:13.618 helix_view::document [DEBUG] id 1 modified - last saved: 0, current: 1
2023-03-22T11:22:13.618 helix_lsp::transport [INFO] <- {"params":{"version":9,"uri":"file:///data/repos/lean/t.lean","diagnostics":[{"source":"Lean 4","severity":1,"range":{"start":{"line":4,"character":2},"end":{"line":4,"character":3}},"message":"type mismatch\n  p\nhas type\n  Prop : Type\nbut is expected to have type\n  q ∧ p : Prop","fullRange":{"start":{"line":4,"character":2},"end":{"line":4,"character":3}}},{"source":"Lean 4","severity":1,"range":{"start":{"line":4,"character":4},"end":{"line":4,"character":4}},"message":"expected token","fullRange":{"start":{"line":4,"character":4},"end":{"line":4,"character":4}}}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}
2023-03-22T11:22:13.618 helix_lsp::transport [INFO] <- {"params":{"textDocument":{"version":9,"uri":"file:///data/repos/lean/t.lean"},"processing":[]},"method":"$/lean/fileProgress","jsonrpc":"2.0"}
2023-03-22T11:22:13.619 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "textDocument/publishDiagnostics", params: Map({"diagnostics": Array [Object {"fullRange": Object {"end": Object {"character": Number(3), "line": Number(4)}, "start": Object {"character": Number(2), "line": Number(4)}}, "message": String("type mismatch\n  p\nhas type\n  Prop : Type\nbut is expected to have type\n  q ∧ p : Prop"), "range": Object {"end": Object {"character": Number(3), "line": Number(4)}, "start": Object {"character": Number(2), "line": Number(4)}}, "severity": Number(1), "source": String("Lean 4")}, Object {"fullRange": Object {"end": Object {"character": Number(4), "line": Number(4)}, "start": Object {"character": Number(4), "line": Number(4)}}, "message": String("expected token"), "range": Object {"end": Object {"character": Number(4), "line": Number(4)}, "start": Object {"character": Number(4), "line": Number(4)}}, "severity": Number(1), "source": String("Lean 4")}], "uri": String("file:///data/repos/lean/t.lean"), "version": Number(9)}) })))
2023-03-22T11:22:13.619 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "textDocument/publishDiagnostics", params: Map({"diagnostics": Array [Object {"fullRange": Object {"end": Object {"character": Number(3), "line": Number(4)}, "start": Object {"character": Number(2), "line": Number(4)}}, "message": String("type mismatch\n  p\nhas type\n  Prop : Type\nbut is expected to have type\n  q ∧ p : Prop"), "range": Object {"end": Object {"character": Number(3), "line": Number(4)}, "start": Object {"character": Number(2), "line": Number(4)}}, "severity": Number(1), "source": String("Lean 4")}, Object {"fullRange": Object {"end": Object {"character": Number(4), "line": Number(4)}, "start": Object {"character": Number(4), "line": Number(4)}}, "message": String("expected token"), "range": Object {"end": Object {"character": Number(4), "line": Number(4)}, "start": Object {"character": Number(4), "line": Number(4)}}, "severity": Number(1), "source": String("Lean 4")}], "uri": String("file:///data/repos/lean/t.lean"), "version": Number(9)}) })))
2023-03-22T11:22:13.619 helix_term::application [DEBUG] received editor event: LanguageServerMessage((0, Notification(Notification { jsonrpc: Some(V2), method: "$/lean/fileProgress", params: Map({"processing": Array [], "textDocument": Object {"uri": String("file:///data/repos/lean/t.lean"), "version": Number(9)}}) })))
2023-03-22T11:22:13.619 helix_term::application [ERROR] received malformed notification from Language Server: Unhandled
2023-03-22T11:22:13.746 helix_view::document [DEBUG] id 1 modified - last saved: 0, current: 2
2023-03-22T11:22:13.748 helix_view::document [DEBUG] id 1 modified - last saved: 0, current: 2
2023-03-22T11:22:13.852 helix_view::document [DEBUG] id 1 modified - last saved: 0, current: 2
2023-03-22T11:22:14.132 helix_view::document [DEBUG] id 1 modified - last saved: 0, current: 2
2023-03-22T11:22:14.258 helix_view::document [DEBUG] id 1 modified - last saved: 0, current: 2
2023-03-22T11:22:14.360 helix_view::document [DEBUG] submitting save of doc 'Some("/data/repos/lean/t.lean")'
2023-03-22T11:22:14.361 helix_view::document [DEBUG] id 1 modified - last saved: 0, current: 2
2023-03-22T11:22:14.363 helix_term::application [DEBUG] received editor event: DocumentSaved(Ok(DocumentSavedEvent { revision: 2, doc_id: DocumentId(1), path: "/data/repos/lean/t.lean", text: ["theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p :=\n  fun hpq : p ∧ q =>\n  have hp : p := And.left hpq\n  have hq : q := And.right hpq\n  p \\to q\n  show q ∧ p from And.intro hq hp\n"] }))
2023-03-22T11:22:14.363 helix_term::application [DEBUG] document Some("/data/repos/lean/t.lean") saved with revision 2
2023-03-22T11:22:14.363 helix_view::document [DEBUG] doc 1 revision updated 0 -> 2
2023-03-22T11:22:14.363 helix_view::editor [DEBUG] editor status: 't.lean' written, 7L 192B
2023-03-22T11:22:14.364 helix_view::document [DEBUG] id 1 modified - last saved: 2, current: 2
2023-03-22T11:22:14.532 helix_term::application [DEBUG] received editor event: IdleTimer
2023-03-22T11:22:15.006 helix_view::document [DEBUG] id 1 modified - last saved: 2, current: 2
2023-03-22T11:22:15.177 helix_view::document [DEBUG] id 1 modified - last saved: 2, current: 2
2023-03-22T11:22:15.232 helix_view::document [DEBUG] id 1 modified - last saved: 2, current: 2
2023-03-22T11:22:15.407 helix_term::application [DEBUG] received editor event: IdleTimer
2023-03-22T11:22:15.716 helix_view::document [DEBUG] submitting save of doc 'Some("/data/repos/lean/t.lean")'
2023-03-22T11:22:15.716 helix_term::job [DEBUG] waiting on jobs...
2023-03-22T11:22:15.717 helix_view::document [DEBUG] doc 1 revision updated 2 -> 2
2023-03-22T11:22:15.717 helix_term::commands::typed [DEBUG] quitting...
2023-03-22T11:22:15.717 helix_view::document [DEBUG] id 1 modified - last saved: 2, current: 2
2023-03-22T11:22:15.717 helix_term::job [DEBUG] waiting on jobs...
2023-03-22T11:22:15.717 helix_term::job [DEBUG] waiting on jobs...
2023-03-22T11:22:15.718 helix_lsp::transport [INFO] -> {"jsonrpc":"2.0","method":"shutdown","id":1}
2023-03-22T11:22:15.729 helix_lsp::transport [INFO] <- {"result":null,"jsonrpc":"2.0","id":1}
2023-03-22T11:22:15.729 helix_lsp::transport [INFO] <- null
2023-03-22T11:22:15.730 helix_lsp::transport [INFO] -> {"jsonrpc":"2.0","method":"exit"}
2023-03-22T11:22:15.730 mio::poll [TRACE] deregistering event source from poller
2023-03-22T11:22:15.731 mio::poll [TRACE] deregistering event source from poller
2023-03-22T11:22:15.731 mio::poll [TRACE] deregistering event source from poller
2023-03-22T11:22:15.731 mio::poll [TRACE] deregistering event source from poller
2023-03-22T11:22:15.731 mio::poll [TRACE] deregistering event source from poller

Platform

Void Linux

Terminal Emulator

Alacritty

Helix Version

helix 22.12

[kirawi]

Have you tried removing the lean. prefix in the config? I think VSCode uses it to know which language to configure.

[danjenson]

Yep, that didn't do anything. In fact, it looks like nothing is really working beyond type checking / errors with the lean language server.

[kendfss]

nothing is really working...

fwiw, not everything that depends on LSP is explicitly labelled as such. Like "rename symbol" is space -> r and doesn't show up when you look at lsp options.