feat: revamp server logging (#10787)

This PR revamps the server logging mechanism to allow filtering the log
output by LSP method.

Author: mhuisi

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