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

feat(library/init/lean/path): use toLower at normalizePath if file system is case-insensitive

Browse source
This commit is contained in:
Leonardo de Moura 2019-07-28 19:50:01 -07:00
parent 6cf8571e37
commit 378d75b3b4
2 changed files with 14 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -23,7 +23,7 @@ do curr ← IO.realPath ".";
constant searchPathRef : IO.Ref (Array String) := default _
def setSearchPath (s : List String) : IO Unit :=
do s ← s.mmap (fun p => IO.realPath (System.FilePath.normalizePathSeparators p));
do s ← s.mmap (fun p => IO.realPath (System.FilePath.normalizePath p));
searchPathRef.set s.toArray
def setSearchPathFromString (s : String) : IO Unit :=
@ -64,7 +64,7 @@ match path with
setSearchPath [path, curr]
def findFile (fname : String) : IO (Option String) :=
do let fname := System.FilePath.normalizePathSeparators fname;
do let fname := System.FilePath.normalizePath fname;
paths ← searchPathRef.get;
paths.mfind $ fun path => do
let path := path ++ pathSep;
@ -96,7 +96,7 @@ def findLean (modName : Name) : IO String :=
findLeanFile modName "lean"
def findAtSearchPath (fname : String) : IO String :=
do fname ← IO.realPath (System.FilePath.normalizePathSeparators fname);
do fname ← IO.realPath (System.FilePath.normalizePath fname);
paths ← searchPathRef.get;
match paths.find (fun path => if path.isPrefixOf fname then some path else none) with
| some r => pure r
@ -106,7 +106,7 @@ do fname ← IO.realPath (System.FilePath.normalizePathSeparators fname);
def moduleNameOfFileName (fname : String) : IO Name :=
do
path ← findAtSearchPath fname;
fname ← IO.realPath (System.FilePath.normalizePathSeparators fname);
fname ← IO.realPath (System.FilePath.normalizePath fname);
let fnameSuffix := fname.drop path.length;
let fnameSuffix := if fnameSuffix.get 0 == pathSeparator then fnameSuffix.drop 1 else fnameSuffix;
if path ++ pathSep ++ fnameSuffix != fname then

14
library/init/system/filepath.lean
View file

@ -27,13 +27,19 @@ if isWindows then ';' else ':'
def extSeparator : Char :=
'.'
def normalizePathSeparators (fname : String) : String :=
if pathSeparators.length == 1 then fname
/-- Case-insensitive file system -/
def isCaseInsensitive : Bool :=
isWindows || isOSX
def normalizePath (fname : String) : String :=
if pathSeparators.length == 1 && !isCaseInsensitive then fname
else fname.map (fun c =>
if pathSeparators.any (fun c' => c == c') then pathSeparator else c)
if pathSeparators.any (fun c' => c == c') then pathSeparator
else if isCaseInsensitive then c.toLower
else c)
def dirName (fname : String) : String :=
let fname := normalizePathSeparators fname;
let fname := normalizePath fname;
match fname.revPosOf pathSeparator with
| none => "."
| some pos => { Substring . str := fname, startPos := 0, stopPos := pos }.toString