From 01480e0f66ebbd8d0913bcb9d54ebdf170d9d26a Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sat, 23 May 2020 12:37:24 +0200
Subject: [PATCH] fix: do not eagerly check and preprocess search paths

---
 src/Init/Lean/Util/Path.lean | 20 +++++---------------
 src/lean.mk.in               |  5 ++---
 2 files changed, 7 insertions(+), 18 deletions(-)

diff --git a/src/Init/Lean/Util/Path.lean b/src/Init/Lean/Util/Path.lean
index e3e0060e12..4c0fd46c5c 100644
--- a/src/Init/Lean/Util/Path.lean
+++ b/src/Init/Lean/Util/Path.lean
@@ -36,27 +36,17 @@ constant searchPathRef : IO.Ref SearchPath := arbitrary _
 def parseSearchPath (path : String) (sp : SearchPath := ∅) : IO SearchPath := do
 let ps := System.FilePath.splitSearchPath path;
 sp ← ps.foldlM (fun (sp : SearchPath) s => match s.splitOn "=" with
-  | [pkg, path] => do
-    condM (IO.isDir path)
-      (pure $ sp.insert pkg path)
-      (throw $ IO.userError $ "invalid search path, '" ++ path ++ "' is not a directory")
+  | [pkg, path] => pure $ sp.insert pkg path
   | _           => throw $ IO.userError $ "ill-formed search path entry '" ++ s ++ "', should be of form 'pkg=path'")
   sp;
 pure sp
 
 def getBuiltinSearchPath : IO SearchPath := do
 appDir ← IO.appDir;
-let installedLibDir := appDir ++ pathSep ++ ".." ++ pathSep ++ "lib" ++ pathSep ++ "lean" ++ pathSep ++ "Init";
-installedLibDirExists ← IO.isDir installedLibDir;
-if installedLibDirExists then do
-  initPath ← realPathNormalized installedLibDir;
-  let map := HashMap.empty.insert "Init" initPath;
-  -- let stdDir := appDir ++ pathSep ++ ".." ++ pathSep ++ "lib" ++ pathSep ++ "lean" ++ pathSep ++ "Std";
-  -- stdPath ← realPathNormalized stdDir;
-  -- let map := map.insert "Std" stdPath;
-  pure map
-else
-  pure ∅
+let map := HashMap.empty;
+let map := map.insert "Init" $ appDir ++ pathSep ++ ".." ++ pathSep ++ "lib" ++ pathSep ++ "lean" ++ pathSep ++ "Init";
+let map := map.insert "Std" $ appDir ++ pathSep ++ ".." ++ pathSep ++ "lib" ++ pathSep ++ "lean" ++ pathSep ++ "Std";
+pure map
 
 def addSearchPathFromEnv (sp : SearchPath) : IO SearchPath := do
 val ← IO.getEnv "LEAN_PATH";
diff --git a/src/lean.mk.in b/src/lean.mk.in
index ef44f535db..0eff6c270c 100644
--- a/src/lean.mk.in
+++ b/src/lean.mk.in
@@ -28,11 +28,10 @@ lib: $(LIB_OUT)/$(STATIC_LIB_NAME)
 
 depends: $(DEPS)
 
-# `lean --deps` complains if the `LEAN_PATH` doesn't point at anything
-$(OLEAN_OUT)/$(PKG) $(LIB_OUT) $(BIN_OUT):
+$(LIB_OUT) $(BIN_OUT):
 	@mkdir -p "$@"
 
-$(TEMP_OUT)/%.depend: %.lean | $(OLEAN_OUT)/$(PKG)
+$(TEMP_OUT)/%.depend: %.lean
 	@mkdir -p "$(TEMP_OUT)/$(*D)"
 # use separate assignment to ensure failure propagation
 # convert path separators and newlines on Windows