diff --git a/RELEASES.md b/RELEASES.md index 7aa09c12e0..688b6876ed 100644 --- a/RELEASES.md +++ b/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 diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean index 97246db729..ee4444b9bc 100644 --- a/src/lake/Lake/Build/Module.lean +++ b/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 diff --git a/src/lake/Lake/Util/Cycle.lean b/src/lake/Lake/Util/Cycle.lean index 523bd0f16e..d2608c8a73 100644 --- a/src/lake/Lake/Util/Cycle.lean +++ b/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. diff --git a/src/lake/Lake/Util/List.lean b/src/lake/Lake/Util/List.lean new file mode 100644 index 0000000000..8070825628 --- /dev/null +++ b/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