lake feature request: reporting nonexistent imports

Stream: lean4

[Frédéric Dupuis]

Suppose that a Lean file imports another Lean file that doesn't exist (which happens fairly frequently when bumping mathlib in a project, or merging master in a mathlib branch). Then, when trying lake build, the failure reported looks like this:

✖ [?/?] Computing build jobs
error: no such file or directory (error code: 2)
  file: ././././Mathlib/Topology/Algebra/UniformGroup.lean
Some required builds logged failures:
- Computing build jobs
error: build failed

Here lake reports the file that doesn't exist, but not which file tried to import it. Would it be possible to make it output this information as well?

[Henrik Böving]

CC @Mac Malone do we have a tracking issue for this already somewhere?

[Junyan Xu]

I'd search the module name in the VSCode search box:
image.png

[Henrik Böving]

I think it's clear to everyone involved how to fix this issue and how to find the location where it's occuring from manually, the point is that you should not need to do this by hand as lake already knows what file is at fault when it throws this error.

[Ruben Van de Velde]

Speaking of, can we get rid of ./././?

[Ruben Van de Velde]

Sorry, ././././

[Joachim Breitner]

Ruben Van de Velde said:

Sorry, ././././

https://github.com/leanprover/lean4/issues/6186

[Kim Morrison]

Nice, and I've already +1'd it. I still find this disconcerting.