max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: clarify server protocol violations around initialize (#11091)

Browse source
This commit is contained in:
Marc Huisinga 2025-11-05 10:53:39 +01:00 • committed by GitHub
parent e7f4f98071
commit 8b43fc54b2
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 56 additions and 53 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Lean/Data/Lsp/InitShutdown.lean
View file

@ -73,8 +73,7 @@ structure InitializationOptions where
structure InitializeParams where
processId? : Option Int := none
clientInfo? : Option ClientInfo := none
/- We don't support the deprecated rootPath
(rootPath? : Option String) -/
/-- Not used by the language server. We use the cwd of the server process instead. -/
rootUri? : Option String := none
initializationOptions? : Option InitializationOptions := none
capabilities : ClientCapabilities

106
src/Lean/Server/ProtocolOverview.lean
View file

@ -29,7 +29,7 @@ inductive ProtocolExtensionKind
structure RequestOverview where
method : String
direction : MessageDirection
kind : ProtocolExtensionKind
kinds : Array ProtocolExtensionKind
parameterType : Type
responseType : Type
description : String
@ -43,7 +43,7 @@ structure RpcRequestOverview where
structure NotificationOverview where
method : String
direction : MessageDirection
kind : ProtocolExtensionKind
kinds : Array ProtocolExtensionKind
parameterType : Type
description : String
@ -68,14 +68,18 @@ def protocolOverview : Array MessageOverview := #[
.notification {
method := "$/cancelRequest"
direction := .clientToServer
kind := .standard
kinds := #[.standard]
parameterType := CancelParams
description := "Emitted in VS Code when a running request is cancelled, e.g. when the document state has changed."
},
.request {
method := "initialize"
direction := .clientToServer
kind := .extendedParameterType #[``InitializeParams.initializationOptions?, ``InitializeParams.capabilities, ``ClientCapabilities.lean?]
kinds := #[
.standardViolation "The Lean language server currently ignores almost all standard client capabilities and expects clients to be sufficiently fully-featured.",
.standardViolation "The `InitializeParams.rootUri?` field is not used by the language server - it instead uses the cwd of the language server process.",
.extendedParameterType #[``InitializeParams.initializationOptions?, ``InitializeParams.capabilities, ``ClientCapabilities.lean?]
]
parameterType := InitializeParams
responseType := InitializeResult
description := "Emitted when the language server is being initialized. The server is only started once an `initialized` notification is emitted after the `initialize` request."
@ -83,14 +87,14 @@ def protocolOverview : Array MessageOverview := #[
.notification {
method := "initialized"
direction := .clientToServer
kind := .standard
kinds := #[.standard]
parameterType := InitializedParams
description := "Emitted after a response to the `initialize` request to start the server."
},
.request {
method := "shutdown"
direction := .clientToServer
kind := .standard
kinds := #[.standard]
parameterType := Option Empty
responseType := Option Empty
description := "Emitted when the language server is being asked to shut down and deliver responses for all pending requests."
@ -98,14 +102,14 @@ def protocolOverview : Array MessageOverview := #[
.notification {
method := "exit"
direction := .clientToServer
kind := .standard
kinds := #[.standard]
parameterType := Option Empty
description := "Emitted once the language server should shut down after a `shutdown` request."
},
.request {
method := "client/registerCapability"
direction := .serverToClient
kind := .standard
kinds := #[.standard]
parameterType := NestedType #[Option RegistrationParams, DidChangeWatchedFilesRegistrationOptions]
responseType := Option Empty
description := "Emitted by the language server after receiving the `initialized` notification to register file watchers for `.lean` and `.ilean` files using the `workspace/didChangeWatchedFiles` registration."
@ -113,56 +117,56 @@ def protocolOverview : Array MessageOverview := #[
.notification {
method := "textDocument/didOpen"
direction := .clientToServer
kind := .extendedParameterType #[``LeanDidOpenTextDocumentParams.dependencyBuildMode?]
kinds := #[.extendedParameterType #[``LeanDidOpenTextDocumentParams.dependencyBuildMode?]]
parameterType := LeanDidOpenTextDocumentParams
description := "Emitted in VS Code when a text document is opened. VS Code may sometimes emit this notification for files that were not opened in an editor."
},
.notification {
method := "textDocument/didClose"
direction := .clientToServer
kind := .standard
kinds := #[.standard]
parameterType := DidCloseTextDocumentParams
description := "Emitted in VS Code when a text document is closed. VS Code may sometimes emit this notification for files that were not opened in an editor."
},
.notification {
method := "textDocument/didChange"
direction := .clientToServer
kind := .standard
kinds := #[.standard]
parameterType := DidChangeTextDocumentParams
description := "Emitted in VS Code when a text document is edited."
},
.notification {
method := "textDocument/didSave"
direction := .clientToServer
kind := .standard
kinds := #[.standard]
parameterType := DidSaveTextDocumentParams
description := "Emitted in VS Code when a text document is saved."
},
.notification {
method := "workspace/didChangeWatchedFiles"
direction := .clientToServer
kind := .standard
kinds := #[.standard]
parameterType := DidChangeWatchedFilesParams
description := "Emitted in VS Code when one of the files that the language server registered a file watcher for changes."
},
.notification {
method := "textDocument/publishDiagnostics"
direction := .serverToClient
kind := .extendedParameterType #[``PublishDiagnosticsParams.diagnostics, ``DiagnosticWith.fullRange?, ``DiagnosticWith.isSilent?, ``DiagnosticWith.leanTags?]
kinds := #[.extendedParameterType #[``PublishDiagnosticsParams.diagnostics, ``DiagnosticWith.fullRange?, ``DiagnosticWith.isSilent?, ``DiagnosticWith.leanTags?]]
parameterType := PublishDiagnosticsParams
description := "Emitted by the language server whenever a new set of diagnostics becomes available for a file. Unlike most language servers, the Lean language server emits this notification incrementally while processing the file, not only when the full file has been processed."
},
.notification {
method := "$/lean/fileProgress"
direction := .serverToClient
kind := .leanSpecificMethod
kinds := #[.leanSpecificMethod]
parameterType := LeanFileProgressParams
description := "Emitted by the language server whenever the elaboration progress of a file changes."
},
.request {
method := "textDocument/completion"
direction := .clientToServer
kind := .standard
kinds := #[.standard]
parameterType := CompletionParams
responseType := CompletionList
description := "Emitted in VS Code when auto-completion is triggered, e.g. automatically while typing or after hitting Ctrl+Space."
@ -170,7 +174,7 @@ def protocolOverview : Array MessageOverview := #[
.request {
method := "completionItem/resolve"
direction := .clientToServer
kind := .standard
kinds := #[.standard]
parameterType := CompletionItem
responseType := CompletionItem
description := "Emitted in VS Code when an auto-completion entry is selected."
@ -178,7 +182,7 @@ def protocolOverview : Array MessageOverview := #[
.request {
method := "textDocument/codeAction"
direction := .clientToServer
kind := .standard
kinds := #[.standard]
parameterType := CodeActionParams
responseType := Array CodeAction
description := "Emitted in VS Code when code actions are triggered, e.g. automatically while typing, moving the text cursor or when hovering over a diagnostic."
@ -186,7 +190,7 @@ def protocolOverview : Array MessageOverview := #[
.request {
method := "codeAction/resolve"
direction := .clientToServer
kind := .standard
kinds := #[.standard]
parameterType := CodeAction
responseType := CodeAction
description := "Emitted in VS Code when a code action in the light bulb menu is selected."
@ -194,7 +198,7 @@ def protocolOverview : Array MessageOverview := #[
.request {
method := "textDocument/signatureHelp"
direction := .clientToServer
kind := .standard
kinds := #[.standard]
parameterType := SignatureHelpParams
responseType := Option SignatureHelp
description := "Emitted in VS Code when the signature help is triggered, e.g. automatically while typing or after hitting Ctrl+Shift+Space."
@ -202,7 +206,7 @@ def protocolOverview : Array MessageOverview := #[
.request {
method := "textDocument/hover"
direction := .clientToServer
kind := .standard
kinds := #[.standard]
parameterType := HoverParams
responseType := Option Hover
description := "Emitted in VS Code when hovering over an identifier in the editor."
@ -210,7 +214,7 @@ def protocolOverview : Array MessageOverview := #[
.request {
method := "textDocument/documentHighlight"
direction := .clientToServer
kind := .standard
kinds := #[.standard]
parameterType := DocumentHighlightParams
responseType := DocumentHighlightResult
description := "Emitted in VS Code when the text cursor is on an identifier."
@ -218,7 +222,7 @@ def protocolOverview : Array MessageOverview := #[
.request {
method := "textDocument/documentSymbol"
direction := .clientToServer
kind := .standard
kinds := #[.standard]
parameterType := DocumentSymbolParams
responseType := DocumentSymbolResult
description := "Emitted in VS Code when a file is first opened or when it is changed."
@ -226,7 +230,7 @@ def protocolOverview : Array MessageOverview := #[
.request {
method := "textDocument/foldingRange"
direction := .clientToServer
kind := .standard
kinds := #[.standard]
parameterType := FoldingRangeParams
responseType := Array FoldingRange
description := "Emitted in VS Code when a file is first opened or when it is changed."
@ -234,7 +238,7 @@ def protocolOverview : Array MessageOverview := #[
.request {
method := "textDocument/documentColor"
direction := .clientToServer
kind := .standard
kinds := #[.standard]
parameterType := DocumentColorParams
responseType := Array ColorInformation
description := "Emitted in VS Code when a file is first opened or when it is changed. The language server defines this handler to override the default document color handler of VS Code with an empty one."
@ -242,7 +246,7 @@ def protocolOverview : Array MessageOverview := #[
.request {
method := "textDocument/semanticTokens/range"
direction := .clientToServer
kind := .standard
kinds := #[.standard]
parameterType := SemanticTokensRangeParams
responseType := SemanticTokens
description := "Emitted in VS Code when a file is changed."
@ -250,7 +254,7 @@ def protocolOverview : Array MessageOverview := #[
.request {
method := "textDocument/semanticTokens/full"
direction := .clientToServer
kind := .standardViolation "Instead of reporting the full semantic tokens for the full file as specified by LSP, the Lean language server will only report the semantic tokens for the part of the file that has been processed so far. If the response is incomplete, the language server periodically emits `workspace/semanticTokens/refresh` to request another `textDocument/semanticTokens/full` request from the client. This process is repeated until the file has been fully processed and all semantic tokens have been reported. We use this trick to stream semantic tokens to VS Code, despite the fact that VS Code does not support result streaming."
kinds := #[.standardViolation "Instead of reporting the full semantic tokens for the full file as specified by LSP, the Lean language server will only report the semantic tokens for the part of the file that has been processed so far. If the response is incomplete, the language server periodically emits `workspace/semanticTokens/refresh` to request another `textDocument/semanticTokens/full` request from the client. This process is repeated until the file has been fully processed and all semantic tokens have been reported. We use this trick to stream semantic tokens to VS Code, despite the fact that VS Code does not support result streaming."]
parameterType := SemanticTokensParams
responseType := SemanticTokens
description := "Emitted in VS Code when a file is first opened, when it is changed or when VS Code receives a `workspace/semanticTokens/refresh` request from the server."
@ -258,7 +262,7 @@ def protocolOverview : Array MessageOverview := #[
.request {
method := "workspace/semanticTokens/refresh"
direction := .serverToClient
kind := .standard
kinds := #[.standard]
parameterType := Option Empty
responseType := Option Empty
description := "Emitted by the language server to request another `textDocument/semanticTokens/full` request from the client."
@ -266,7 +270,7 @@ def protocolOverview : Array MessageOverview := #[
.request {
method := "textDocument/inlayHint"
direction := .clientToServer
kind := .standardViolation "Instead of reporting the full inlay hints for the full file as specified by LSP, the Lean language server will only report the inlay hints for the part of the file that has been processed so far. If the response is incomplete, the language server periodically emits `workspace/inlayHint/refresh` to request another `textDocument/inlayHint` request from the client. This process is repeated until the file has been fully processed and all inlay hints have been reported. We use this trick to stream inlay hints to VS Code, despite the fact that VS Code does not support result streaming."
kinds := #[.standardViolation "Instead of reporting the full inlay hints for the full file as specified by LSP, the Lean language server will only report the inlay hints for the part of the file that has been processed so far. If the response is incomplete, the language server periodically emits `workspace/inlayHint/refresh` to request another `textDocument/inlayHint` request from the client. This process is repeated until the file has been fully processed and all inlay hints have been reported. We use this trick to stream inlay hints to VS Code, despite the fact that VS Code does not support result streaming."]
parameterType := InlayHintParams
responseType := Array InlayHint
description := "Emitted in VS Code when a file is first opened, when it is changed or when VS Code receives a `workspace/inlayHint/refresh` request from the server."
@ -274,7 +278,7 @@ def protocolOverview : Array MessageOverview := #[
.request {
method := "workspace/inlayHint/refresh"
direction := .serverToClient
kind := .standard
kinds := #[.standard]
parameterType := Option Empty
responseType := Option Empty
description := "Emitted by the language server to request another `textDocument/inlayHint` request from the client."
@ -282,7 +286,7 @@ def protocolOverview : Array MessageOverview := #[
.request {
method := "textDocument/definition"
direction := .clientToServer
kind := .standard
kinds := #[.standard]
parameterType := DefinitionParams
responseType := Array LocationLink
description := "Emitted in VS Code when clicking 'Go to Definition' in the context menu or using Ctrl+Click."
@ -290,7 +294,7 @@ def protocolOverview : Array MessageOverview := #[
.request {
method := "textDocument/declaration"
direction := .clientToServer
kind := .standard
kinds := #[.standard]
parameterType := DefinitionParams
responseType := Array LocationLink
description := "Emitted in VS Code when clicking 'Go to Declaration' in the context menu."
@ -298,7 +302,7 @@ def protocolOverview : Array MessageOverview := #[
.request {
method := "textDocument/typeDefinition"
direction := .clientToServer
kind := .standard
kinds := #[.standard]
parameterType := DefinitionParams
responseType := Array LocationLink
description := "Emitted in VS Code when clicking 'Go to Type Definition' in the context menu."
@ -306,7 +310,7 @@ def protocolOverview : Array MessageOverview := #[
.request {
method := "textDocument/references"
direction := .clientToServer
kind := .standard
kinds := #[.standard]
parameterType := ReferenceParams
responseType := Array Location
description := "Emitted in VS Code when clicking 'Find All References' or 'Go to References' in the context menu."
@ -314,7 +318,7 @@ def protocolOverview : Array MessageOverview := #[
.request {
method := "textDocument/prepareCallHierarchy"
direction := .clientToServer
kind := .standard
kinds := #[.standard]
parameterType := CallHierarchyPrepareParams
responseType := Array CallHierarchyItem
description := "Emitted in VS Code when clicking 'Show Call Hierarchy' in the context menu."
@ -322,7 +326,7 @@ def protocolOverview : Array MessageOverview := #[
.request {
method := "callHierarchy/incomingCalls"
direction := .clientToServer
kind := .standard
kinds := #[.standard]
parameterType := CallHierarchyIncomingCallsParams
responseType := Array CallHierarchyIncomingCall
description := "Emitted in VS Code when expanding a node in the call hierarchy in 'incoming calls' mode."
@ -330,7 +334,7 @@ def protocolOverview : Array MessageOverview := #[
.request {
method := "callHierarchy/outgoingCalls"
direction := .clientToServer
kind := .standard
kinds := #[.standard]
parameterType := CallHierarchyOutgoingCallsParams
responseType := Array CallHierarchyOutgoingCall
description := "Emitted in VS Code when expanding a node in the call hierarchy in 'outgoing calls' mode."
@ -338,7 +342,7 @@ def protocolOverview : Array MessageOverview := #[
.request {
method := "$/lean/prepareModuleHierarchy"
direction := .clientToServer
kind := .leanSpecificMethod
kinds := #[.leanSpecificMethod]
parameterType := LeanPrepareModuleHierarchyParams
responseType := Option LeanModule
description := "Emitted in VS Code when clicking 'Show Module Hierarchy' or 'Show Inverse Module Hierarchy' in the context menu."
@ -346,7 +350,7 @@ def protocolOverview : Array MessageOverview := #[
.request {
method := "$/lean/moduleHierarchy/imports"
direction := .clientToServer
kind := .leanSpecificMethod
kinds := #[.leanSpecificMethod]
parameterType := LeanModuleHierarchyImportsParams
responseType := Array LeanImport
description := "Emitted in VS Code when expanding a node in the module hierarchy."
@ -354,7 +358,7 @@ def protocolOverview : Array MessageOverview := #[
.request {
method := "$/lean/moduleHierarchy/importedBy"
direction := .clientToServer
kind := .leanSpecificMethod
kinds := #[.leanSpecificMethod]
parameterType := LeanModuleHierarchyImportedByParams
responseType := Array LeanImport
description := "Emitted in VS Code when expanding a node in the inverse module hierarchy."
@ -362,7 +366,7 @@ def protocolOverview : Array MessageOverview := #[
.request {
method := "textDocument/prepareRename"
direction := .clientToServer
kind := .standard
kinds := #[.standard]
parameterType := PrepareRenameParams
responseType := Option Range
description := "Emitted in VS Code when clicking 'Rename Symbol' in the context menu."
@ -370,7 +374,7 @@ def protocolOverview : Array MessageOverview := #[
.request {
method := "textDocument/rename"
direction := .clientToServer
kind := .standard
kinds := #[.standard]
parameterType := RenameParams
responseType := WorkspaceEdit
description := "Emitted in VS Code when entering an identifier after clicking 'Rename Symbol' in the context menu."
@ -378,7 +382,7 @@ def protocolOverview : Array MessageOverview := #[
.request {
method := "workspace/symbol"
direction := .clientToServer
kind := .standard
kinds := #[.standard]
parameterType := WorkspaceSymbolParams
responseType := Array SymbolInformation
description := "Emitted in VS Code when opening the command prompt and entering a `#` prefix with a query after it."
@ -386,7 +390,7 @@ def protocolOverview : Array MessageOverview := #[
.request {
method := "$/lean/plainGoal"
direction := .clientToServer
kind := .leanSpecificMethod
kinds := #[.leanSpecificMethod]
parameterType := PlainGoalParams
responseType := Option PlainGoal
description := "Not used in VS Code. Emitted in editors that do not support an interactive InfoView (e.g. Emacs) and interactive tests."
@ -394,7 +398,7 @@ def protocolOverview : Array MessageOverview := #[
.request {
method := "$/lean/plainTermGoal"
direction := .clientToServer
kind := .leanSpecificMethod
kinds := #[.leanSpecificMethod]
parameterType := PlainTermGoalParams
responseType := Option PlainTermGoal
description := "Not used in VS Code. Emitted in editors that do not support an interactive InfoView (e.g. Emacs) and interactive tests."
@ -402,7 +406,7 @@ def protocolOverview : Array MessageOverview := #[
.request {
method := "textDocument/waitForDiagnostics"
direction := .clientToServer
kind := .leanSpecificMethod
kinds := #[.leanSpecificMethod]
parameterType := WaitForDiagnosticsParams
responseType := WaitForDiagnostics
description := "Not used in the editor. Emitted in interactive tests to wait for all diagnostics up to a given point."
@ -410,7 +414,7 @@ def protocolOverview : Array MessageOverview := #[
.request {
method := "$/lean/waitForILeans"
direction := .clientToServer
kind := .leanSpecificMethod
kinds := #[.leanSpecificMethod]
parameterType := WaitForILeansParams
responseType := WaitForILeans
description := "Not used in the editor. Emitted in interactive tests to wait for all .ileans in the project and the .ilean of the given file to be loaded."
@ -418,7 +422,7 @@ def protocolOverview : Array MessageOverview := #[
.request {
method := "$/lean/rpc/connect"
direction := .clientToServer
kind := .leanSpecificMethod
kinds := #[.leanSpecificMethod]
parameterType := RpcConnectParams
responseType := RpcConnected
description := "Emitted in VS Code when an RPC session for InfoView interactivity is initially set up."
@ -426,21 +430,21 @@ def protocolOverview : Array MessageOverview := #[
.notification {
method := "$/lean/rpc/release"
direction := .clientToServer
kind := .leanSpecificMethod
kinds := #[.leanSpecificMethod]
parameterType := RpcReleaseParams
description := "Emitted in VS Code when an RPC object in the server (the lifecycle of which is managed by the client) is freed by the client."
},
.notification {
method := "$/lean/rpc/keepAlive"
direction := .clientToServer
kind := .leanSpecificMethod
kinds := #[.leanSpecificMethod]
parameterType := RpcKeepAliveParams
description := "Emitted periodically in VS Code to signal that the RPC client has not disconnected yet to keep the RPC session alive."
},
.request {
method := "$/lean/rpc/call"
direction := .clientToServer
kind := .leanSpecificMethod
kinds := #[.leanSpecificMethod]
parameterType := RpcCallParams
responseType := Json
description := "Emitted in VS Code when an RPC method is called. `RpcCallParams.method` and `RpcCallParams.params` can be any of the builtin `.rpcRequest`s described in this overview or any custom RPC methods tagged with `@[server_rpc_method]` that can be set up for use in the widget system."