From df84536315f90cf9d60fe49ecc247b837387a43c Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 1 Aug 2024 15:39:27 +0200 Subject: [PATCH] Revert "fix: make import resolution case-sensitive on all platforms (#4538)" This reverts commit d5a8c9647f197e8fec626aadd4e548a0d5391809. --- src/Lean/Elab/Import.lean | 2 +- src/Lean/Environment.lean | 2 + src/Lean/Util/Path.lean | 53 ++++----------------- src/lake/Lake/Build/Module.lean | 3 -- tests/pkg/import-case/.gitignore | 1 - tests/pkg/import-case/ImportCase.lean | 2 - tests/pkg/import-case/ImportCase/Basic.lean | 1 - tests/pkg/import-case/lakefile.toml | 5 -- tests/pkg/import-case/test.sh | 5 -- 9 files changed, 12 insertions(+), 62 deletions(-) delete mode 100644 tests/pkg/import-case/.gitignore delete mode 100644 tests/pkg/import-case/ImportCase.lean delete mode 100644 tests/pkg/import-case/ImportCase/Basic.lean delete mode 100644 tests/pkg/import-case/lakefile.toml delete mode 100755 tests/pkg/import-case/test.sh diff --git a/src/Lean/Elab/Import.lean b/src/Lean/Elab/Import.lean index aff17800c028..88a013c49040 100644 --- a/src/Lean/Elab/Import.lean +++ b/src/Lean/Elab/Import.lean @@ -39,7 +39,7 @@ def parseImports (input : String) (fileName : Option String := none) : IO (Array def printImports (input : String) (fileName : Option String) : IO Unit := do let (deps, _, _) ← parseImports input fileName for dep in deps do - let fname ← findOLean (checkExists := false) dep.module + let fname ← findOLean dep.module IO.println fname end Lean.Elab diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 5d16c12d12a1..4055bc296fee 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -806,6 +806,8 @@ partial def importModulesCore (imports : Array Import) : ImportStateM Unit := do continue modify fun s => { s with moduleNameSet := s.moduleNameSet.insert i.module } let mFile ← findOLean i.module + unless (← mFile.pathExists) do + throw <| IO.userError s!"object file '{mFile}' of module {i.module} does not exist" let (mod, region) ← readModuleData mFile importModulesCore mod.imports modify fun s => { s with diff --git a/src/Lean/Util/Path.lean b/src/Lean/Util/Path.lean index 0bca075c0cb5..6d1ba4c4074a 100644 --- a/src/Lean/Util/Path.lean +++ b/src/Lean/Util/Path.lean @@ -40,52 +40,25 @@ where | Name.anonymous => base | Name.num _ _ => panic! "ill-formed import" -variable (base : FilePath) (ext : String) in -/-- -Checks whether a module of the given name and extension exists in `base`; this uses case-sensitive -path comparisons regardless of underlying file system to ensure the check is consistent across -platforms. --/ -partial def moduleExists : Name → IO Bool := go ext -where go (ext : String) - | .mkStr parent str => do - -- Case-sensitive check for file with extension in top-level call, for directory recursively - let entryName := if ext.isEmpty then str else s!"{str}.{ext}" - unless (← go "" parent) do - return false - return (← (modToFilePath base parent "").readDir).any (·.fileName == entryName) - | .anonymous => base.pathExists - | .num .. => panic! "ill-formed import" - /-- A `.olean' search path. -/ abbrev SearchPath := System.SearchPath namespace SearchPath -def findRoot (sp : SearchPath) (ext : String) (pkg : String) : IO (Option FilePath) := do - sp.findM? fun p => do - unless (← p.isDir) do -- Lake may pass search roots that do not exist (yet) - return false - if (← (p / pkg).isDir) then - return (← p.readDir).any (·.fileName == pkg) - else - let fileName := s!"{pkg}.{ext}" - return (← p.readDir).any (·.fileName == fileName) - /-- If the package of `mod` can be found in `sp`, return the path with extension `ext` (`lean` or `olean`) corresponding to `mod`. Otherwise, return `none`. Does not check whether the returned path exists. -/ def findWithExt (sp : SearchPath) (ext : String) (mod : Name) : IO (Option FilePath) := do let pkg := mod.getRoot.toString (escape := false) - let root? ← findRoot sp ext pkg + let root? ← sp.findM? fun p => + (p / pkg).isDir <||> ((p / pkg).addExtension ext).pathExists return root?.map (modToFilePath · mod ext) /-- Like `findWithExt`, but ensures the returned path exists. -/ def findModuleWithExt (sp : SearchPath) (ext : String) (mod : Name) : IO (Option FilePath) := do - let pkg := mod.getRoot.toString (escape := false) - if let some root ← findRoot sp ext pkg then - if (← moduleExists root ext mod) then - return some <| modToFilePath root mod ext + if let some path ← findWithExt sp ext mod then + if ← path.pathExists then + return some path return none def findAllWithExt (sp : SearchPath) (ext : String) : IO (Array FilePath) := do @@ -132,20 +105,12 @@ def initSearchPath (leanSysroot : FilePath) (sp : SearchPath := ∅) : IO Unit : private def initSearchPathInternal : IO Unit := do initSearchPath (← getBuildDir) -/-- -Returns the path of the .olean file for `mod`. Throws an error if no search path entry for `mod` -could be located, or if `checkExists` is true and the resulting path does not exist. --/ -partial def findOLean (mod : Name) (checkExists := true) : IO FilePath := do +partial def findOLean (mod : Name) : IO FilePath := do let sp ← searchPathRef.get - let pkg := mod.getRoot.toString (escape := false) - if let some root ← sp.findRoot "olean" pkg then - let path := modToFilePath root mod "olean" - if !checkExists || (← moduleExists root "olean" mod) then - return path - else - throw <| IO.userError s!"object file '{path}' of module {mod} does not exist" + if let some fname ← sp.findWithExt "olean" mod then + return fname else + let pkg := FilePath.mk <| mod.getRoot.toString (escape := false) let mut msg := s!"unknown module prefix '{pkg}' No directory '{pkg}' or file '{pkg}.olean' in the search path entries: diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean index c352b593bd41..03ca79436beb 100644 --- a/src/lake/Lake/Build/Module.lean +++ b/src/lake/Lake/Build/Module.lean @@ -31,9 +31,6 @@ Recursively parse the Lean files of a module and its imports building an `Array` product of its direct local imports. -/ def Module.recParseImports (mod : Module) : FetchM (Array Module) := do - -- Make sure we fail reading the file independently of the FS case sensitivity - unless (← Lean.moduleExists mod.lib.srcDir "lean" mod.name) do - error s!"module source file not found: {mod.leanFile}" let contents ← IO.FS.readFile mod.leanFile let imports ← Lean.parseImports' contents mod.leanFile.toString let mods ← imports.foldlM (init := OrdModuleSet.empty) fun set imp => diff --git a/tests/pkg/import-case/.gitignore b/tests/pkg/import-case/.gitignore deleted file mode 100644 index bfb30ec8c762..000000000000 --- a/tests/pkg/import-case/.gitignore +++ /dev/null @@ -1 +0,0 @@ -/.lake diff --git a/tests/pkg/import-case/ImportCase.lean b/tests/pkg/import-case/ImportCase.lean deleted file mode 100644 index 83be2888b28f..000000000000 --- a/tests/pkg/import-case/ImportCase.lean +++ /dev/null @@ -1,2 +0,0 @@ --- should *not* be accepted on any platform -import ImportCase.basic diff --git a/tests/pkg/import-case/ImportCase/Basic.lean b/tests/pkg/import-case/ImportCase/Basic.lean deleted file mode 100644 index e99d3a6f69f8..000000000000 --- a/tests/pkg/import-case/ImportCase/Basic.lean +++ /dev/null @@ -1 +0,0 @@ -def hello := "world" \ No newline at end of file diff --git a/tests/pkg/import-case/lakefile.toml b/tests/pkg/import-case/lakefile.toml deleted file mode 100644 index 6254c1e2c2e6..000000000000 --- a/tests/pkg/import-case/lakefile.toml +++ /dev/null @@ -1,5 +0,0 @@ -name = "«import-case»" -defaultTargets = ["ImportCase"] - -[[lean_lib]] -name = "ImportCase" diff --git a/tests/pkg/import-case/test.sh b/tests/pkg/import-case/test.sh deleted file mode 100755 index 889a4fb42ce8..000000000000 --- a/tests/pkg/import-case/test.sh +++ /dev/null @@ -1,5 +0,0 @@ -#!/usr/bin/env bash -set -euxo pipefail - -rm -rf .lake/build -(lake build 2>&1 && exit 1 || true) | grep --color -F 'module source file not found'