feat: debugging LSP server via LEAN_SERVER_LOG_DIR

src/Lean/Server/FileWorker.lean

@@ -308,6 +308,10 @@ partial def mainLoop : Unit → ServerM Unit
   | _ => throw (userError "got invalid JSON-RPC message")
 
 def initAndRunWorker (i o e : FS.Stream) : IO Unit := do
+i ← maybeTee "fwIn.txt" false i;
+o ← maybeTee "fwOut.txt" true o;
+e ← maybeTee "fwErr.txt" true e;
+
 -- TODO(WN): act in accordance with InitializeParams
 _ ← Lsp.readLspRequestAs i "initialize" InitializeParams;
 param ← Lsp.readLspNotificationAs i "textDocument/didOpen" DidOpenTextDocumentParams;
@@ -332,7 +336,7 @@ end Test
 end Server
 end Lean
 
-def main (_ : List String) : IO UInt32 := do
+def main (args : List String) : IO UInt32 := do
 i ← IO.getStdin;
 o ← IO.getStdout;
 e ← IO.getStderr;

src/Lean/Server/README.md

@@ -27,34 +27,18 @@ An easy way to get an LSP client is to build the [sample extension](https://gith
       env: {
         LEAN_PATH: "$LEAN4_HOME/build/$RELEASE_OR_DEBUG/stage1/lib/lean/",
         LEAN_WORKER_PATH: "$LEAN4_HOME/src/Lean/Server/build/bin/FileWorker"
+        // Add this for LSP message logs
+        //, LEAN_SERVER_LOG_DIR: "my/log/dir"
       }
     }
   };
 ```
 
-or if logging LSP requests using Netcat (below):
-
-```typescript
-  let serverOptions: ServerOptions = {
-    command: "/usr/bin/nc",
-    args: ["localhost", "12345"],
-    options: null
-  };
-```
-
 ## Logging LSP requests
 
-### In `bash` with Netcat:
+### In general
 
-```
-cd $LEAN4_HOME/src/Lean/Server/
-mkfifo pipe
-# So that the server can find and import packages
-export LEAN_PATH=$LEAN4_HOME/build/$RELEASE_OR_DEBUG/stage0.5/lib/lean/
-export LEAN_WORKER_PATH=$LEAN4_HOME/src/Lean/Server/build/bin/FileWorker
-nc -l -p 12345 < pipe | tee client.log | ./build/bin/Watchdog 2> stderr | tee pipe server.log
-```
-will create three files to follow with `tail -f` -- `client.log` for client messages, `server.log` for server messages and `stderr` for server `IO.stderr` debugging.
+To log all LSP messages and server output into a directory, just set the `LEAN_SERVER_LOG_DIR` environment variable. This will create a file for each I/O stream of the main server process, as well as those of each worker process.
 
 ### In VSCode
 

src/Lean/Server/Utils.lean

@@ -1,6 +1,51 @@
 import Lean.Data.Position
 import Lean.Data.Lsp
 
+namespace IO
+namespace FS
+namespace Stream
+
+/-- Chains two streams by creating a new stream s.t. writing to it
+just writes to `a` but reading from it also duplicates the read output
+into `b`, c.f. `a | tee b` on Unix.
+NB: if `a` is written to but this stream is never read from,
+the output will *not* be duplicated. Use this if you only care
+about the data that was actually read. -/
+def chainRight (a : Stream) (b : Stream) (flushEagerly : Bool := false) : Stream :=
+{ isEof := a.isEof,
+  read := fun sz => do
+    bs ← a.read sz;
+    b.write bs;
+    when flushEagerly b.flush;
+    pure bs,
+  getLine := do
+    ln ← a.getLine;
+    b.putStr ln;
+    when flushEagerly b.flush;
+    pure ln,
+  flush := a.flush *> b.flush,
+  write := a.write,
+  putStr := a.putStr }
+
+/-- Like `tee a | b` on Unix. See `chainOut`. -/
+def chainLeft (a : Stream) (b : Stream) (flushEagerly : Bool := false) : Stream :=
+{ isEof := b.isEof,
+  read := b.read,
+  getLine := b.getLine,
+  flush := a.flush *> b.flush,
+  write := fun bs => do
+    a.write bs;
+    when flushEagerly a.flush;
+    b.write bs,
+  putStr := fun s => do
+    a.putStr s;
+    when flushEagerly a.flush;
+    b.putStr s }
+
+end Stream
+end FS
+end IO
+
 namespace Lean
 namespace Server
 
@@ -11,6 +56,22 @@ let pre := text.source.extract 0 start;
 let post := text.source.extract «end» text.source.bsize;
 (pre ++ newText ++ post).toFileMap
 
+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
+logDir ← getEnv "LEAN_SERVER_LOG_DIR";
+match logDir with
+| none => pure h
+| some logDir => do
+  hTee ← FS.Handle.mk (System.mkFilePath [logDir, fName]) FS.Mode.write true;
+  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 all changes applied, together with the position of the change
@@ -31,10 +92,5 @@ let accumulateChanges : TextDocumentContentChangeEvent → FileMap × String.Pos
 -- NOTE: We assume Lean files are below 16 EiB.
 changes.foldr accumulateChanges (oldText, 0xffffffff)
 
--- TODO(WN): should these instances be in Core?
-instance Thunk.monad : Monad Thunk :=
-{ pure := @Thunk.pure,
-  bind := @Thunk.bind }
-
 end Server
 end Lean

src/Lean/Server/Watchdog.lean

@@ -203,7 +203,7 @@ def startFileWorker (uri : DocumentUri) (version : Nat) (text : FileMap) : Serve
 st ← read;
 headerAst ← monadLift $ parseHeaderAst text.source;
 let doc : OpenDocument := ⟨version, text, headerAst⟩;
-workerProc ← monadLift $ Process.spawn {workerCfg with cmd := st.workerPath};
+workerProc ← monadLift $ Process.spawn { workerCfg with cmd := st.workerPath };
 pendingRequestsRef ← IO.mkRef (RBMap.empty : PendingRequestMap);
 -- the task will never access itself, so this is fine
 let commTaskFw : FileWorker := ⟨doc, workerProc, Task.pure WorkerEvent.terminated, WorkerState.running, pendingRequestsRef⟩;
@@ -409,11 +409,15 @@ let workerPath := match workerPath with
   | some p => p;
 fileWorkersRef ← IO.mkRef (RBMap.empty : FileWorkerMap);
 
+i ← maybeTee "wdIn.txt" false i;
+o ← maybeTee "wdOut.txt" true o;
+e ← maybeTee "wdErr.txt" true e;
+
 initRequest ← readLspRequestAs i "initialize" InitializeParams;
 writeLspResponse o initRequest.id
-  { capabilities := mkLeanServerCapabilities,
-    serverInfo? := some { name := "Lean 4 server",
-                          version? := "0.0.1" } : InitializeResult };
+{ capabilities := mkLeanServerCapabilities,
+  serverInfo? := some { name := "Lean 4 server",
+                        version? := "0.0.1" } : InitializeResult };
 
 runReader
   initAndRunWatchdogAux
@@ -436,7 +440,7 @@ end Lean
 
 -- TODO: compile separately OR add as a flag to the `lean` binary in order to stop
 -- polluting the global symbol list with a `main` (and ditto in FileWorker.lean)
-def main (_ : List String) : IO UInt32 := do
+def main (args : List String) : IO UInt32 := do
 i ← IO.getStdin;
 o ← IO.getStdout;
 e ← IO.getStderr;

src/Lean/Server/lean4-lsp.el

@@ -36,14 +36,19 @@
 (add-to-list 'lsp-language-id-configuration
              '(lean4-lsp-mode . "lean4"))
 
-(defconst lean4-server-bin (concat lean4-home "/src/Lean/Server/build/bin/ServerBin"))
+(defconst lean4-server-bin (concat lean4-home "/src/Lean/Server/build/bin/Watchdog"))
+(defconst lean4-worker-bin (concat lean4-home "/src/Lean/Server/build/bin/FileWorker"))
 (defconst lean4-lib (concat lean4-home "/build/release/stage1/lib/lean/"))
 
 (lsp-register-client
  (make-lsp-client :new-connection (lsp-stdio-connection lean4-server-bin)
                   :major-modes '(lean4-lsp-mode)
                   :environment-fn (lambda ()
-                                    '(("LEAN_PATH" . lean4-lib)))
+                                    '(("LEAN_PATH" . lean4-lib)
+                                      ("LEAN_WORKER_PATH" . lean4-worker-bin)
+                                      ;; Set to dump LSP communications
+                                      ;("LEAN_SERVER_LOG_DIR" . "my/log/dir")
+                                      ))
                   :server-id 'lean4-lsp))
 
 (add-hook 'lean4-lsp-mode-hook #'lsp)