From 82bb27fd7d9e339419483710ed0fe21c9f7ad3f4 Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Thu, 9 Apr 2026 00:03:52 -0400
Subject: [PATCH] fix: lake: report bad imports from a library build (#13340)

This PR fixes a Lake issue where library builds would not produce
informative errors about bad imports (unlike module builds).
---
 src/lake/Lake/Build/Library.lean         | 35 +++++++++++++++---------
 tests/lake/tests/badImport/lakefile.lean |  4 ++-
 tests/lake/tests/badImport/test.sh       |  4 +++
 3 files changed, 29 insertions(+), 14 deletions(-)

diff --git a/src/lake/Lake/Build/Library.lean b/src/lake/Lake/Build/Library.lean
index 6cb600d16b..6fcf2fed23 100644
--- a/src/lake/Lake/Build/Library.lean
+++ b/src/lake/Lake/Build/Library.lean
@@ -24,6 +24,11 @@ namespace Lake
 
 /-! ## Build Lean & Static Lib -/
 
+private structure ModuleCollection where
+  mods : Array Module := #[]
+  modSet : ModuleSet := ∅
+  hasErrors : Bool := false
+
 /--
 Collect the local modules of a library.
 That is, the modules from `getModuleArray` plus their local transitive imports.
@@ -31,23 +36,27 @@ That is, the modules from `getModuleArray` plus their local transitive imports.
 private partial def LeanLib.recCollectLocalModules
   (self : LeanLib) : FetchM (Job (Array Module))
 := ensureJob do
-  let mut mods := #[]
-  let mut modSet := ModuleSet.empty
+  let mut col : ModuleCollection := {}
   for mod in (← self.getModuleArray) do
-    (mods, modSet) ← go mod mods modSet
-  return Job.pure mods
+    col ← go mod col
+  if col.hasErrors then
+    -- This is not considered a fatal error because we want the modules
+    -- built to provide better error categorization in the monitor.
+    logError s!"{self.name}: some modules have bad imports"
+  return Job.pure col.mods
 where
-  go root mods modSet := do
-    let mut mods := mods
-    let mut modSet := modSet
-    unless modSet.contains root do
-      modSet := modSet.insert root
-      let imps ← (← root.imports.fetch).await
+  go root col := do
+    let mut col := col
+    unless col.modSet.contains root do
+      col := {col with modSet := col.modSet.insert root}
+      -- We discard errors here as they will be reported later when the module is built.
+      let some imps ← (← root.imports.fetch).wait?
+        | return {col with hasErrors := true}
       for mod in imps do
         if mod.lib.name = self.name then
-          (mods, modSet) ← go mod mods modSet
-      mods := mods.push root
-    return (mods, modSet)
+          col ← go mod col
+      col := {col with mods := col.mods.push root}
+    return col
 
 /-- The `LibraryFacetConfig` for the builtin `modulesFacet`. -/
 private def LeanLib.modulesFacetConfig : LibraryFacetConfig modulesFacet :=
diff --git a/tests/lake/tests/badImport/lakefile.lean b/tests/lake/tests/badImport/lakefile.lean
index 2eeaac9621..dbce133313 100644
--- a/tests/lake/tests/badImport/lakefile.lean
+++ b/tests/lake/tests/badImport/lakefile.lean
@@ -3,7 +3,9 @@ open Lake DSL
 
 package test
 
-lean_lib Lib
+lean_lib Lib where
+  globs := #[`Lib.+]
+
 lean_lib Etc
 
 lean_exe X
diff --git a/tests/lake/tests/badImport/test.sh b/tests/lake/tests/badImport/test.sh
index 54ca71f90c..7f77c87495 100755
--- a/tests/lake/tests/badImport/test.sh
+++ b/tests/lake/tests/badImport/test.sh
@@ -10,6 +10,10 @@ source ../common.sh
 # https://github.com/leanprover/lean4/issues/3351
 # https://github.com/leanprover/lean4/issues/3809
 
+# Test that library builds report bad imports
+test_err "module imports itself" build Lib:static
+test_err "Lib: some modules have bad imports" build Lib
+
 # Test a module with a bad import does not kill the whole build
 test_err "Building Etc" build Lib.U Etc
 # Test importing a missing module from outside the workspace