feat: show path of failed import (#2616)

RELEASES.md

@@ -11,6 +11,7 @@ v4.3.0 (development in progress)
 ---------
 
 * The derive handler for `DecidableEq` [now handles](https://github.com/leanprover/lean4/pull/2591) mutual inductive types.
+* [Show path of failed import in Lake](https://github.com/leanprover/lean4/pull/2616).
 * [Fix linker warnings on macOS](https://github.com/leanprover/lean4/pull/2598).
 
 v4.2.0

src/lake/Lake/Build/Module.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich, Mac Malone
 -/
 import Lake.Util.OrdHashSet
+import Lake.Util.List
 import Lean.Elab.ParseImportsFast
 import Lake.Build.Common
 
@@ -58,7 +59,18 @@ 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) : IndexBuildM (Array Module) := do
-  let contents ← IO.FS.readFile mod.leanFile
+  let callstack : CallStack BuildKey ← EquipT.lift <| CycleT.readCallStack
+  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 =>
+      match bk with
+      | .moduleFacet mod .. => .some s!"'{mod.toString}'"
+      | _ => .none
+    ) |> List.squeeze
+    let breadcrumb := String.intercalate " ▸ " callstack.reverse
+    throw <| IO.userError 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/Lake/Util/Cycle.lean

@@ -15,6 +15,11 @@ abbrev Cycle κ := CallStack κ
 /-- A transformer that equips a monad with a `CallStack` to detect cycles. -/
 abbrev CycleT κ m := ReaderT (CallStack κ) <| ExceptT (Cycle κ) m
 
+/-- Read the call stack from a CycleT.
+  this specialized version exists to be used in e.g. `BuildM`. -/
+def CycleT.readCallStack [Pure m] : CycleT κ m (CallStack κ) :=
+  fun callStack => ExceptT.mk <| pure (Except.ok callStack)
+
 /--
 Add `key` to the monad's `CallStack` before invoking `act`.
 If adding `key` produces a cycle, the cyclic call stack is thrown.

src/lake/Lake/Util/List.lean

@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2023 Siddharth Bhat. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Siddharth Bhat
+-/
+
+open Lean
+
+namespace Lake
+
+/-- Remove adjacent duplicates. -/
+def List.squeeze [BEq α] : List α → List α
+| [] => []
+| x :: xs =>
+  match List.squeeze xs with
+  | [] => [x]
+  | x' :: xs' => if x == x' then x' :: xs' else x :: x' :: xs'
+
+end Lake