New lake messages

Stream: lean4

[Patrick Massot]

I’m bumping Mathematics in Lean from 4.6.0 to 4.8.0rc1 and lake build ends with:

Some build steps logged failures:
- Computing build jobs
- Building MIL.C02_Basics.S04_More_on_Order_and_Divisibility
- Building MIL.C02_Basics.S05_Proving_Facts_about_Algebraic_Structures
- Building MIL.C03_Logic.S02_The_Existential_Quantifier
- Building MIL.C03_Logic.S06_Sequences_and_Convergence
- Building MIL.C04_Sets_and_Functions.S03_The_Schroeder_Bernstein_Theorem
- Building MIL.C05_Elementary_Number_Theory.S01_Irrational_Roots
- Building MIL.C05_Elementary_Number_Theory.S02_Induction_and_Recursion

This is so much nicer than crawling through the output to search for file names! Thanks a lot @Mac Malone!

[Kevin Buzzard]

Oh this is very cool! This is a great improvement! Thanks a lot Mac!

[Yaël Dillies]

I recently noticed that the "lint mathlib" step of CI runs even if the "build mathlib" fails. As a consequence, all the build errors resurface during linting (which fails quickly), making it super practical to debug a PR.

[Damiano Testa]

@Yaël Dillies this was probably a consequence of #11454: I intended for CI to continue after shake, but it seems that it just... continues!

[Yaël Dillies]

Oh I see. Serendipitous!

[Patrick Massot]

I have fixed all errors except for

Some build steps logged failures:
- Computing build jobs
error: build failed

which is not very useful. Here I need to go at the very beginning of the lake output to find the error (a non-existent import). The Summary message would a be lot more useful if Computing build jobs could be replaced (or extended) with something mentioning the missing file and where it is imported.

[Mac Malone]

That is a consequence of a import errors causing the main Lake process to fail. Yael already reported this as an issue in lean4#3809. Fixing that should fix this as well.

[Patrick Massot]

Thanks Mac. I understand where this comes from. I simply say it could be nicer. And, since you recently improved those messages a lot, I thought now may be a good time.

[Yaël Dillies]

I've edited the issue to mention that the error message doesn't where the bad import is

[Patrick Massot]

And now I am super confused. I think I got rid of all errors, but lake does not become silent, it still seems to go through files and print messages.

[Patrick Massot]

But it exits with code 0. Does this mean lean is happy?

[Yaël Dillies]

Yes I believe that's another recent change

[Patrick Massot]

Then it is a bit disturbing. Maybe ending with a friendly message telling that everything is ok would be nice.

[Utensil Song]

Does lake know these are no-ops? If so, a message like make's in this situation can be emitted to indicate that nothing needs to be done. make's message makes it clear that it has check all targets/tasks (nothing is missing), and nothing further needs to be done (no todo, no failure), so the user is rest assured.

[Mac Malone]

@Utensil Song Sadly, no, not at the top-level were the progress is now managed.

[Utensil Song]

Ah, I see. I assumed that the information is propagated like task todo/done/no-op.