a flag to stop `lean --make` at the first error

[robertylewis]

When I call lean --make I often don't care about the full output; either it succeeds, or there's an error, and I want to start fixing from the first error. Would it be possible to add a flag that would stop the build as soon as something goes wrong?

mathlib pipes the build into a Python script to short circuit on errors, and I'd like to duplicate that behavior in other CI in a less hackish way.

Prerequisites

• [ ] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs, or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

[Description of the issue]

Steps to Reproduce

1. [First Step]
2. [Second Step]
3. [and so on...]

Expected behavior: [What you expect to happen]

Actual behavior: [What actually happens]

Reproduces how often: [What percentage of the time does it reproduce?]

Versions

You can get this information from copy and pasting the output of lean --version, please include the OS and what version of the OS you're running.

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.