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

@@ -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

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.

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

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

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

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."
+  },
+]

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 {

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

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

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