RFC: lake job tally to count failed jobs

I was just watching a mathlib build on CI, looking at lines like

✔ [7021/7028] Built Mathlib.NumberTheory.NumberField.DedekindZeta (2.4s)

and was happy that the build looks good and will succeed in a moment. Only to then see

error: build failed
Some required targets logged failures:
- Batteries.Data.HashMap.Lemmas
- Mathlib.Data.Nat.Hyperoperation

and making me disappointed.

I assume it is often that case that when people are watching an ongoing build they will want to know if it will succeed or if has already failed, because often if here is some error, you might want to abort the build or do something else.

(Passing the flag to lake to not keep going isn’t helpful here, because you don't know that in advance or it’s CI).

Proposal

I’d like the ongoing build monitor to somehow indicate that some jobs have failed, and maybe how many. Possible ideas:

✔ [7019✔ 2✖ 7028⧗] Built Mathlib.NumberTheory.NumberField.DedekindZeta (2.4s)

or (with the count only showing up if non-zero)

✔ [7021/7028 (2✖)]] Built Mathlib.NumberTheory.NumberField.DedekindZeta (2.4s)

or possibly other ideas.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start at the Lake ongoing build monitor and its existing output for completed targets and required target failures. Compare the proposed tally formats and define a consistent indication of nonzero failed jobs; done means an ongoing build clearly shows whether failures have already occurred and how many.