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

fix(library/init/lean/path): add support for default.lean

Browse source
This commit is contained in:
Leonardo de Moura 2019-07-31 08:52:55 -07:00
parent 8a4bc188c2
commit a9ba3773c7
1 changed files with 7 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
library/init/lean/path.lean
View file

@ -67,12 +67,14 @@ match path with
curr ← realPathNormalized ".";
setSearchPath [path, curr]
def findFile (fname : String) : IO (Option String) :=
def findFile (fname : String) (ext : String) : IO (Option String) :=
do let fname := System.FilePath.normalizePath fname;
paths ← searchPathRef.get;
paths.mfind $ fun path => do
let path := path ++ pathSep;
let curr := path ++ fname;
let curr := path ++ pathSep ++ fname;
isDir ← IO.isDir curr;
let curr := if isDir then curr ++ pathSep ++ "default" else curr;
let curr := curr ++ toString extSeparator ++ ext;
ex ← IO.fileExists curr;
if ex then pure (some curr) else pure none
@ -88,8 +90,8 @@ def addRel (baseDir : String) : Nat → String
def findLeanFile (modName : Name) (ext : String) : IO String :=
do
let fname := modNameToFileName modName ++ toString extSeparator ++ ext;
some fname ← findFile fname | throw (IO.userError ("module '" ++ toString modName ++ "' not found"));
let fname := modNameToFileName modName;
some fname ← findFile fname ext | throw (IO.userError ("module '" ++ toString modName ++ "' not found"));
realPathNormalized fname
def findOLean (modName : Name) : IO String :=