RFC(lake): Do not include missing files in `Some builds logged failures`

Proposal

Thanks to #4115, #3809 is solved! This is great, except that I noticed some rough edges in the new grouping. Here's one:

When running lake build in MyProject, the log ends with something like this:

Some builds logged failures:
- DependencyProject.Foo
- MyProject.Bar
- MyProject

I would hope this list is the list of files I need to fix. However, DependencyProject.Foo is not part of my project and does not even exist. The reason it's included in the list is because MyProject.Bar tries to import DependencyProject.Foo, but this information is already available to me via MyProject.Bar being in the list.

It's important that the output of lake build clearly pinpoints where the errors are, as this is what users like me look at to fix the build.

Community Feedback

Zulip

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.