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

feat: generalise SearchPath lookup

Browse source
This commit is contained in:
Wojciech Nawrocki 2021-01-18 15:49:17 -05:00 • committed by Leonardo de Moura
parent 31ed0621c7
commit f252a47bbb
1 changed files with 22 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

35
src/Lean/Util/Path.lean
View file

@ -18,15 +18,32 @@ def realPathNormalized (fname : String) : IO String := do
let fname ← IO.realPath fname
pure (System.FilePath.normalizePath fname)
def modPathToFilePath : Name → String
| Name.str p h _ => modPathToFilePath p ++ pathSep ++ h
| Name.anonymous => ""
| Name.num p _ _ => panic! "ill-formed import"
abbrev SearchPath := List String
namespace SearchPath
/-- Finds the file with extension `ext` (`.lean` or `.olean`) corresponding to `mod`
in the given search path. -/
def findWithExt (sp : SearchPath) (mod : Name) (ext : String) : IO String := do
let pkg := mod.getRoot.toString
let some root ← sp.findM? (fun path => IO.isDir s!"{path}{pathSep}{pkg}" <||> IO.fileExists s!"{path}{pathSep}{pkg}{ext}")
| throw $ IO.userError $ "unknown package '" ++ pkg ++ "'"
pure $ root ++ modPathToFilePath mod ++ ext
end SearchPath
builtin_initialize searchPathRef : IO.Ref SearchPath ← IO.mkRef {}
def parseSearchPath (path : String) (sp : SearchPath := ∅) : IO SearchPath :=
pure $ System.FilePath.splitSearchPath path ++ sp
def parseSearchPath (path : String) (sp : SearchPath := ∅) : SearchPath :=
System.FilePath.splitSearchPath path ++ sp
@[extern c inline "LEAN_IS_STAGE0"]
constant isStage0 (u : Unit) : Bool
private constant isStage0 (u : Unit) : Bool
def getBuiltinSearchPath : IO SearchPath := do
let appDir ← IO.appDir
@ -42,23 +59,15 @@ def addSearchPathFromEnv (sp : SearchPath) : IO SearchPath := do
@[export lean_init_search_path]
def initSearchPath (path : Option String := none) : IO Unit :=
match path with
| some path => parseSearchPath path >>= searchPathRef.set
| some path => searchPathRef.set <| parseSearchPath path
| none => do
let sp ← getBuiltinSearchPath
let sp ← addSearchPathFromEnv sp
searchPathRef.set sp
def modPathToFilePath : Name → String
| Name.str p h _ => modPathToFilePath p ++ pathSep ++ h
| Name.anonymous => ""
| Name.num p _ _ => panic! "ill-formed import"
def findOLean (mod : Name) : IO String := do
let sp ← searchPathRef.get
let pkg := mod.getRoot.toString
let some root ← sp.findM? (fun path => IO.isDir s!"{path}{pathSep}{pkg}" <||> IO.fileExists s!"{path}{pathSep}{pkg}.olean")
| throw $ IO.userError $ "unknown package '" ++ pkg ++ "'"
pure $ root ++ modPathToFilePath mod ++ ".olean"
sp.findWithExt mod ".olean"
/-- Infer module name of source file name. -/
@[export lean_module_name_of_file]