Lean4
/-- `importPathMessage env idx` produces a message laying out an import chain from `idx` to the
current module. The output is of the form
```
Mathlib.Init,
which is imported by Mathlib.Util.AssertExistsExt,
which is imported by Mathlib.Util.AssertExists,
which is imported by this file.
```
if `env` is an `Environment` and `idx` is the module index of `Mathlib.Init`.
-/
def importPathMessage (env : Environment) (idx : ModuleIdx) : MessageData :=
let modNames := env.header.moduleNames
let msg :=
(env.importPath modNames[idx]!).foldl (init := m! "{modNames[idx]!},") (· ++ m!"\n which is imported by {·},")
msg ++ m!"\n which is imported by this file."
