chore: revert "fix: make import resolution case-sensitive on all platforms" (#4896)

Reverts leanprover/lean4#4538 because of unexpected overhead

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

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

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:

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 =>

tests/pkg/import-case/.gitignore

@@ -1 +0,0 @@
-/.lake

tests/pkg/import-case/ImportCase.lean

@@ -1,2 +0,0 @@
--- should *not* be accepted on any platform
-import ImportCase.basic

tests/pkg/import-case/ImportCase/Basic.lean

@@ -1 +0,0 @@
-def hello := "world"

tests/pkg/import-case/lakefile.toml

@@ -1,5 +0,0 @@
-name = "«import-case»"
-defaultTargets = ["ImportCase"]
-
-[[lean_lib]]
-name = "ImportCase"

tests/pkg/import-case/test.sh

@@ -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'