Lake default verbosity

Stream: lean4

[Mario Carneiro]

Currently, lake will print out the command it uses to compile every file. This is useful in some circumstances, but it makes it more difficult to spot warnings and errors and I have started piping the output through grep so that don't have to hunt for the actual warnings in a sea of text. I would propose that the current output be hidden behind a -v/--verbose flag, and the default behavior should be to skip those lines but print anything that lean has to say.

In the future, it might be better to get a more ncurses-style status view, similar to what lean 3 does (but less buggy on long file names). That way you can at least see progress through the files.

[Scott Morrison]

I was going to ask for the same thing!

[Mac]

This is on the the TODO list, and I hope to get around to it. Unfortunately, I only have two weeks left in my internship before I have to switch back to focus on my dissertation research. Thus, I am not sure whether I will have the time. I do hope to still sporadically update Lake in the Fall, so hopefully this won't be on the list for another whole year.

[Mario Carneiro]

The -v change should be a small one (just gate the print behind a conditional). I can try to make a PR if you don't have the time

[James Gallicchio]

resurrecting this, I'd love to have less verbose output from lake, seems an easy way to get a huge UX improvement

[Mario Carneiro]

This should have landed already

[Mario Carneiro]

I'm getting messages like Building Foo.Bar, is that not your experience?

[Mario Carneiro]

Lake version 4.0.0 (Lean version 4.0.0-nightly-2022-09-15)

[James Gallicchio]

Oh, wait, you're right -- lake gives relatively minimal output. I was thinking of the language server error messages at the top of files when their dependencies don't compile, which have nothing to do with lake

[Mario Carneiro]

That's lean4#1438