feat: add emptyEnv and add initSearchPath temporarily so that server binary finds LEAN_PATH

src/Lean/Data/Lsp/Communication.lean

@@ -58,9 +58,7 @@ def writeLspMessage (h : FS.Handle) (m : Message) : IO Unit := do
 let j := (toJson m).compress;
 let header := "Content-Length: " ++ toString j.utf8ByteSize ++ "\r\n\r\n";
 h.putStr (header ++ j);
---IO.println "starting to flush now";
 h.flush
---IO.println "flushed";
 
 def writeLspResponse {α : Type*} [Lean.HasToJson α] (h : FS.Handle) (id : RequestID) (r : α) : IO Unit :=
 writeLspMessage h (Message.response id (toJson r))

src/Lean/Server/Server.lean

@@ -33,8 +33,8 @@ match @fromJson? paramType _ params with
 
 def runFrontend (text : String) : IO (Environment × Environment × MessageLog) := do
 let inputCtx := Parser.mkInputContext text "<input>";
-envNul ← mkEmptyEnvironment;
-match Parser.parseHeader envNul inputCtx with
+emptyEnv ← mkEmptyEnvironment;
+match Parser.parseHeader emptyEnv inputCtx with
 | (header, parserState, messages) => do
   (env, messages) ← processHeader header messages inputCtx;
   parserStateRef ← IO.mkRef parserState;
@@ -180,5 +180,6 @@ end Lean.Server
 def main (n : List String) : IO UInt32 := do
 i ← IO.stdin;
 o ← IO.stdout;
+Lean.initSearchPath;
 catch (Lean.Server.initialize i o) (fun err => o.putStrLn (toString err));
 pure 0

src/Lean/Server/test.py

@@ -3,8 +3,7 @@ from concurrent.futures import ThreadPoolExecutor
 from json import dumps
 import re
 
-text = """
-prelude
+text = """prelude
 import Lean.Environment
 import Lean.Elab.Frontend
 import Lean.Data.Lsp
@@ -141,7 +140,8 @@ end Lean.Server
 def main (n : List String) : IO UInt32 := do
 i ← IO.stdin;
 o ← IO.stdout;
-Lean.Server.initialize i o -- intentional error to test diagnostics
+Lean.initSearchPath;
+Lean.Server.initialize i o; -- intentional error to test diagnostics
 pure 0
 """
 
@@ -180,6 +180,4 @@ send(initialized)
 print("sending open1")
 send(open1)
 read()
-read()
-read()
 print(p.wait())