lake: redundant missing import errors

[digama0]

Here is an example failing build of Mathport due to a moved upstream file:

$ lake build
✖ [63/1717] Running Mathlib.Init.ZeroOne
error: no such file or directory (error code: 2)
  file: ././.lake/packages/mathlib/././Mathlib/Init/ZeroOne.lean
✖ [64/1717] Running Mathport.Binary.Number
error: ././././Mathport/Binary/Number.lean: bad import 'Mathlib.Init.ZeroOne'
✖ [65/1717] Running Mathport.Binary.Heterogenize
error: ././././Mathport/Binary/Heterogenize.lean: bad import 'Mathport.Binary.Number'
✖ [66/1717] Running Mathport.Binary.TranslateExpr
error: ././././Mathport/Binary/TranslateExpr.lean: bad import 'Mathport.Binary.Number'
error: ././././Mathport/Binary/TranslateExpr.lean: bad import 'Mathport.Binary.Heterogenize'
✖ [67/1717] Running Mathport.Binary.Apply
error: ././././Mathport/Binary/Apply.lean: bad import 'Mathport.Binary.TranslateExpr'
✖ [68/1717] Running Mathport.Binary
error: ././././Mathport/Binary.lean: bad import 'Mathport.Binary.Apply'
✖ [1641/1717] Running Mathport
error: ././././Mathport.lean: bad import 'Mathport.Binary'
✖ [1642/1717] Running MathportApp
error: ././././MathportApp.lean: bad import 'Mathport'
✖ [1644/1717] Running mathport
error: ././././MathportApp.lean: bad import 'Mathport'

The first error is correct, but all subsequent errors are incorrect / misleading. Essentially, if a file imports a nonexistent file, then that file will itself be considered nonexistent by its dependencies, possibly leading to hundreds of cascading failures, within which the original error might be hard to spot.

Tested on Lake version 5.0.0-702c31b (Lean version 4.10.0-rc2).

[tydeu]

@digama0 Yes, this was intentionally designed this way. It is not necessarily the case that the module with a bad import is the problem, it can sometimes be its parents. While not as often useful in the case of a missing file, it can be very useful for cyclic imports (both missing files and cycles are considered "bad imports").

However, since it is less useful for files missing imports, maybe it is worth sacrificing the information for that special case?