Build project without warnings

Stream: new members

[Martin Dvořák]

I want to build my project so that, from the output of the command, I will clearly see whether the build succeeded or failed, not showing sorry warnings. I want to ignore all check and print too. When the output is too long, I sometimes overlook an error. I tried lean --make -q src but it didn't omit the stuff I wanted to ignore.

[Alex J. Best]

You could use the JSON output option to filter errors (there in lean 3 for sure, no idea about 4). I'm on mobile now so can't link to the thread but someone asked before and we came up with: lean --json src/s.lean | jq 'select(.severity == "error") | [{"name":.file_name,"error":.text, "line":.pos_line}]' using the tool jq

[Eric Wieser]

Doesn't the exit code tell you that?

[Kevin Buzzard]

If it does then LTE is finished (and it's not):

buzzard@bob:~/active-lean-projects/lean-liquid$ lean --make src
buzzard@bob:~/active-lean-projects/lean-liquid$ echo $?
0

There are for sure sorries in that repo, and I saw the warnings when I compiled the first time, but when I compile the second time it ignores them.

[Eric Wieser]

@Martin Dvořák said they wanted to ignore "sorry warnings"

[Eric Wieser]

I think LTE considers "sorry" more than a warning