RFC: Exclude transitively failing files from build output

Proposal

This is not clearly a RFC nor a bug report since the behavior described might be intended.

Consider the following build log: https://github.com/leanprover-community/mathlib4/actions/runs/13527525523/job/37801718042 It contains hundreds of very uniformative lines of the form error: ././././Mathlib.lean: bad import 'Mathlib.Topology.Instances.Irrational', followed by the same number of lines in the Some required builds logged failures: part.

This happens because I added an import to Mathlib.Algebra.Group.Aut, which doesn't exist. But it's really hard to figure this information from the build output!

What seems to happen is that files with a missing import do not get an olean, and so in turn appear missing to the files that import them.

Suggestion: Make sure that only the files that are immediately failing get mentioned in the build output. Possibly polemically, that could also exclude the file which I am wrongly trying to import, eg here Mathlib.Algebra.Group.Aut.

Benefits: The build output now acts as an actionable list of files. This will benefit everyone in the community, but particularly people working on big projects like Mathlib.

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.

Start with the linked build log and the reported missing import of Mathlib.Algebra.Group.Aut, then trace how transitively missing .olean files are reported in build output. Done means the output identifies only immediately failing files, with the desired treatment of the missing imported file clarified and covered by suitable tests.