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

chore: remove obsolete built-in search path

Browse source
This commit is contained in:
Sebastian Ullrich 2020-05-19 14:54:47 +02:00 • committed by Leonardo de Moura
parent 18a89abbe6
commit dc56eb7a86
1 changed files with 6 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -48,19 +48,13 @@ pure sp
def getBuiltinSearchPath : IO SearchPath := do
appDir ← IO.appDir;
let libDir := appDir ++ pathSep ++ ".." ++ pathSep ++ "src" ++ pathSep ++ "Init";
libDirExists ← IO.isDir libDir;
if libDirExists then do
path ← realPathNormalized libDir;
let installedLibDir := appDir ++ pathSep ++ ".." ++ pathSep ++ "lib" ++ pathSep ++ "lean" ++ pathSep ++ "Init";
installedLibDirExists ← IO.isDir installedLibDir;
if installedLibDirExists then do
path ← realPathNormalized installedLibDir;
pure $ HashMap.empty.insert "Init" path
else do
let installedLibDir := appDir ++ pathSep ++ ".." ++ pathSep ++ "lib" ++ pathSep ++ "lean" ++ pathSep ++ "Init";
installedLibDirExists ← IO.isDir installedLibDir;
if installedLibDirExists then do
path ← realPathNormalized installedLibDir;
pure $ HashMap.empty.insert "Init" path
else
pure ∅
else
pure ∅
def addSearchPathFromEnv (sp : SearchPath) : IO SearchPath := do
val ← IO.getEnv "LEAN_PATH";