From a9ba3773c740eb2dbf2eb9bc2c6cd63e0815ba14 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 31 Jul 2019 08:52:55 -0700 Subject: [PATCH] fix(library/init/lean/path): add support for `default.lean` --- library/init/lean/path.lean | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/library/init/lean/path.lean b/library/init/lean/path.lean index b8d184ba0f..00afc8ec6a 100644 --- a/library/init/lean/path.lean +++ b/library/init/lean/path.lean @@ -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 :=