diff --git a/src/Init/Lean/Util/Path.lean b/src/Init/Lean/Util/Path.lean index 5e132a4bf7..7477de7844 100644 --- a/src/Init/Lean/Util/Path.lean +++ b/src/Init/Lean/Util/Path.lean @@ -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";