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;