From 275af93904a17e6310550372bfb6feab22aafeb4 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Thu, 12 Oct 2023 15:33:22 -0400
Subject: [PATCH] test: lake: show module with failed import

---
 src/lake/Lake/Build/Module.lean        |  5 ++---
 src/lake/tests/badImport/.gitignore    |  1 +
 src/lake/tests/badImport/Lib/A.lean    |  1 +
 src/lake/tests/badImport/Lib/B.lean    |  1 +
 src/lake/tests/badImport/X.lean        |  1 +
 src/lake/tests/badImport/clean.sh      |  1 +
 src/lake/tests/badImport/lakefile.lean |  7 +++++++
 src/lake/tests/badImport/test.sh       | 14 ++++++++++++++
 8 files changed, 28 insertions(+), 3 deletions(-)
 create mode 100644 src/lake/tests/badImport/.gitignore
 create mode 100644 src/lake/tests/badImport/Lib/A.lean
 create mode 100644 src/lake/tests/badImport/Lib/B.lean
 create mode 100644 src/lake/tests/badImport/X.lean
 create mode 100755 src/lake/tests/badImport/clean.sh
 create mode 100644 src/lake/tests/badImport/lakefile.lean
 create mode 100755 src/lake/tests/badImport/test.sh

diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean
index ee4444b9bc..6eeace9f02 100644
--- a/src/lake/Lake/Build/Module.lean
+++ b/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
diff --git a/src/lake/tests/badImport/.gitignore b/src/lake/tests/badImport/.gitignore
new file mode 100644
index 0000000000..b96c2ef548
--- /dev/null
+++ b/src/lake/tests/badImport/.gitignore
@@ -0,0 +1 @@
+lakefile.olean
diff --git a/src/lake/tests/badImport/Lib/A.lean b/src/lake/tests/badImport/Lib/A.lean
new file mode 100644
index 0000000000..895a99b39a
--- /dev/null
+++ b/src/lake/tests/badImport/Lib/A.lean
@@ -0,0 +1 @@
+import Lib.A
diff --git a/src/lake/tests/badImport/Lib/B.lean b/src/lake/tests/badImport/Lib/B.lean
new file mode 100644
index 0000000000..49a9376868
--- /dev/null
+++ b/src/lake/tests/badImport/Lib/B.lean
@@ -0,0 +1 @@
+import Lib.C
diff --git a/src/lake/tests/badImport/X.lean b/src/lake/tests/badImport/X.lean
new file mode 100644
index 0000000000..2bfb39bdb5
--- /dev/null
+++ b/src/lake/tests/badImport/X.lean
@@ -0,0 +1 @@
+import Y
diff --git a/src/lake/tests/badImport/clean.sh b/src/lake/tests/badImport/clean.sh
new file mode 100755
index 0000000000..e30197eeaf
--- /dev/null
+++ b/src/lake/tests/badImport/clean.sh
@@ -0,0 +1 @@
+rm -f lakefile.olean
diff --git a/src/lake/tests/badImport/lakefile.lean b/src/lake/tests/badImport/lakefile.lean
new file mode 100644
index 0000000000..de8ad6ea31
--- /dev/null
+++ b/src/lake/tests/badImport/lakefile.lean
@@ -0,0 +1,7 @@
+import Lake
+open Lake DSL
+
+package test
+
+lean_lib X
+lean_lib Lib
diff --git a/src/lake/tests/badImport/test.sh b/src/lake/tests/badImport/test.sh
new file mode 100755
index 0000000000..8c02a8a48b
--- /dev/null
+++ b/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"