fix: bad 'unknown package' error message (leanprover#4424)

This message is older than corresponding, better checks in Lake and vscode-lean4 Fixes leanprover#4419 --------- Co-authored-by: Mac Malone <[email protected]>
jumanjimi · Jun 13, 2024 · 749bf9c · 749bf9c
1 parent 7b971b9
commit 749bf9c
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 11 deletions.
diff --git a/src/Lean/Util/Path.lean b/src/Lean/Util/Path.lean
@@ -111,16 +111,10 @@ partial def findOLean (mod : Name) : IO FilePath := do
     return fname
   else
     let pkg := FilePath.mk <| mod.getRoot.toString (escape := false)
-    let mut msg := s!"unknown package '{pkg}'"
-    let rec maybeThisOne dir := do
-      if ← (dir / pkg).isDir then
-        return some s!"\nYou might need to open '{dir}' as a workspace in your editor"
-      if let some dir := dir.parent then
-        maybeThisOne dir
-      else
-       return none
-    if let some msg' ← maybeThisOne (← IO.currentDir) then
-      msg := msg ++ msg'
+    let mut msg := s!"unknown module prefix '{pkg}'
+
+No directory '{pkg}' or file '{pkg}.lean' in the search path entries:
+{"\n".intercalate <| sp.map (·.toString)}"
     throw <| IO.userError msg
 
 /-- Infer module name of source file name. -/

diff --git a/src/lake/tests/badImport/test.sh b/src/lake/tests/badImport/test.sh
@@ -13,7 +13,7 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}
 # https://github.com/leanprover/lean4/issues/3809
 
 # Test importing a nmissing module from outside the workspace
-($LAKE build +X 2>&1 && exit 1 || true) | grep --color -F "X.lean:1:0: unknown package 'Y'"
+($LAKE build +X 2>&1 && exit 1 || true) | grep --color -F "X.lean:1:0: unknown module prefix 'Y'"
 $LAKE setup-file ./X.lean Y # Lake ignores the file (the server will error)
 # Test importing onself
 ($LAKE build +Lib.A 2>&1 && exit 1 || true) | grep --color -F "A.lean: module imports itself"