From 0e2e2886c83490bfa1ea9eb2c290339d0da0313f Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Fri, 9 Oct 2020 18:53:33 -0400 Subject: [PATCH] feat: debugging LSP server via LEAN_SERVER_LOG_DIR --- src/Lean/Server/FileWorker.lean | 6 ++- src/Lean/Server/README.md | 24 ++---------- src/Lean/Server/Utils.lean | 66 ++++++++++++++++++++++++++++++--- src/Lean/Server/Watchdog.lean | 14 ++++--- src/Lean/Server/lean4-lsp.el | 9 ++++- 5 files changed, 86 insertions(+), 33 deletions(-) diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index 9fcc9354ad..f41ffd3ab1 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/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; diff --git a/src/Lean/Server/README.md b/src/Lean/Server/README.md index 87cf342a99..fa51b4b9bf 100644 --- a/src/Lean/Server/README.md +++ b/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 diff --git a/src/Lean/Server/Utils.lean b/src/Lean/Server/Utils.lean index 9550273bab..746adbeb52 100644 --- a/src/Lean/Server/Utils.lean +++ b/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 diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index 81e07ec065..3e7591a11f 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/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; diff --git a/src/Lean/Server/lean4-lsp.el b/src/Lean/Server/lean4-lsp.el index 4ef9fc0c43..c99e236986 100644 --- a/src/Lean/Server/lean4-lsp.el +++ b/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)