Quieter CI logging

Stream: mathlib4

[Bolton Bailey]

When my PR (this one inspired this) experiences CI failure on build mathlib due to some warning like a linter problem, it typically prints out 1000s of lines of logs about all the files it successfully built. This makes it hard to scroll through and find the actual error.

Could the --quiet flag be passed to the build command for this CI step so that we don't have to look through all of this? Would that harm anything else?

[Bolton Bailey]

See #25167 for experimentation

[Damiano Testa]

I personally find that quiet options in CI are never a good idea. So much can go wrong that any form of hint about what the remote computer is doing is valuable.

[Damiano Testa]

In the specific case of lake build, the current setup gives a progress report with number of built file/number of files to be built information. This is very useful to monitor how the build is progressing, potentially catching issues with individual files and informing of whether a problematic file has passed CI or not.

[Damiano Testa]

If you want the quiet output, you can download the cache and replay it locally with all the flags that are appropriate.

[Damiano Testa]

Alternatively, I would rather explore the possibility of adding a CI step that runs lake build with the quiet option and maybe also no-build, to get a "cleaner" output that hopefully does not increase build times significantly.