From f13b703285b39e64c1bee7c44377d146ce7df82c Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Fri, 9 Oct 2020 12:40:39 -0400
Subject: [PATCH] chore: re-add 'runWithInputFile' to server

---
 src/Lean/Server/FileWorker.lean | 21 ++++++++++++++++-----
 src/Lean/Server/Watchdog.lean   | 23 +++++++++++++++++------
 2 files changed, 33 insertions(+), 11 deletions(-)

diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index 076cc797a5..9fcc9354ad 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -307,17 +307,28 @@ partial def mainLoop : Unit → ServerM Unit
     mainLoop ()
   | _ => throw (userError "got invalid JSON-RPC message")
 
-def initAndRunWorker (i o : FS.Stream) : IO Unit := do
+def initAndRunWorker (i o e : FS.Stream) : IO Unit := do
 -- TODO(WN): act in accordance with InitializeParams
 _ ← Lsp.readLspRequestAs i "initialize" InitializeParams;
 param ← Lsp.readLspNotificationAs i "textDocument/didOpen" DidOpenTextDocumentParams;
-h ← FS.Handle.mk "fwlog.txt" FS.Mode.write false;
-_ ← IO.setStderr (FS.Stream.ofHandle h);
+_ ← IO.setStderr e; -- TODO(WN): use a stream var in WorkerM instead of global state
 doc ← openDocument o param;
 docRef ← IO.mkRef doc;
 pendingRequestsRef ← IO.mkRef (RBMap.empty : PendingRequestMap);
 runReader (mainLoop ()) (⟨i, o, docRef, pendingRequestsRef⟩ : ServerContext)
 
+namespace Test
+
+def runWorkerWithInputFile (fn : String) (searchPath : Option String) : IO Unit := do
+o ← IO.getStdout;
+e ← IO.getStderr;
+FS.withFile fn FS.Mode.read (fun hFile => do
+  Lean.initSearchPath searchPath;
+  catch
+    (Lean.Server.initAndRunWorker (FS.Stream.ofHandle hFile) o e)
+    (fun err => e.putStrLn $ toString err))
+
+end Test
 end Server
 end Lean
 
@@ -327,6 +338,6 @@ o ← IO.getStdout;
 e ← IO.getStderr;
 Lean.initSearchPath;
 catch
-  (Lean.Server.initAndRunWorker i o)
-  (fun err => e.putStrLn (toString err));
+  (Lean.Server.initAndRunWorker i o e)
+  (fun err => e.putStrLn $ toString err);
 pure 0
diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean
index 3400b55349..81e07ec065 100644
--- a/src/Lean/Server/Watchdog.lean
+++ b/src/Lean/Server/Watchdog.lean
@@ -140,7 +140,7 @@ abbrev FileWorkerMap := RBMap DocumentUri FileWorker (fun a b => Decidable.decid
 
 structure ServerContext :=
 (hIn hOut : FS.Stream)
-(log : FS.Stream)
+(hLog : FS.Stream)
 (fileWorkersRef : IO.Ref FileWorkerMap)
 /- We store these to pass them to workers. -/
 (initParams : InitializeParams)
@@ -162,7 +162,7 @@ def eraseFileWorker (uri : DocumentUri) : ServerM Unit :=
 fun st => st.fileWorkersRef.modify (fun fileWorkers => fileWorkers.erase uri)
 
 def log (msg : String) : ServerM Unit :=
-fun st => st.log.putStrLn msg
+fun st => st.hLog.putStrLn msg
 
 -- TODO: this creates a long-running Task, which should be okay with upcoming API changes.
 partial def fwdMsgAux (fw : FileWorker) (hOut : FS.Stream) : Unit → IO WorkerEvent
@@ -401,7 +401,7 @@ catch
   -- so that we can die in peace
   (fun err => do shutdown; throw err)
 
-def initAndRunWatchdog (i o : FS.Stream) : IO Unit := do
+def initAndRunWatchdog (i o e : FS.Stream) : IO Unit := do
 workerPath ← IO.getEnv "LEAN_WORKER_PATH";
 appDir ← IO.appDir;
 let workerPath := match workerPath with
@@ -415,11 +415,22 @@ writeLspResponse o initRequest.id
     serverInfo? := some { name := "Lean 4 server",
                           version? := "0.0.1" } : InitializeResult };
 
-e ← IO.getStderr;
 runReader
   initAndRunWatchdogAux
   (⟨i, o, e, fileWorkersRef, initRequest.param, workerPath⟩ : ServerContext)
 
+namespace Test
+
+def runWatchdogWithInputFile (fn : String) (searchPath : Option String) : IO Unit := do
+o ← IO.getStdout;
+e ← IO.getStderr;
+FS.withFile fn FS.Mode.read (fun hFile => do
+  Lean.initSearchPath searchPath;
+  catch
+    (Lean.Server.initAndRunWatchdog (FS.Stream.ofHandle hFile) o e)
+    (fun err => e.putStrLn $ toString err))
+
+end Test
 end Server
 end Lean
 
@@ -431,6 +442,6 @@ o ← IO.getStdout;
 e ← IO.getStderr;
 Lean.initSearchPath;
 catch
-  (Lean.Server.initAndRunWatchdog i o)
-  (fun err => e.putStrLn (toString err));
+  (Lean.Server.initAndRunWatchdog i o e)
+  (fun err => e.putStrLn $ toString err);
 pure 0