lake build less verbose

Stream: lean4

[Jon Eugster]

Is there some config option for lake build so that logInfos (blue squigglies) are not printed to the shell?

[Richard Copley]

Does --quiet (or -q) do what you want? (lake --quiet build)

[Mario Carneiro]

no, that only suppresses status messages

[Mario Carneiro]

> /dev/null will probably work :upside_down:

[Richard Copley]

moreLeanArgs := #["--quiet"]? (or weakLeanArgs)

[Jon Eugster]

I think both of these versions are good for not getting any output at all and only get the errors. However, what I was specifically looking for is:

• don't have logInfo printed
• still get logWarning printed (they are also printed to stdout)
• preferabble still get the [1629/1649] Building Project.Algebra.Basic messages, but not essential

[Jon Eugster]

I guess there is something like WarningAsError but I think with that the build fails if there are any warnings at all

[Mario Carneiro]

I think the ability to do this in lake is limited by the fact that it doesn't receive messages in a machine readable format (e.g. json), it's just seeing lean print things to stdout

[Richard Copley]

I'm not sure which messages "lean --quiet" suppresses, but not all of them; the help says "do not print verbose messages". Give it a try? And the 'Building' message comes from lake, not lean, so shouldn't be affected by adding "--quiet" to weakLeanArgs.

[Jon Eugster]

Buster said:

moreLeanArgs := #["--quiet"]? (or weakLeanArgs)

It seems like this has no effect for me at all. I'll need a second to investigate :thinking:

[Jon Eugster]

Buster said:

moreLeanArgs := #["--quiet"]? (or weakLeanArgs)

looks like both of these versions still print infos to stdout (unless Im doing something wrong...), thanks for the suggestion though

[Richard Copley]

Hmm, that's disappointing. It looks like "--quiet" only cancels a previous "--verbose".

[Mario Carneiro]

like I said, it disables status messages (i.e. Building Foo.Bar)

[Jon Eugster]

I wasn't sure if lake --quiet build and lean --quiet were two different options and you were commenting on the former.

[Mario Carneiro]

oh, does lean also have a --quiet option? I was commenting only on the former

[Mario Carneiro]

lean --quiet is apparently equivalent to set_option verbose false

[Mario Carneiro]

AFAICT this option has no effect

[Jon Eugster]

oh well, I can live with a noisy output:sweat_smile:

[Mario Carneiro]

the mathlib approach is just to try to avoid noisy output in the first place

[Mario Carneiro]

unless you are writing teaching material it's generally bad practice to leave things with info logging in the source

[Jon Eugster]

Mario Carneiro said:

the mathlib approach is just to try to avoid noisy output in the first place

It is for teaching. I like the idea to have logInfo to help people creating a game, something like "Your exercise overwrites a statement existing in mathlib, the mathilb version will be used in the next level" or "You did not provide a tactic documentation, displaying the docstring instead" can be really useful when writing NNG levels.

[Kevin Buzzard]

What I've been doing is just building twice. The first time you get all the blue underline information, the second time you don't.

[Jon Eugster]

Well if you don't need to rebuild a file, you won't get any messages, info or warning, from that file

[Jon Eugster]

Today I revisited this, so I'm leaving a note here for reference. My solution currently is to set -Dtrace.debug in the lakefile:

package Game where
  moreLeanArgs := #["-Dtrace.debug=false"]
  moreServerArgs := #["-Dtrace.debug=true"]

and then use trace[debug] "a message that only displays in vscode." to display blue squiggles in VS-Code that do not appear when calling lake build. The disadvantage is that you loose the perks of logInfo like logInfoAt ref m!"x: {x}".

Another option seems to be to misuse any inbuilt option in that way and then use if autoLift.get (← getOptions) then but obviously it's quite bad to set such an option and it might break things. I didn't find a way to set my custom option (register_option) depending on whether we run in server or not. I did not find a way to test if we are in server from within lean.

[Mac Malone]

Jon Eugster said:

I did not find a way to test if we are in server from within lean.

Yes, this is sadly a missing feature. It might be worth making an RFC issue on leanprover/lean4 requesting it. It may be sufficiently popular to get noticed.