RFC: lean/lake should continue building files downstream of an elaboration error

Prerequisites

[X] Put an X between the brackets on this line if you have done all of the following:
- Check that your issue is not already filed.
- Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

When performing fixes to mathlib or other large projects after a change to lean or other foundational library, it can be inconvenient to have to iterate several times with CI or a local build finding errors, fixing them, and then finding new errors in downstream files. Lean will already report multiple errors when they occur in a single file, but the cross file case is currently not handled, and fixing this requires changes to both lean and lake.

Context

This has come up many times, but the nightly fixes for this month's release have been particularly susceptible to this because of many back-and-forths with new lean changes that fix and break many things in mathlib. (I suggested this briefly on Zulip and it appeared well received; I expect that the team would be on board with this general direction, although there are a few design decisions to be made about how to surface it and what to make the default behavior.)

Additional Information

The lean side of this is implemented in #3568. For the lake side it requires a bit of discussion on how best to continue after an error without stopping the build or swallowing the error silently.

Impact

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

leanprover / lean4