lean without warning

Stream: general

[Patrick Massot]

@Gabriel Ebner how hard would it be to add a command line switch to lean --make to suppress all sorry warnings and #check or #print output, leaving only errors? Those days we are breaking a lot the LFTCM2020 repository with mathlib upgrades and it's very painful to spot the error in a huge flood of warnings and checks.

[Sebastien Gouezel]

My workflow is:

lean --make >> errors.txt

and then open the file errors.txt and look for error.

[Patrick Massot]

Sébastien, seeing the error in real time would be much faster.

[Sebastien Gouezel]

Of course!

[Kevin Buzzard]

When working on LTE I also wish for a --suppress-warnings option

[Johan Commelin]

I guess for LTE the fix is to just get rid of all those sorrys :stuck_out_tongue_wink:

[Mario Carneiro]

Patrick Massot said:

Sébastien, seeing the error in real time would be much faster.

You can pipe the output of lean through grep or awk. I used to have a script for doing this to one of the metamath tools that had a lot of noisy diagnostics - I would filter out all the diagnostic messages I didn't care about and reformat the errors with color and priority to make them more obvious

[Kevin Buzzard]

You can but unfortunately you then have to rely on the buffer being flushed. I've tried this and sometimes you just sit there with no output

[Ben Toner]

You can move further towards what you want with lean --make 2> /dev/null | grep -v sorry.

This works because the #print and #check commands write to stderr (file descriptor 2) , which we redirect with the 2>. Error and warning messages are on stdout so are not affected.

Piping to grep has trade-offs: it consumes the progress messages (e.g. parsing at line 700) and you'll also have to potentially wait as @Kevin Buzzard says, although that can be solved: e.g., on Ubuntu you can sudo apt install expect and then
unbuffer lean --make 2> /dev/null | grep -v sorry.

[Patrick Massot]

Thanks!