RFC: Exclude transitively failing files from build output

Stream: lean4

[Yaël Dillies]

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

[Yaël Dillies]

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!

[Yaël Dillies]

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.

[Ruben Van de Velde]

Also, the first error is on the file that doesn't exist, rather than the file that has the broken import

[Kevin Buzzard]

At least this is better than before though, where not only was the error triggered by a bad import obscure but it didn't even mention "bad import" at all (oh wait, that was for looping imports, maybe that's different)

[Yaël Dillies]

Yes indeed, that was different

[Kim Morrison]

@Yaël Dillies, can you open an issue?

[Yaël Dillies]

lean4#7280