Zulip Chat Archive

Stream: lean4

Topic: Lake default verbosity


Mario Carneiro (Jul 27 2022 at 01:56):

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 (Jul 27 2022 at 01:58):

I was going to ask for the same thing!

Mac (Jul 27 2022 at 08:00):

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 (Jul 27 2022 at 08:10):

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 (Sep 20 2022 at 19:08):

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

Mario Carneiro (Sep 20 2022 at 19:08):

This should have landed already

Mario Carneiro (Sep 20 2022 at 19:09):

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

Mario Carneiro (Sep 20 2022 at 19:09):

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

James Gallicchio (Sep 20 2022 at 19:12):

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 (Sep 20 2022 at 19:13):

That's lean4#1438


Last updated: Dec 20 2023 at 11:08 UTC