test: lake: show module with failed import

src/lake/Lake/Build/Module.lean

@@ -60,7 +60,7 @@ building an `Array` product of its direct local imports.
 -/
 def Module.recParseImports (mod : Module) : IndexBuildM (Array Module) := do
   let callstack : CallStack BuildKey ← EquipT.lift <| CycleT.readCallStack
-  let contents ← liftM <| tryCatch (IO.FS.readFile mod.leanFile) (fun err =>
+  let contents ← liftM <| tryCatch (IO.FS.readFile mod.leanFile) fun err =>
     -- filter out only modules from build key, and remove adjacent duplicates (squeeze),
     -- since Lake visits multiple nested facets of the same module.
     let callstack := callstack.filterMap (fun bk =>
@@ -69,8 +69,7 @@ def Module.recParseImports (mod : Module) : IndexBuildM (Array Module) := do
       | _ => .none
     ) |> List.squeeze
     let breadcrumb := String.intercalate " ▸ " callstack.reverse
-    throw <| IO.userError s!"({breadcrumb}): {err}"
-  )
+    error s!"{breadcrumb}: {err}"
   let imports ← Lean.parseImports' contents mod.leanFile.toString
   let mods ← imports.foldlM (init := OrdModuleSet.empty) fun set imp =>
     findModule? imp.module <&> fun | some mod => set.insert mod | none => set

src/lake/tests/badImport/.gitignore

@@ -0,0 +1 @@
+lakefile.olean

src/lake/tests/badImport/Lib/A.lean

@@ -0,0 +1 @@
+import Lib.A

src/lake/tests/badImport/Lib/B.lean

@@ -0,0 +1 @@
+import Lib.C

src/lake/tests/badImport/X.lean

@@ -0,0 +1 @@
+import Y

src/lake/tests/badImport/clean.sh

@@ -0,0 +1 @@
+rm -f lakefile.olean

src/lake/tests/badImport/lakefile.lean

@@ -0,0 +1,7 @@
+import Lake
+open Lake DSL
+
+package test
+
+lean_lib X
+lean_lib Lib

src/lake/tests/badImport/test.sh

@@ -0,0 +1,14 @@
+#!/usr/bin/env bash
+set -euxo pipefail
+
+LAKE=${LAKE:-../../build/bin/lake}
+
+./clean.sh
+
+# Test that failed imports show the module that imported them
+# https://github.com/leanprover/lake/issues/25
+# https://github.com/leanprover/lean4/issues/2569
+# https://github.com/leanprover/lean4/issues/2415
+
+($LAKE build +X 2>&1 && exit 1 || true) | grep -F "X.lean"
+($LAKE print-paths Lib.B 2>&1 && exit 1 || true) | grep -F "Lib.B"