From 19533ab1d4312903f98ff0429a5962db24ce402b Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Tue, 28 Oct 2025 17:26:59 +0100 Subject: [PATCH] feat: revamp server logging (#10787) This PR revamps the server logging mechanism to allow filtering the log output by LSP method. --- src/Lean/Data/JsonRpc.lean | 26 +- src/Lean/Data/Lsp/InitShutdown.lean | 21 +- src/Lean/Server.lean | 1 + src/Lean/Server/FileWorker.lean | 4 +- src/Lean/Server/Logging.lean | 121 ++++++ src/Lean/Server/ProtocolOverview.lean | 508 ++++++++++++++++++++++++++ src/Lean/Server/Test/Runner.lean | 2 +- src/Lean/Server/Utils.lean | 16 - src/Lean/Server/Watchdog.lean | 175 ++++++--- tests/lean/run/versoDocs.lean | 3 +- 10 files changed, 796 insertions(+), 81 deletions(-) create mode 100644 src/Lean/Server/Logging.lean create mode 100644 src/Lean/Server/ProtocolOverview.lean diff --git a/src/Lean/Data/JsonRpc.lean b/src/Lean/Data/JsonRpc.lean index ac9780c141..ff20dff854 100644 --- a/src/Lean/Data/JsonRpc.lean +++ b/src/Lean/Data/JsonRpc.lean @@ -25,7 +25,7 @@ inductive RequestID where | str (s : String) | num (n : JsonNumber) | null - deriving Inhabited, BEq, Ord + deriving Inhabited, BEq, Hashable, Ord instance : OfNat RequestID n := ⟨RequestID.num n⟩ @@ -307,6 +307,12 @@ inductive MessageMetaData where | responseError (id : RequestID) (code : ErrorCode) (message : String) (data? : Option Json) deriving Inhabited +def Message.metaData : Message → MessageMetaData + | .request id method .. => .request id method + | .notification method .. => .notification method + | .response id .. => .response id + | .responseError id code message data? => .responseError id code message data? + def MessageMetaData.toMessage : MessageMetaData → Message | .request id method => .request id method none | .notification method => .notification method none @@ -394,6 +400,24 @@ Namely: def parseMessageMetaData (input : String) : Except String MessageMetaData := messageMetaDataParser input |>.run input +public inductive MessageDirection where + | clientToServer + | serverToClient + deriving Inhabited, FromJson, ToJson + +inductive MessageKind where + | request + | notification + | response + | responseError + deriving FromJson, ToJson + +def MessageKind.ofMessage : Message → MessageKind + | .request .. => .request + | .notification .. => .notification + | .response .. => .response + | .responseError .. => .responseError + end Lean.JsonRpc namespace IO.FS.Stream diff --git a/src/Lean/Data/Lsp/InitShutdown.lean b/src/Lean/Data/Lsp/InitShutdown.lean index ee9fb2b272..a953115926 100644 --- a/src/Lean/Data/Lsp/InitShutdown.lean +++ b/src/Lean/Data/Lsp/InitShutdown.lean @@ -47,15 +47,27 @@ instance Trace.hasToJson : ToJson Trace := | Trace.messages => "messages" | Trace.verbose => "verbose"⟩ +local instance [BEq α] [Hashable α] [ToJson α] : ToJson (Std.HashSet α) where + toJson s := .arr <| s.toArray.map toJson + +local instance [BEq α] [Hashable α] [FromJson α] : FromJson (Std.HashSet α) where + fromJson? + | .arr a => return Std.HashSet.ofArray <| ← a.mapM fromJson? + | _ => throw "Expected array when converting JSON to Std.HashSet" + +structure LogConfig where + logDir? : Option System.FilePath + allowedMethods? : Option (Std.HashSet String) + disallowedMethods? : Option (Std.HashSet String) + deriving FromJson, ToJson + /-- Lean-specific initialization options. -/ structure InitializationOptions where - /-- Time (in milliseconds) which must pass since latest edit until elaboration begins. Lower - values may make editors feel faster at the cost of higher CPU usage. Defaults to 200ms. -/ - editDelay? : Option Nat /-- Whether the client supports interactive widgets. When true, in order to improve performance the server may cease including information which can be retrieved interactively in some standard LSP messages. Defaults to false. -/ hasWidgets? : Option Bool + logCfg? : Option LogConfig deriving ToJson, FromJson structure InitializeParams where @@ -71,9 +83,6 @@ structure InitializeParams where workspaceFolders? : Option (Array WorkspaceFolder) := none deriving ToJson -def InitializeParams.editDelay (params : InitializeParams) : Nat := - params.initializationOptions? |>.bind (·.editDelay?) |>.getD 200 - instance : FromJson InitializeParams where fromJson? j := do /- Many of these params can be null instead of not present. diff --git a/src/Lean/Server.lean b/src/Lean/Server.lean index c843f8549c..5e9e63cb36 100644 --- a/src/Lean/Server.lean +++ b/src/Lean/Server.lean @@ -12,3 +12,4 @@ public import Lean.Server.FileWorker public import Lean.Server.Rpc public import Lean.Server.CodeActions public import Lean.Server.Test +public import Lean.Server.ProtocolOverview diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index a67d767449..c7c6142e89 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -1040,8 +1040,6 @@ where return false def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO Unit := do - let i ← maybeTee "fwIn.txt" false i - let o ← maybeTee "fwOut.txt" true o let initParams ← i.readLspRequestAs "initialize" InitializeParams let ⟨_, param⟩ ← i.readLspNotificationAs "textDocument/didOpen" LeanDidOpenTextDocumentParams let doc := param.textDocument @@ -1090,5 +1088,7 @@ def workerMain (opts : Options) : IO UInt32 := do catch err => e.putStrLn err.toString IO.Process.forceExit 1 -- Terminate all tasks of this process + finally + IO.Process.forceExit (α := UInt32) 1 end Lean.Server.FileWorker diff --git a/src/Lean/Server/Logging.lean b/src/Lean/Server/Logging.lean new file mode 100644 index 0000000000..1ee4a5e278 --- /dev/null +++ b/src/Lean/Server/Logging.lean @@ -0,0 +1,121 @@ +/- +Copyright (c) 2025 Lean FRO. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Marc Huisinga +-/ +module + +prelude +public import Lean.Data.JsonRpc +import Std.Time +import Lean.Data.Lsp.Extra +public import Lean.Data.Lsp.InitShutdown + +namespace Lean.Server.Logging + +public structure LogConfig where + isEnabled : Bool + logFile : System.FilePath + allowedMethods? : Option (Std.HashSet String) + disallowedMethods? : Option (Std.HashSet String) + +public def LogConfig.ofLspLogConfig (lspCfg? : Option Lsp.LogConfig) : IO LogConfig := do + let time ← Std.Time.ZonedDateTime.now + let time := time.format "yyyy-MM-dd-HH-mm-ss-SSSSXX" + let logFileName := s!"LSP_{time}.log" + let defaultLogFile : System.FilePath := System.FilePath.join "." logFileName + let some lspCfg := lspCfg? + | return { + isEnabled := false + logFile := defaultLogFile + allowedMethods? := none + disallowedMethods? := none + } + return { + isEnabled := true + logFile := lspCfg.logDir?.map (System.FilePath.join · logFileName) |>.getD defaultLogFile + allowedMethods? := lspCfg.allowedMethods? + disallowedMethods? := lspCfg.disallowedMethods? + } + +open Lean + +public inductive MessageMethod where + | request (method : String) + | rpcRequest (method : String) + | notification (method : String) + deriving Inhabited + +def MessageMethod.all : MessageMethod → Array String + | .request method + | .notification method => + #[method] + | .rpcRequest method => + #["$/lean/rpc/call", method] + +public def messageMethod? : JsonRpc.Message → Option MessageMethod + | .request _ method params? => do + if method == "$/lean/rpc/call" then + let params := toJson params? + if let .ok (callParams : Lsp.RpcCallParams) := fromJson? params then + return .rpcRequest callParams.method.toString + return .request method + | .notification method _ => + some <| .notification method + | _ => + none + +def messageId? : JsonRpc.Message → Option JsonRpc.RequestID + | .request id .. => some id + | .response id .. => some id + | .responseError id .. => some id + | _ => none + +def isMsgAllowed (cfg : LogConfig) + (pending : Std.HashMap JsonRpc.RequestID MessageMethod) + (msg : JsonRpc.Message) : Bool := Id.run do + if ! cfg.isEnabled then + return false + let some method := method? + | return false + let allMethods := method.all + if let some allowedMethods := cfg.allowedMethods? then + if allMethods.any (! allowedMethods.contains ·) then + return false + if let some disallowedMethods := cfg.disallowedMethods? then + if allMethods.any (disallowedMethods.contains ·) then + return false + return true +where + method? : Option MessageMethod := + messageMethod? msg <|> (do pending.get? (← messageId? msg)) + +local instance : ToJson Std.Time.ZonedDateTime where + toJson dt := dt.toISO8601String + +local instance : FromJson Std.Time.ZonedDateTime where + fromJson? + | .str s => Std.Time.ZonedDateTime.fromISO8601String s + | _ => throw "Expected string when converting JSON to Std.Time.ZonedDateTime" + +structure LogEntry where + time : Std.Time.ZonedDateTime + direction : JsonRpc.MessageDirection + kind : JsonRpc.MessageKind + msg : JsonRpc.Message + deriving FromJson, ToJson + +public def writeLogEntry (cfg : LogConfig) (pending : Std.HashMap JsonRpc.RequestID MessageMethod) + (log : IO.FS.Handle) (direction : JsonRpc.MessageDirection) (msg : JsonRpc.Message) : IO Unit := do + if ! isMsgAllowed cfg pending msg then + return + let entry : LogEntry := { + time := ← Std.Time.ZonedDateTime.now + direction + kind := .ofMessage msg + msg + } + let entry := toJson entry |>.compress + log.putStrLn entry + log.flush diff --git a/src/Lean/Server/ProtocolOverview.lean b/src/Lean/Server/ProtocolOverview.lean new file mode 100644 index 0000000000..c270e7c50f --- /dev/null +++ b/src/Lean/Server/ProtocolOverview.lean @@ -0,0 +1,508 @@ +/- +Copyright (c) 2025 Lean FRO. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Marc Huisinga +-/ +module + +prelude +import Lean.Server.FileWorker.WidgetRequests +import Lean.Widget.UserWidget + +/-! +This file includes a complete overview over the Lean LSP API for documentation purposes. +-/ + +namespace Lean.Server.Overview + +open Lean.JsonRpc Lean.Lsp Lean.Widget + +inductive ProtocolExtensionKind + | standard + | leanSpecificMethod + | extendedParameterType (fieldNames : Array Name) + | extendedResponseType (fieldNames : Array Name) + | extendedParameterAndResponseType (parameterFieldNames responseFieldNames : Array Name) + | standardViolation (description : String) + +structure RequestOverview where + method : String + direction : MessageDirection + kind : ProtocolExtensionKind + parameterType : Type + responseType : Type + description : String + +structure RpcRequestOverview where + method : Name + parameterType : Type + responseType : Type + description : String + +structure NotificationOverview where + method : String + direction : MessageDirection + kind : ProtocolExtensionKind + parameterType : Type + description : String + +inductive MessageOverview where + | request (o : RequestOverview) + | rpcRequest (o : RpcRequestOverview) + | notification (o : NotificationOverview) + +opaque NestedType (outerToInner : Array Type) : Type + +/-- +Complete overview over the full Lean LSP API. + +The Lean language server requires all files for which it receives requests and notifications +to be opened by a `textDocument/didOpen` notification first, i.e. for the language client +to fully manage the contents of all files. +It will discard notifications and error requests for closed files. +This is in violation with LSP, which leaves the possibility open for language servers to receive +requests for open files, but this violation does not create problems with either VS Code or NeoVim. +-/ +def protocolOverview : Array MessageOverview := #[ + .notification { + method := "$/cancelRequest" + direction := .clientToServer + kind := .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?] + 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." + }, + .notification { + method := "initialized" + direction := .clientToServer + kind := .standard + parameterType := InitializedParams + description := "Emitted after a response to the `initialize` request to start the server." + }, + .request { + method := "shutdown" + direction := .clientToServer + kind := .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." + }, + .notification { + method := "exit" + direction := .clientToServer + kind := .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 + 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." + }, + .notification { + method := "textDocument/didOpen" + direction := .clientToServer + kind := .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 + 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 + parameterType := DidChangeTextDocumentParams + description := "Emitted in VS Code when a text document is edited." + }, + .notification { + method := "textDocument/didSave" + direction := .clientToServer + kind := .standard + parameterType := DidSaveTextDocumentParams + description := "Emitted in VS Code when a text document is saved." + }, + .notification { + method := "workspace/didChangeWatchedFiles" + direction := .clientToServer + kind := .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?] + 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 + parameterType := LeanFileProgressParams + description := "Emitted by the language server whenever the elaboration progress of a file changes." + }, + .request { + method := "textDocument/completion" + direction := .clientToServer + kind := .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." + }, + .request { + method := "completionItem/resolve" + direction := .clientToServer + kind := .standard + parameterType := CompletionItem + responseType := CompletionItem + description := "Emitted in VS Code when an auto-completion entry is selected." + }, + .request { + method := "textDocument/codeAction" + direction := .clientToServer + kind := .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." + }, + .request { + method := "codeAction/resolve" + direction := .clientToServer + kind := .standard + parameterType := CodeAction + responseType := CodeAction + description := "Emitted in VS Code when a code action in the light bulb menu is selected." + }, + .request { + method := "textDocument/signatureHelp" + direction := .clientToServer + kind := .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." + }, + .request { + method := "textDocument/hover" + direction := .clientToServer + kind := .standard + parameterType := HoverParams + responseType := Option Hover + description := "Emitted in VS Code when hovering over an identifier in the editor." + }, + .request { + method := "textDocument/documentHighlight" + direction := .clientToServer + kind := .standard + parameterType := DocumentHighlightParams + responseType := DocumentHighlightResult + description := "Emitted in VS Code when the text cursor is on an identifier." + }, + .request { + method := "textDocument/documentSymbol" + direction := .clientToServer + kind := .standard + parameterType := DocumentSymbolParams + responseType := DocumentSymbolResult + description := "Emitted in VS Code when a file is first opened or when it is changed." + }, + .request { + method := "textDocument/foldingRange" + direction := .clientToServer + kind := .standard + parameterType := FoldingRangeParams + responseType := Array FoldingRange + description := "Emitted in VS Code when a file is first opened or when it is changed." + }, + .request { + method := "textDocument/documentColor" + direction := .clientToServer + kind := .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." + }, + .request { + method := "textDocument/semanticTokens/range" + direction := .clientToServer + kind := .standard + parameterType := SemanticTokensRangeParams + responseType := SemanticTokens + description := "Emitted in VS Code when a file is changed." + }, + .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." + 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." + }, + .request { + method := "workspace/semanticTokens/refresh" + direction := .serverToClient + kind := .standard + parameterType := Option Empty + responseType := Option Empty + description := "Emitted by the language server to request another `textDocument/semanticTokens/full` request from the client." + }, + .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." + 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." + }, + .request { + method := "workspace/inlayHint/refresh" + direction := .serverToClient + kind := .standard + parameterType := Option Empty + responseType := Option Empty + description := "Emitted by the language server to request another `textDocument/inlayHint` request from the client." + }, + .request { + method := "textDocument/definition" + direction := .clientToServer + kind := .standard + parameterType := DefinitionParams + responseType := Array LocationLink + description := "Emitted in VS Code when clicking 'Go to Definition' in the context menu or using Ctrl+Click." + }, + .request { + method := "textDocument/declaration" + direction := .clientToServer + kind := .standard + parameterType := DefinitionParams + responseType := Array LocationLink + description := "Emitted in VS Code when clicking 'Go to Declaration' in the context menu." + }, + .request { + method := "textDocument/typeDefinition" + direction := .clientToServer + kind := .standard + parameterType := DefinitionParams + responseType := Array LocationLink + description := "Emitted in VS Code when clicking 'Go to Type Definition' in the context menu." + }, + .request { + method := "textDocument/references" + direction := .clientToServer + kind := .standard + parameterType := ReferenceParams + responseType := Array Location + description := "Emitted in VS Code when clicking 'Find All References' or 'Go to References' in the context menu." + }, + .request { + method := "textDocument/prepareCallHierarchy" + direction := .clientToServer + kind := .standard + parameterType := CallHierarchyPrepareParams + responseType := Array CallHierarchyItem + description := "Emitted in VS Code when clicking 'Show Call Hierarchy' in the context menu." + }, + .request { + method := "callHierarchy/incomingCalls" + direction := .clientToServer + kind := .standard + parameterType := CallHierarchyIncomingCallsParams + responseType := Array CallHierarchyIncomingCall + description := "Emitted in VS Code when expanding a node in the call hierarchy in 'incoming calls' mode." + }, + .request { + method := "callHierarchy/outgoingCalls" + direction := .clientToServer + kind := .standard + parameterType := CallHierarchyOutgoingCallsParams + responseType := Array CallHierarchyOutgoingCall + description := "Emitted in VS Code when expanding a node in the call hierarchy in 'outgoing calls' mode." + }, + .request { + method := "$/lean/prepareModuleHierarchy" + direction := .clientToServer + kind := .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." + }, + .request { + method := "$/lean/moduleHierarchy/imports" + direction := .clientToServer + kind := .leanSpecificMethod + parameterType := LeanModuleHierarchyImportsParams + responseType := Array LeanImport + description := "Emitted in VS Code when expanding a node in the module hierarchy." + }, + .request { + method := "$/lean/moduleHierarchy/importedBy" + direction := .clientToServer + kind := .leanSpecificMethod + parameterType := LeanModuleHierarchyImportedByParams + responseType := Array LeanImport + description := "Emitted in VS Code when expanding a node in the inverse module hierarchy." + }, + .request { + method := "textDocument/prepareRename" + direction := .clientToServer + kind := .standard + parameterType := PrepareRenameParams + responseType := Option Range + description := "Emitted in VS Code when clicking 'Rename Symbol' in the context menu." + }, + .request { + method := "textDocument/rename" + direction := .clientToServer + kind := .standard + parameterType := RenameParams + responseType := WorkspaceEdit + description := "Emitted in VS Code when entering an identifier after clicking 'Rename Symbol' in the context menu." + }, + .request { + method := "workspace/symbol" + direction := .clientToServer + kind := .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." + }, + .request { + method := "$/lean/plainGoal" + direction := .clientToServer + kind := .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." + }, + .request { + method := "$/lean/plainTermGoal" + direction := .clientToServer + kind := .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." + }, + .request { + method := "textDocument/waitForDiagnostics" + direction := .clientToServer + kind := .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." + }, + .request { + method := "$/lean/waitForILeans" + direction := .clientToServer + kind := .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." + }, + .request { + method := "$/lean/rpc/connect" + direction := .clientToServer + kind := .leanSpecificMethod + parameterType := RpcConnectParams + responseType := RpcConnected + description := "Emitted in VS Code when an RPC session for InfoView interactivity is initially set up." + }, + .notification { + method := "$/lean/rpc/release" + direction := .clientToServer + kind := .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 + 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 + 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." + }, + .rpcRequest { + method := `Lean.Widget.getInteractiveDiagnostics + parameterType := GetInteractiveDiagnosticsParams + responseType := Array InteractiveDiagnostic + description := "Emitted in VS Code when the text cursor is moved, the set of diagnostics at the cursor position changes or the file starts or finishes processing." + }, + .rpcRequest { + method := `Lean.Widget.getInteractiveGoals + parameterType := Lsp.PlainGoalParams + responseType := Option InteractiveGoals + description := "Emitted in VS Code when the text cursor is moved, the set of diagnostics at the cursor position changes or the file starts or finishes processing." + }, + .rpcRequest { + method := `Lean.Widget.getInteractiveTermGoal + parameterType := Lsp.PlainTermGoalParams + responseType := Option InteractiveTermGoal + description := "Emitted in VS Code when the text cursor is moved, the set of diagnostics at the cursor position changes or the file starts or finishes processing." + }, + .rpcRequest { + method := `Lean.Widget.getWidgets + parameterType := Position + responseType := GetWidgetsResponse + description := "Emitted in VS Code when the text cursor is moved, the set of diagnostics at the cursor position changes or the file starts or finishes processing." + }, + .rpcRequest { + method := `Lean.Widget.InteractiveDiagnostics.infoToInteractive + parameterType := WithRpcRef Elab.InfoWithCtx + responseType := InfoPopup + description := "Emitted in VS Code when hovering over terms in the InfoView." + }, + .rpcRequest { + method := `Lean.Widget.getGoToLocation + parameterType := GetGoToLocationParams + responseType := Array Lsp.LocationLink + description := "Emitted in VS Code when clicking 'Go to Definition' in the context menu of the InfoView or using Ctrl+Click in the InfoView." + }, + .rpcRequest { + method := `Lean.Widget.lazyTraceChildrenToInteractive + parameterType := WithRpcRef LazyTraceChildren + responseType := Array InteractiveMessage + description := "Emitted in VS Code when unfolding a lazy trace message in the InfoView." + }, + .rpcRequest { + method := `Lean.Widget.highlightMatches + parameterType := HighlightMatchesParams + responseType := HighlightedInteractiveMessage + description := "Emitted in VS Code when using the trace search in the InfoView." + }, + .rpcRequest { + method := `Lean.Widget.getWidgetSource + parameterType := GetWidgetSourceParams + responseType := WidgetSource + description := "Emitted in VS Code when a widget is imported from another widget." + }, + .rpcRequest { + method := `Lean.Widget.InteractiveDiagnostics.msgToInteractive + parameterType := MsgToInteractive + responseType := InteractiveMessage + description := "Emitted in VS Code in some widgets to convert non-interactive messages to interactive ones." + }, +] diff --git a/src/Lean/Server/Test/Runner.lean b/src/Lean/Server/Test/Runner.lean index 46abc5be75..8cb924b41e 100644 --- a/src/Lean/Server/Test/Runner.lean +++ b/src/Lean/Server/Test/Runner.lean @@ -697,8 +697,8 @@ partial def main (args : List String) : IO Unit := do -- We want `dbg_trace` tactics to write directly to stderr instead of being caught in reuse Ipc.runWith ipcCmd ipcArgs do let initializationOptions? := some { - editDelay? := none hasWidgets? := some true + logCfg? := none } let capabilities := { textDocument? := some { diff --git a/src/Lean/Server/Utils.lean b/src/Lean/Server/Utils.lean index 74fdcc15e6..46a0826d39 100644 --- a/src/Lean/Server/Utils.lean +++ b/src/Lean/Server/Utils.lean @@ -119,22 +119,6 @@ def replaceLspRange (text : FileMap) (r : Lsp.Range) (newText : String) : FileMa open IO -/-- -Duplicates an I/O stream to a log file `fName` in LEAN_SERVER_LOG_DIR -if that envvar is set. --/ -def maybeTee (fName : String) (isOut : Bool) (h : FS.Stream) : IO FS.Stream := do - match (← IO.getEnv "LEAN_SERVER_LOG_DIR") with - | none => pure h - | some logDir => - IO.FS.createDirAll logDir - let hTee ← FS.Handle.mk (System.mkFilePath [logDir, fName]) FS.Mode.write - let hTee := FS.Stream.ofHandle hTee - pure $ if isOut then - hTee.chainLeft h true - else - h.chainRight hTee true - open Lsp /-- Returns the document contents with the change applied. -/ diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index 50f1ca5f14..00e55d5e4e 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -13,6 +13,8 @@ public import Lean.Server.Requests public import Lean.Server.References public import Lean.Server.Completion.CompletionUtils public import Init.Data.List.Sort +public import Std.Sync.Channel +public import Lean.Server.Logging public section @@ -397,10 +399,19 @@ section ServerM let rd := { rd with finalizedWorkerILeanVersions := ∅ } { rd with finalizedWorkerILeanVersions := f finalized } + inductive LogMsg where + | deserialized (direction : MessageDirection) (msg : JsonRpc.Message) + | serialized (direction : MessageDirection) (msg : String) + deriving Inhabited + + structure LogData where + cfg : Logging.LogConfig + chan? : Option (Std.Channel LogMsg) + structure ServerContext where hIn : FS.Stream hOut : FS.Stream - hLog : FS.Stream + logData : LogData /-- Command line arguments. -/ args : List String fileWorkersRef : IO.Ref FileWorkerMap @@ -418,6 +429,25 @@ section ServerM abbrev ServerM := ReaderT ServerContext IO + def readMessage : ServerM JsonRpc.Message := do + let ctx ← read + let msg ← ctx.hIn.readLspMessage + if let some logChan := ctx.logData.chan? then + logChan.sync.send <| .deserialized .clientToServer msg + return msg + + def writeMessage (msg : JsonRpc.Message) : ServerM Unit := do + let ctx ← read + if let some logChan := ctx.logData.chan? then + logChan.sync.send <| .deserialized .serverToClient msg + (← read).hOut.writeLspMessage msg + + def writeSerializedMessage (msg : String) : ServerM Unit := do + let ctx ← read + if let some logChan := ctx.logData.chan? then + logChan.sync.send <| .serialized .serverToClient msg + (← read).hOut.writeSerializedLspMessage msg + def updateFileWorkers (val : FileWorker) : ServerM Unit := do (←read).fileWorkersRef.modify (fun fileWorkers => fileWorkers.insert val.doc.uri val) @@ -461,10 +491,11 @@ section ServerM let rd := rd.modifyFinalizedWorkerILeanVersions (·.erase uri) (pending, rd) for pendingWaitForILeanRequest in pendingWaitForILeanRequests do - s.hOut.writeLspResponseError { + writeMessage { id := pendingWaitForILeanRequest.id, code := ErrorCode.contentModified, message := s!"The file worker for {uri} has been terminated." + : ResponseError Unit } @@ -483,7 +514,7 @@ section ServerM set <| d.clearWorkerRequestData uri return pendingRequests for (id, _) in pendingRequests do - ctx.hOut.writeLspResponseError { id := id, code := code, message := msg } + writeMessage { id := id, code := code, message := msg : ResponseError Unit } def eraseGetPendingRequest (uri : DocumentUri) (id : RequestID) : ServerM (Option (JsonRpc.Request Json)) := do let ctx ← read @@ -497,11 +528,6 @@ section ServerM let r? ← eraseGetPendingRequest uri id return r?.isSome - def log (msg : String) : ServerM Unit := do - let st ← read - st.hLog.putStrLn msg - st.hLog.flush - def handleILeanHeaderInfo (fw : FileWorker) (params : LeanILeanHeaderInfoParams) : ServerM Unit := do let module := fw.doc.mod let uri := fw.doc.uri @@ -526,7 +552,7 @@ section ServerM for pendingWaitForILeanRequest in pendingWaitForILeanRequests do if pendingWaitForILeanRequest.uri == uri && pendingWaitForILeanRequest.version <= params.version then - s.hOut.writeLspResponse { + writeMessage { id := pendingWaitForILeanRequest.id result := ⟨⟩ : Response WaitForILeans @@ -789,7 +815,6 @@ section ServerM -- from the old process, so that they can't race with one another in the client. fw.state.atomically (m := StateT (Std.TreeMap RequestID (ServerTask Unit × CancelToken)) ServerM) do let s ← get - let o := (← read).hOut let uri := fw.doc.uri if s matches .terminating then return @@ -805,7 +830,7 @@ section ServerM -- that were still pending. if let some req := req? then let resp ← handleResponseSpecialCases fw req msg - o.writeSerializedLspMessage resp + writeSerializedMessage resp | .responseError id code _ _ => do let wasPending ← erasePendingRequest uri id if code matches .requestCancelled then @@ -813,7 +838,7 @@ section ServerM if let some (_, cancelTk) := pendingWorkerToWatchdogRequests.get? id then cancelTk.set if wasPending then - o.writeSerializedLspMessage msg + writeSerializedMessage msg | .request id method => if method == "$/lean/queryModule" then if let .ok params := parseRequestParams? LeanQueryModuleParams msg then @@ -823,7 +848,7 @@ section ServerM if let .ok params? := parseRequestParams? (Option Json.Structured) msg then let globalID ← (← read).serverRequestData.modifyGet (·.trackOutboundRequest fw.doc.uri id) - o.writeLspMessage (Message.request globalID method params?) + writeMessage (Message.request globalID method params?) | .notification "$/lean/ileanHeaderInfo" => if let .ok params := parseNotificationParams? LeanILeanHeaderInfoParams msg then handleILeanHeaderInfo fw params @@ -837,11 +862,11 @@ section ServerM if let .ok params := parseNotificationParams? LeanImportClosureParams msg then handleImportClosure fw params | _ => - o.writeSerializedLspMessage msg + writeSerializedMessage msg def startFileWorker (m : DocumentMeta) : ServerM Unit := do let st ← read - st.hOut.writeLspMessage <| mkFileProgressAtPosNotification m 0 + writeMessage <| mkFileProgressAtPosNotification m 0 let workerProc ← Process.spawn { toStdioConfig := workerCfg cmd := st.workerPath.toString @@ -905,7 +930,7 @@ section ServerM s!"The file worker for {uri} has been terminated." -- Clear the diagnostics for this file so that stale errors -- do not remain in the editor forever. - (← read).hOut.writeLspMessage <| mkPublishDiagnosticsNotification fw.doc #[] + writeMessage <| mkPublishDiagnosticsNotification fw.doc #[] catch _ => -- Client closed stdout => Still ensure that file worker is terminated pure () @@ -1330,19 +1355,21 @@ section MessageHandling else match (← routeLspRequest method params) with | Except.error e => - (←read).hOut.writeLspResponseError <| e.toLspResponseError id + writeMessage <| e.toLspResponseError id return | Except.ok uri => pure uri if ! (← fileWorkerExists fileId) then /- Clients may send requests to closed files, which we respond to with an error. For example, VSCode sometimes sends requests just after closing a file, and RPC clients may also do so, e.g. due to remaining timers. -/ - (←read).hOut.writeLspResponseError - { id := id - /- Some clients (VSCode) also send requests *before* opening a file. We reply - with `contentModified` as that does not display a "request failed" popup. -/ - code := ErrorCode.contentModified - message := s!"Cannot process request to closed file '{toString fileId}'" } + writeMessage { + id := id + /- Some clients (VSCode) also send requests *before* opening a file. We reply + with `contentModified` as that does not display a "request failed" popup. -/ + code := ErrorCode.contentModified + message := s!"Cannot process request to closed file '{toString fileId}'" + : ResponseError Unit + } return let r := Request.mk id method params tryWriteMessage fileId r @@ -1350,23 +1377,24 @@ section MessageHandling def handleReferenceRequest α β [FromJson α] [ToJson β] (id : RequestID) (params : Json) (handler : α → ReaderT ReferenceRequestContext IO β) : ServerM Unit := do let ctx ← read - let hOut := ctx.hOut let fileWorkerMods := (← ctx.fileWorkersRef.get).fileWorkers.map fun _ fw => fw.doc.mod let references ← getReferences - let _ ← ServerTask.IO.asTask do + let _ ← ServerTask.IO.asTask <| ReaderT.run (ρ := ServerContext) (r := ctx) do try let params ← parseParams α params let result ← ReaderT.run (m := IO) (r := { fileWorkerMods, references : ReferenceRequestContext }) <| handler params - hOut.writeLspResponse ⟨id, result⟩ + writeMessage { id, result : Response β } catch -- TODO Do fancier error handling, like in file worker? - | e => hOut.writeLspResponseError { - id := id - code := ErrorCode.internalError - message := s!"Failed to process request {id}: {e}" - } + | e => + writeMessage { + id := id + code := ErrorCode.internalError + message := s!"Failed to process request {id}: {e}" + : ResponseError Unit + } def handleRequest (id : RequestID) (method : String) (params : Json) : ServerM Unit := do let ctx ← read @@ -1399,10 +1427,12 @@ section MessageHandling IO.wait rd.loadingTask.task let ⟨uri, version⟩ ← parseParams WaitForILeansParams params if let none ← getFileWorker? uri then - ctx.hOut.writeLspResponseError { + writeMessage { id code := ErrorCode.contentModified - message := s!"Cannot process '$/lean/waitForILeans' request to closed file '{uri}'" } + message := s!"Cannot process '$/lean/waitForILeans' request to closed file '{uri}'" + : ResponseError Unit + } return ctx.referenceData.atomically do let deferResponse := modify fun rd => @@ -1418,7 +1448,7 @@ section MessageHandling if lastFinalizedVersion < version then deferResponse return - ctx.hOut.writeLspResponse { + writeMessage { id result := ⟨⟩ : Response WaitForILeans @@ -1447,10 +1477,7 @@ section MessageHandling | "$/lean/rpc/keepAlive" => handle RpcKeepAliveParams (forwardNotification method) | _ => - -- implementation-dependent notifications can be safely ignored - if ! "$/".isPrefixOf method then - (←read).hLog.putStrLn s!"Got unsupported notification: {method}" - (←read).hLog.flush + pure () def handleResponse (id : RequestID) (result : Json) : ServerM Unit := do let some translation ← (← read).serverRequestData.modifyGet (·.translateInboundResponse id) @@ -1484,9 +1511,9 @@ section MainLoop def runClientTask : ServerM (ServerTask ServerEvent) := do let st ← read - let readMsgAction : IO ServerEvent := do + let readMsgAction : IO ServerEvent := ReaderT.run (r := st) do /- Runs asynchronously. -/ - let msg ← st.hIn.readLspMessage + let msg ← readMessage pure <| ServerEvent.clientMsg msg let clientTask := (← ServerTask.IO.asTask readMsgAction).mapCheap fun | Except.ok ev => ev @@ -1510,7 +1537,7 @@ section MainLoop match msg with | Message.request id "shutdown" _ => shutdown - st.hOut.writeLspResponse ⟨id, Json.null⟩ + writeMessage { id, result := Json.null : Response Json } | Message.request id method (some params) => handleRequest id method (toJson params) mainLoop (←runClientTask) @@ -1539,7 +1566,7 @@ section MainLoop (ErrorCode.workerCrashed, "likely due to a stack overflow or a bug") errorPendingRequests uri errorCode s!"Server process for {uri} crashed, {errorCausePointer}." - (← read).hOut.writeLspMessage <| mkFileProgressAtPosNotification doc 0 (kind := LeanFileProgressKind.fatalError) + writeMessage <| mkFileProgressAtPosNotification doc 0 (kind := LeanFileProgressKind.fatalError) setWorkerState fw .crashed mainLoop clientTask | WorkerEvent.terminated => @@ -1607,18 +1634,21 @@ def initAndRunWatchdogAux : ServerM Unit := do let st ← read try discard $ st.hIn.readLspNotificationAs "initialized" InitializedParams - st.hOut.writeLspRequest { + writeMessage { id := RequestID.str "register_lean_watcher" method := "client/registerCapability" param := some { - registrations := #[ { + registrations := #[{ id := "lean_watcher" method := "workspace/didChangeWatchedFiles" registerOptions := some <| toJson { watchers := #[ { globPattern := "**/*.lean" }, { globPattern := "**/*.ilean" } ] - : DidChangeWatchedFilesRegistrationOptions } - } ] - : RegistrationParams } + : DidChangeWatchedFilesRegistrationOptions + } + }] + : RegistrationParams + } + : Request (Option RegistrationParams) } let clientTask ← runClientTask mainLoop clientTask @@ -1641,10 +1671,11 @@ def initAndRunWatchdogAux : ServerM Unit := do break | .request id _ _ => -- The LSP spec suggests that requests after 'shutdown' should be errored in this manner. - st.hOut.writeLspResponseError { + writeMessage { id, code := .invalidRequest, message := "Request received after 'shutdown' request." + : ResponseError Unit } | _ => -- Ignore all other message types. @@ -1683,7 +1714,33 @@ def startLoadingReferences (referenceData : Std.Mutex ReferenceData) : IO Unit : referenceData.atomically <| modify fun rd => { rd with loadingTask := task.mapCheap fun _ => () } -def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do +def runMessageLoggingTask (logData : LogData) : IO Unit := do + let some ch := logData.chan? + | return + let _ ← ServerTask.IO.asTask do + let logFile ← IO.FS.Handle.mk logData.cfg.logFile FS.Mode.append + let mut pending : Std.HashMap RequestID Logging.MessageMethod := ∅ + repeat + let msg := (← ch.recv).get + let (direction, msg) := + match msg with + | .deserialized direction msg => + (direction, msg) + | .serialized direction msg => + let msg := Json.parse msg >>= fromJson? |>.toOption.get! + (direction, msg) + Logging.writeLogEntry logData.cfg pending logFile direction msg + match msg with + | .request id .. => + let msgMethod := Logging.messageMethod? msg |>.get! + pending := pending.insert id msgMethod + | .response id .. + | .responseError id .. => + pending := pending.erase id + | _ => + pure () + +def initAndRunWatchdog (args : List String) (i o : FS.Stream) : IO Unit := do let workerPath ← findWorkerPath let referenceData : Std.Mutex ReferenceData ← Std.Mutex.new { loadingTask := ServerTask.pure () @@ -1699,9 +1756,6 @@ def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do } let importData ← IO.mkRef ⟨Std.TreeMap.empty, Std.TreeMap.empty⟩ let requestData ← RequestDataMutex.new - let i ← maybeTee "wdIn.txt" false i - let o ← maybeTee "wdOut.txt" true o - let e ← maybeTee "wdErr.txt" true e let initRequest ← i.readLspRequestAs "initialize" InitializeParams o.writeLspResponse { id := initRequest.id @@ -1714,10 +1768,21 @@ def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do : InitializeResult } } + let logCfg ← Logging.LogConfig.ofLspLogConfig <| initRequest.param.initializationOptions?.bind (·.logCfg?) + let logChan? ← + if logCfg.isEnabled then + pure <| some <| ← Std.Channel.new (capacity := some 1024) + else + pure none + let logData : LogData := { + cfg := logCfg + chan? := logChan? + } + runMessageLoggingTask logData ReaderT.run initAndRunWatchdogAux { hIn := i hOut := o - hLog := e + logData args := args fileWorkersRef := fileWorkersRef initParams := initRequest.param @@ -1734,10 +1799,12 @@ def watchdogMain (args : List String) : IO UInt32 := do let o ← IO.getStdout let e ← IO.getStderr try - initAndRunWatchdog args i o e + initAndRunWatchdog args i o IO.Process.forceExit 0 -- Terminate all tasks of this process catch err => e.putStrLn s!"Watchdog error: {err}" IO.Process.forceExit 1 -- Terminate all tasks of this process + finally + IO.Process.forceExit (α := UInt32) 1 end Lean.Server.Watchdog diff --git a/tests/lean/run/versoDocs.lean b/tests/lean/run/versoDocs.lean index 64e1445592..c2f78fcfba 100644 --- a/tests/lean/run/versoDocs.lean +++ b/tests/lean/run/versoDocs.lean @@ -204,7 +204,8 @@ end A error: Unknown constant `a` Hint: Insert a fully-qualified name: - {name ̲(̲f̲u̲l̲l̲ ̲:̲=̲ ̲A̲.̲a̲)̲}`a` + • {name ̲(̲f̲u̲l̲l̲ ̲:̲=̲ ̲A̲.̲a̲)̲}`a` + • {name ̲(̲f̲u̲l̲l̲ ̲:̲=̲ ̲S̲t̲d̲.̲T̲i̲m̲e̲.̲M̲o̲d̲i̲f̲i̲e̲r̲.̲a̲)̲}`a` -/ #guard_msgs in /--