diff --git a/src/Lean/Data/Lsp/Communication.lean b/src/Lean/Data/Lsp/Communication.lean
index 5f803e7563..5cd50af621 100644
--- a/src/Lean/Data/Lsp/Communication.lean
+++ b/src/Lean/Data/Lsp/Communication.lean
@@ -19,12 +19,12 @@ private def parseHeaderField (s : String) : Option (String × String) :=
   if s = "" ∨ s.takeRight 2 ≠ "\r\n" then
     none
   else
-    let xs := (s.dropRight 2).splitOn ": ";
+    let xs := (s.dropRight 2).splitOn ": "
     match xs with
     | []  => none
     | [_] => none
     | name :: value :: rest =>
-      let value := ": ".intercalate (value :: rest);
+      let value := ": ".intercalate (value :: rest)
       some ⟨name, value⟩
 
 private partial def readHeaderFields (h : FS.Stream) : IO (List (String × String)) := do
@@ -47,36 +47,38 @@ private def readLspHeader (h : FS.Stream) : IO Nat := do
     | none   => throw (userError ("Content-Length header value '" ++ length ++ "' is not a Nat"))
   | none => throw (userError ("no Content-Length header in header fields: " ++ toString fields))
 
-def readLspMessage (h : FS.Stream) : IO Message := do
+variables {m : Type → Type} [Monad m] [MonadIO m]
+
+def readLspMessage (h : FS.Stream) : m Message := do
   let nBytes ← readLspHeader h
   h.readMessage nBytes
 
-def readLspRequestAs (h : FS.Stream) (expectedMethod : String) (α : Type) [FromJson α] : IO (Request α) := do
+def readLspRequestAs (h : FS.Stream) (expectedMethod : String) (α : Type) [FromJson α] : m (Request α) := do
   let nBytes ← readLspHeader h
   h.readRequestAs nBytes expectedMethod α
 
-def readLspNotificationAs (h : FS.Stream) (expectedMethod : String) (α : Type) [FromJson α] : IO α := do
+def readLspNotificationAs (h : FS.Stream) (expectedMethod : String) (α : Type) [FromJson α] : m α := do
   let nBytes ← readLspHeader h
   h.readNotificationAs nBytes expectedMethod α
 
-def writeLspMessage (h : FS.Stream) (m : Message) : IO Unit := do
+def writeLspMessage (h : FS.Stream) (msg : Message) : m Unit := do
   -- inlined implementation instead of using jsonrpc's writeMessage
   -- to maintain the atomicity of putStr
-  let j := (toJson m).compress
+  let j := (toJson msg).compress
   let header := "Content-Length: " ++ toString j.utf8ByteSize ++ "\r\n\r\n"
   h.putStr (header ++ j)
   h.flush
 
-def writeLspRequest {α : Type} [ToJson α] (h : FS.Stream) (id : RequestID) (method : String) (params : α) : IO Unit :=
+def writeLspRequest {α : Type} [ToJson α] (h : FS.Stream) (id : RequestID) (method : String) (params : α) : m Unit :=
   writeLspMessage h (Message.request id method (fromJson? (toJson params)))
 
-def writeLspNotification {α : Type} [ToJson α] (h : FS.Stream) (method : String) (r : α) : IO Unit :=
+def writeLspNotification {α : Type} [ToJson α] (h : FS.Stream) (method : String) (r : α) : m Unit :=
   writeLspMessage h (Message.notification method (fromJson? (toJson r)))
 
-def writeLspResponse {α : Type} [ToJson α] (h : FS.Stream) (id : RequestID) (r : α) : IO Unit :=
+def writeLspResponse {α : Type} [ToJson α] (h : FS.Stream) (id : RequestID) (r : α) : m Unit :=
   writeLspMessage h (Message.response id (toJson r))
 
-def writeLspResponseError {α : Type} [ToJson α] (h : FS.Stream) (id : RequestID) (code : ErrorCode) (message : String) (data : α) : IO Unit :=
+def writeLspResponseError {α : Type} [ToJson α] (h : FS.Stream) (id : RequestID) (code : ErrorCode) (message : String) (data : α) : m Unit :=
   writeLspMessage h (Message.responseError id code message (toJson data))
 
 end Lsp
diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index 048170339f..eda90fadd9 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -9,6 +9,7 @@ import Std.Data.RBMap
 
 import Lean.Environment
 import Lean.Server.Snapshots
+import Lean.Server.Utils
 import Lean.Data.Lsp
 import Lean.Data.Json.FromToJson
 
@@ -187,25 +188,11 @@ fun st => st.docRef.get
 def updatePendingRequests (map : Array (Task (Except IO.Error Unit)) → Array (Task (Except IO.Error Unit))) : ServerM Unit :=
 fun st => st.pendingRequestsRef.modify map
 
-def readLspMessage : ServerM JsonRpc.Message :=
-fun st => monadLift $ readLspMessage st.hIn
-
-def readLspRequestAs (expectedMethod : String) (α : Type*) [HasFromJson α] : ServerM (Request α) :=
-fun st => monadLift $ readLspRequestAs st.hIn expectedMethod α
-
-def readLspNotificationAs (expectedMethod : String) (α : Type*) [HasFromJson α] : ServerM α :=
-fun st => monadLift $ readLspNotificationAs st.hIn expectedMethod α
-
-def writeLspNotification {α : Type*} [HasToJson α] (method : String) (params : α) : ServerM Unit :=
-fun st => monadLift $ writeLspNotification st.hOut method params
-
-def writeLspResponse {α : Type*} [HasToJson α] (id : RequestID) (params : α) : ServerM Unit :=
-fun st => monadLift $ writeLspResponse st.hOut id params
-
 /-- Clears diagnostics for the document version 'version'. -/
 -- TODO(WN): how to clear all diagnostics? Sending version 'none' doesn't seem to work
 def clearDiagnostics (uri : DocumentUri) (version : Nat) : ServerM Unit :=
-writeLspNotification "textDocument/publishDiagnostics"
+fun st =>
+writeLspNotification st.hOut "textDocument/publishDiagnostics"
   { uri := uri,
     version? := version,
     diagnostics := #[] : PublishDiagnosticsParams }
@@ -225,13 +212,6 @@ let text := doc.text.toFileMap;
 newDoc ← compileDocument h doc.uri doc.version text;
 pure newDoc
 
-private def replaceLspRange (text : FileMap) (r : Lsp.Range) (newText : String) : FileMap :=
-let start := text.lspPosToUtf8Pos r.start;
-let «end» := text.lspPosToUtf8Pos r.«end»;
-let pre := text.source.extract 0 start;
-let post := text.source.extract «end» text.source.bsize;
-(pre ++ newText ++ post).toFileMap
-
 def handleDidChange (p : DidChangeTextDocumentParams) : ServerM Unit := do
 let docId := p.textDocument;
 let changes := p.contentChanges;
@@ -292,8 +272,9 @@ match method with
 
 partial def mainLoop : Unit → ServerM Unit
 | () => do
+  st ← read;
   -- TODO(MH): gracefully terminate when stdin is closed by watchdog?
-  msg ← readLspMessage;
+  msg ← readLspMessage st.hIn;
   -- TODO(MH): updatePendingRequests ...: get rid of all requests that are finished
   match msg with
   | Message.request id method (some params) => do
@@ -304,9 +285,9 @@ partial def mainLoop : Unit → ServerM Unit
     mainLoop ()
   | _ => throw (userError "got invalid JSON-RPC message")
 
-def initAndRunServer (i o : FS.Stream) : IO Unit := do
--- ignore InitializeParams for MWE
-initRequest ← Lsp.readLspRequestAs i "initialize" InitializeParams;
+def initAndRunWorker (i o : FS.Stream) : IO Unit := do
+-- TODO(WN): act in accordance with InitializeParams
+_ ← Lsp.readLspRequestAs i "initialize" InitializeParams;
 docRequest ← Lsp.readLspRequestAs i "textDocument/didOpen" DidOpenTextDocumentParams;
 doc ← openDocument o docRequest.param;
 docRef ← IO.mkRef doc;
@@ -315,3 +296,8 @@ runReader (mainLoop ()) (⟨i, o, docRef, pendingRequestsRef⟩ : ServerContext)
 
 end Server
 end Lean
+
+def main : IO Unit := do
+hIn ← IO.getStdin;
+hOut ← IO.getStdout;
+Lean.Server.initAndRunWorker hIn hOut
diff --git a/src/Lean/Server/Utils.lean b/src/Lean/Server/Utils.lean
new file mode 100644
index 0000000000..90ce53015d
--- /dev/null
+++ b/src/Lean/Server/Utils.lean
@@ -0,0 +1,15 @@
+import Lean.Data.Position
+import Lean.Data.Lsp
+
+namespace Lean
+namespace Server
+
+def replaceLspRange (text : FileMap) (r : Lsp.Range) (newText : String) : FileMap :=
+let start := text.lspPosToUtf8Pos r.start;
+let «end» := text.lspPosToUtf8Pos r.«end»;
+let pre := text.source.extract 0 start;
+let post := text.source.extract «end» text.source.bsize;
+(pre ++ newText ++ post).toFileMap
+
+end Server
+end Lean
diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean
index 93c0adb925..883841490b 100644
--- a/src/Lean/Server/Watchdog.lean
+++ b/src/Lean/Server/Watchdog.lean
@@ -11,6 +11,7 @@ import Lean.Elab.Import
 
 import Lean.Data.Lsp
 import Lean.Server.HasFileSource
+import Lean.Server.Utils
 
 /-!
 For general server architecture, see `README.md`. This module implements the watchdog process.
@@ -63,21 +64,7 @@ open Std (RBMap RBMap.empty)
 open Lsp
 open JsonRpc
 
-private def replaceLspRange (text : FileMap) (r : Lsp.Range) (newText : String) : FileMap :=
-let start := text.lspPosToUtf8Pos r.start;
-let «end» := text.lspPosToUtf8Pos r.«end»;
-let pre := text.source.extract 0 start;
-let post := text.source.extract «end» text.source.bsize;
-(pre ++ newText ++ post).toFileMap
-
-private def parsedImportsEndPos (input : String) : IO String.Pos := do
-env ← mkEmptyEnvironment;
-let fileName := "<input>";
-let inputCtx := Parser.mkInputContext input fileName;
-let (_, parserState, _) := Parser.parseHeader env inputCtx;
-pure parserState.pos
-
-structure EditableDocument :=
+structure OpenDocument :=
 (version : Nat)
 (text : FileMap)
 (headerEndPos : String.Pos)
@@ -85,17 +72,11 @@ structure EditableDocument :=
 def workerCfg : Process.StdioConfig := ⟨Process.Stdio.piped, Process.Stdio.piped, Process.Stdio.piped⟩
 
 structure FileWorker :=
-(doc : EditableDocument)
+(doc : OpenDocument)
 (proc : Process.Child workerCfg)
 
 namespace FileWorker
 
-def spawnArgs : Process.SpawnArgs := {workerCfg with cmd := "fileworker"}
-
-def spawn (doc : EditableDocument) : IO FileWorker := do
-proc ← Process.spawn spawnArgs;
-pure ⟨doc, proc⟩
-
 def stdin (fw : FileWorker) : FS.Stream :=
 FS.Stream.ofHandle fw.proc.stdin
 
@@ -105,7 +86,7 @@ FS.Stream.ofHandle fw.proc.stdout
 def stderr (fw : FileWorker) : FS.Stream :=
 FS.Stream.ofHandle fw.proc.stderr
 
-def wait (w : FileWorker) : IO Nat := pure 0
+def wait (fw : FileWorker) : IO Nat := pure 0 -- TODO
 
 end FileWorker
 
@@ -114,69 +95,26 @@ abbrev FileWorkerMap := RBMap DocumentUri FileWorker (fun a b => Decidable.decid
 structure ServerContext :=
 (hIn hOut : FS.Stream)
 (fileWorkersRef : IO.Ref FileWorkerMap)
+/- We store these to pass them to workers. -/
 (initParams : InitializeParams)
+(workerPath : String)
 
 abbrev ServerM := ReaderT ServerContext IO
 
-def updateFileWorkers (key : DocumentUri) (val : FileWorker) : ServerM Unit :=
-fun st => st.fileWorkersRef.modify (fun fileWorkers => fileWorkers.insert key val)
+def spawnFileWorker (doc : OpenDocument) : ServerM FileWorker :=
+fun st => do
+  proc ← Process.spawn {workerCfg with cmd := st.workerPath};
+  pure ⟨doc, proc⟩
 
-def findFileWorker (key : DocumentUri) : ServerM FileWorker :=
+def updateFileWorkers (uri : DocumentUri) (val : FileWorker) : ServerM Unit :=
+fun st => st.fileWorkersRef.modify (fun fileWorkers => fileWorkers.insert uri val)
+
+def findFileWorker (uri : DocumentUri) : ServerM FileWorker :=
 fun st => do
 fileWorkers ← st.fileWorkersRef.get;
-match fileWorkers.find? key with
+match fileWorkers.find? uri with
 | some fw => pure fw
-| none    => throw (userError $ "got unknown document URI (" ++ key ++ ")")
-
-def readWorkerLspMessage (key : DocumentUri) : ServerM JsonRpc.Message :=
-findFileWorker key >>= fun fw => monadLift $ readLspMessage fw.stdout
-
-def readUserLspMessage : ServerM JsonRpc.Message :=
-fun st => monadLift $ readLspMessage st.hIn
-
-def readWorkerLspRequestAs (key : DocumentUri) (expectedMethod : String) (α : Type*) [HasFromJson α] : ServerM (Request α) :=
-findFileWorker key >>= fun fw => monadLift $ readLspRequestAs fw.stdout expectedMethod α
-
-def readUserLspRequestAs (expectedMethod : String) (α : Type*) [HasFromJson α] : ServerM (Request α) :=
-fun st => monadLift $ readLspRequestAs st.hIn expectedMethod α
-
-def readWorkerLspNotificationAs (key : DocumentUri) (expectedMethod : String) (α : Type*) [HasFromJson α] : ServerM α :=
-findFileWorker key >>= fun fw => monadLift $ readLspNotificationAs fw.stdout expectedMethod α
-
-def readUserLspNotificationAs (expectedMethod : String) (α : Type*) [HasFromJson α] : ServerM α :=
-fun st => monadLift $ readLspNotificationAs st.hIn expectedMethod α
-
-def writeWorkerLspMessage (key : DocumentUri) (msg : JsonRpc.Message) : ServerM Unit :=
-findFileWorker key >>= fun fw => monadLift $ writeLspMessage fw.stdin msg
-
-def writeUserLspMessage (msg : JsonRpc.Message) : ServerM Unit :=
-fun st => monadLift $ writeLspMessage st.hOut msg
-
-def writeWorkerLspRequest {α : Type*} [HasToJson α] (key : DocumentUri) (id : RequestID) (method : String) (params : α) : ServerM Unit :=
-findFileWorker key >>= fun fw => monadLift $ writeLspRequest fw.stdin id method params
-
-def writeUserLspRequest {α : Type*} [HasToJson α] (id : RequestID) (method : String) (params : α) : ServerM Unit :=
-fun st => monadLift $ writeLspRequest st.hOut id method params
-
-def writeWorkerLspNotification {α : Type*} [HasToJson α] (key : DocumentUri) (method : String) (params : α) : ServerM Unit :=
-findFileWorker key >>= fun fw => monadLift $ writeLspNotification fw.stdin method params
-
-def writeUserLspNotification {α : Type*} [HasToJson α] (method : String) (params : α) : ServerM Unit :=
-fun st => monadLift $ writeLspNotification st.hOut method params
-
-def writeWorkerLspResponse {α : Type*} [HasToJson α] (key : DocumentUri) (id : RequestID) (params : α) : ServerM Unit :=
-findFileWorker key >>= fun fw => monadLift $ writeLspResponse fw.stdin id params
-
-def writeUserLspResponse {α : Type*} [HasToJson α] (id : RequestID) (params : α) : ServerM Unit :=
-fun st => monadLift $ writeLspResponse st.hOut id params
-
-def writeWorkerInitializeParams (key : DocumentUri) : ServerM Unit := do
-st ← read;
-writeWorkerLspRequest key (0 : Nat) "initialize" st.initParams
-
-def writeWorkerDidOpenNotification (key : DocumentUri) : ServerM Unit := do
-findFileWorker key >>= fun fw => writeWorkerLspNotification key "textDocument/didOpen"
-  (DidOpenTextDocumentParams.mk ⟨key, "lean", fw.doc.version, fw.doc.text.source⟩)
+| none    => throw (userError $ "got unknown document URI (" ++ uri ++ ")")
 
 def parseParams (paramType : Type*) [HasFromJson paramType] (params : Json) : ServerM paramType :=
 match fromJson? params with
@@ -190,17 +128,24 @@ partial def forwardFileWorkerPackets (fw : FileWorker) : Unit → ServerM Unit
 | ⟨⟩ => do
   -- TODO(MH): detect closed stream somehow and terminate gracefully
   -- TODO(MH): potentially catch unintended termination (e.g. due to stack overflow) and restart process
-  msg ← monadLift $ readLspMessage fw.stdout;
-  -- NOTE: Writes to Lean I/O streams are atomic, so we don't need to synchronise these in principle.
-  writeUserLspMessage msg;
+  msg ← readLspMessage fw.stdout;
+  writeLspMessage fw.stdin msg;
   forwardFileWorkerPackets ⟨⟩
 
-def startFileWorker (key : DocumentUri) (version : Nat) (text : FileMap) : ServerM Unit := do
+private def parsedImportsEndPos (input : String) : IO String.Pos := do
+emptyEnv ← mkEmptyEnvironment; -- TODO(WN): a lot of things could be purified if `mkEmptyEnvironment` was just a pure ctr
+let inputCtx := Parser.mkInputContext input "<input>";
+let (_, parserState, _) := Parser.parseHeader emptyEnv inputCtx;
+pure parserState.pos
+
+def startFileWorker (uri : DocumentUri) (version : Nat) (text : FileMap) : ServerM Unit := do
+st ← read;
 pos ← monadLift $ parsedImportsEndPos text.source;
-fw ← monadLift $ FileWorker.spawn ⟨version, text, pos⟩;
-updateFileWorkers key fw;
-writeWorkerInitializeParams key;
-writeWorkerDidOpenNotification key;
+fw ← spawnFileWorker ⟨version, text, pos⟩;
+writeLspRequest fw.stdin (0 : Nat) "initialize" st.initParams;
+writeLspNotification fw.stdin "textDocument/didOpen"
+  (DidOpenTextDocumentParams.mk ⟨uri, "lean", fw.doc.version, fw.doc.text.source⟩);
+updateFileWorkers uri fw;
 -- TODO(MH): replace with working IO variant
 -- TODO(MH): Sebastian said something about this better being implemented as threads
 -- (due to the long running nature of these tasks) but i did not yet have time to
@@ -242,9 +187,9 @@ else changes.forM $ fun change =>
       terminateFileWorker fw;
       startFileWorker doc.uri newVersion newDocText
     else
-      let newDoc : EditableDocument := ⟨newVersion, newDocText, oldHeaderEndPos⟩;
+      let newDoc : OpenDocument := ⟨newVersion, newDocText, oldHeaderEndPos⟩;
       updateFileWorkers doc.uri { fw with doc := newDoc };
-      writeWorkerLspNotification doc.uri "textDocument/didChange" p
+      writeLspNotification fw.stdin "textDocument/didChange" p
   | TextDocumentContentChangeEvent.fullChange (text : String) =>
     throw (userError "TODO impl computing the diff of two sources.")
 
@@ -258,7 +203,8 @@ st.fileWorkersRef.modify (fun fileWorkers => fileWorkers.erase doc.uri)
 def handleRequest (id : RequestID) (method : String) (params : Json) : ServerM Unit := do
 let h := (fun α [HasFromJson α] [HasToJson α] [HasFileSource α] => do
            parsedParams ← parseParams α params;
-           writeWorkerLspRequest (fileSource parsedParams) id method parsedParams);
+           fw ← findFileWorker $ fileSource parsedParams;
+           writeLspRequest fw.stdin id method parsedParams);
 match method with
 | "textDocument/hover" => h HoverParams
 | _ => throw (userError $ "got unsupported request: " ++ method ++
@@ -267,7 +213,8 @@ match method with
 def handleNotification (method : String) (params : Json) : ServerM Unit := do
 let forward := (fun α [HasFromJson α] [HasToJson α] [HasFileSource α] => do
            parsedParams ← parseParams α params;
-           writeWorkerLspNotification (fileSource parsedParams) method parsedParams);
+           fw ← findFileWorker $ fileSource parsedParams;
+           writeLspNotification fw.stdin method parsedParams);
 let handle := (fun α [HasFromJson α] (handler : α → ServerM Unit) => parseParams α params >>= handler);
 match method with
 | "textDocument/didOpen"   => handle DidOpenTextDocumentParams handleDidOpen
@@ -278,10 +225,11 @@ match method with
 
 partial def mainLoop : Unit → ServerM Unit
 | () => do
-  msg ← readUserLspMessage;
+  st ← read;
+  msg ← readLspMessage st.hIn;
   match msg with
   | Message.request id "shutdown" _ =>
-    writeUserLspResponse id (Json.null)
+    writeLspResponse st.hOut id (Json.null)
   | Message.request id method (some params) => do
     handleRequest id method (toJson params);
     mainLoop ()
@@ -299,22 +247,26 @@ def mkLeanServerCapabilities : ServerCapabilities :=
     save? := none },
   hoverProvider := true }
 
+def initAndRunServerAux : ServerM Unit := do
+st ← read;
+_ ← readLspNotificationAs st.hIn "initialized" InitializedParams;
+mainLoop ();
+Message.notification "exit" none ← readLspMessage st.hIn
+  | throw (userError "Expected an Exit Notification.");
+pure ()
+
 def initAndRunServer (i o : FS.Stream) : IO Unit := do
+some workerPath ← IO.getEnv "LEAN_WORKER_PATH"
+  | throw $ userError "You need to specify LEAN_WORKER_PATH in the environment.";
 fileWorkersRef ← IO.mkRef (RBMap.empty : FileWorkerMap);
--- ignore InitializeParams for MWE
 initRequest ← readLspRequestAs i "initialize" InitializeParams;
+writeLspResponse o initRequest.id
+  { capabilities := mkLeanServerCapabilities,
+    serverInfo? := some { name := "Lean 4 server",
+                          version? := "0.0.1" } : InitializeResult };
 runReader
-  (do
-    writeUserLspResponse initRequest.id
-      { capabilities := mkLeanServerCapabilities,
-        serverInfo? := some { name := "Lean 4 server",
-                              version? := "0.0.1" } : InitializeResult };
-    _ ← readUserLspNotificationAs "initialized" InitializedParams;
-    mainLoop ();
-    Message.notification "exit" none ← readUserLspMessage
-      | throw (userError "Expected an Exit Notification.");
-    pure ())
-  (⟨i, o, fileWorkersRef, initRequest.param⟩ : ServerContext)
+  initAndRunServerAux
+  (⟨i, o, fileWorkersRef, initRequest.param, workerPath⟩ : ServerContext)
 
 end Server
 end Lean