could lake report the file where a build error appears?

Stream: lean4

[Rob Lewis]

I just tried to lake build a large project where one file has an import error:

$ lake build LoVe
error: no such file or directory (error code: 2)
  file: ./././LoVe/Love10_HoareLogic_DemoMaster.lean

It took me a few minutes to figure out what the problem was. (The file name is LoVe10_, oops, but spelled correctly in other places.) It would be super helpful if lake could report which file the error appears in. Is this feasible? And if I should open an issue, is it more appropriate for lake or lean4?

[Sebastian Ullrich]

Yes, please open an issue in lean4!

[Mac Malone]

@Rob Lewis FYI, this is already reported as lake#25. lake#34 would also help.