From 3cdcdac9214528a236c8cdf17e9198802e745215 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 9 Oct 2020 10:44:44 +0200
Subject: [PATCH] feat: infer worker path

---
 src/Init/System/FilePath.lean | 3 +++
 src/Lean/Server/Watchdog.lean | 8 ++++++--
 2 files changed, 9 insertions(+), 2 deletions(-)

diff --git a/src/Init/System/FilePath.lean b/src/Init/System/FilePath.lean
index d6214a5fce..be9b05e7bc 100644
--- a/src/Init/System/FilePath.lean
+++ b/src/Init/System/FilePath.lean
@@ -33,6 +33,9 @@ def splitSearchPath (s : String) : List String :=
 /-- File extension character -/
 def extSeparator : Char := '.'
 
+def exeSuffix : String :=
+if isWindows then ".exe" else ""
+
 /-- Case-insensitive file system -/
 def isCaseInsensitive : Bool := isWindows || isOSX
 
diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean
index b96610197f..3400b55349 100644
--- a/src/Lean/Server/Watchdog.lean
+++ b/src/Lean/Server/Watchdog.lean
@@ -65,6 +65,7 @@ open IO
 open Std (RBMap RBMap.empty)
 open Lsp
 open JsonRpc
+open System.FilePath
 
 structure OpenDocument :=
 (version : Nat)
@@ -401,8 +402,11 @@ catch
   (fun err => do shutdown; throw err)
 
 def initAndRunWatchdog (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.";
+workerPath ← IO.getEnv "LEAN_WORKER_PATH";
+appDir ← IO.appDir;
+let workerPath := match workerPath with
+  | none   => appDir ++ pathSeparator.toString ++ "FileWorker" ++ exeSuffix
+  | some p => p;
 fileWorkersRef ← IO.mkRef (RBMap.empty : FileWorkerMap);
 
 initRequest ← readLspRequestAs i "initialize" InitializeParams;