Instant build fail on wrong import

Stream: general

[Yaël Dillies]

When you write an import statement about a file that doesn't exist, the build instantly fails. Is there a reason why it's so, instead of letting the build continue for every file not downstream of the wrong import, like every other error?

[Yaël Dillies]

1. In mathlib CI, it's annoying because I don't get to see the next error, and sometimes I have several wrong imports and don't notice until I have wasted 2-3 CI cycles.
2. I thought maybe this has to do with the fact that we wouldn't even know what to build when an import is wrong, but actually that's not true. Any file whose transitive dependencies all have correct imports can be built.
3. The error only tells me what the wrong import is, but not where it is.

[Yury G. Kudryashov]

A workaround: run timeout 20 lake build before git push

[Yaël Dillies]

Yeah, I know about that workaround, but it involves more brain power than I have when I push

[Sebastian Ullrich]

I think the reason is simply that this will need extra code, so could you log a Lake issue at lean4?

[Yaël Dillies]

lean4#3809

[Damiano Testa]

Does the proposal also include the possibility of importing a file that exists but contains an error and still try to make the best of it?

[Yaël Dillies]

No