From c5abab8fd2e725738e0ece79d234f2deae71461e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 4 Aug 2019 08:38:48 -0700 Subject: [PATCH] fix(library/init/lean/path): `/.lean` must have precedence over `//default.lean` --- library/init/lean/path.lean | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/library/init/lean/path.lean b/library/init/lean/path.lean index 43d407b957..d4fa3f2d99 100644 --- a/library/init/lean/path.lean +++ b/library/init/lean/path.lean @@ -65,15 +65,18 @@ match path with setSearchPath (pathEnv ++ builtinPath) def findFile (fname : String) (ext : String) : IO (Option String) := +let checkFile (curr : String) : IO (Option String) := do { + ex ← IO.fileExists curr; + if ex then pure (some curr) else pure none +}; do let fname := System.FilePath.normalizePath fname; paths ← searchPathRef.get; paths.mfind $ fun path => do 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 + result ← checkFile (curr ++ toString extSeparator ++ ext); + match result with + | none => checkFile (curr ++ pathSep ++ "default" ++ toString extSeparator ++ ext) + | other => pure other def modNameToFileName : Name → String | (Name.mkString Name.anonymous h) := h