max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: do not eagerly check and preprocess search paths

Browse source
This commit is contained in:
Sebastian Ullrich 2020-05-23 12:37:24 +02:00
parent b8557b63af
commit 01480e0f66
2 changed files with 7 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/Init/Lean/Util/Path.lean
View file

@ -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";

5
src/lean.mk.in
View file

@ -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