feat: revamp server logging

Author: mhuisi

src/Lean/Data/JsonRpc.lean

@@ -26,7 +26,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⟩
 
@@ -308,6 +308,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

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

@@ -1050,8 +1050,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

src/Lean/Server/Logging.lean

@@ -0,0 +1,139 @@
+/-
+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))
+
+public inductive MessageDirection where
+  | clientToServer
+  | serverToClient
+  deriving Inhabited, FromJson, ToJson
+
+inductive MessageKind where
+  | request
+  | notification
+  | response
+  | responseError
+  deriving FromJson, ToJson
+
+def MessageKind.ofMessage : JsonRpc.Message → MessageKind
+  | .request .. => .request
+  | .notification .. => .notification
+  | .response .. => .response
+  | .responseError .. => .responseError
+
+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 : MessageDirection
+  kind : MessageKind
+  msg : JsonRpc.Message
+  deriving FromJson, ToJson
+
+public def writeLogEntry (cfg : LogConfig) (pending : Std.HashMap JsonRpc.RequestID MessageMethod)
+    (log : IO.FS.Handle) (direction : 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/Test/Runner.lean

@@ -698,8 +698,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

@@ -120,22 +120,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. -/