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

Prerequisites

• 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 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by reviewing the RFC description and the Lean-side implementation in #3568, then examine the lake build flow and the related discussion about continuing after errors. The open design questions are how lake should proceed without stopping the build or silently swallowing errors, and what the default behavior should be. Done means downstream files continue building while the elaboration error remains visible.