Make lean4 fail at sorry

Stream: new members

[Vadim Fomin]

Hi there, noob question: is there a way to make lean4 fail when it encounters a sorry, instead of writing a warning declaration uses 'sorry'?
UPD: fail as in "elevate it to an error"

[Edward van de Meent]

what is it you mean with "fail"? do you want to elevate it to an error? do you want the server/compiler to panic?

[Vadim Fomin]

I meant for it to elevate it to an error

[Daniel Weber]

You can run lake build --wfail

[Daniel Weber]

This makes all warnings cause it to fail

[Vadim Fomin]

Thanks! Is there something more specific to sorry maybe? Or a way to check if code uses a sorry?

[Vadim Fomin]

E.g. I've read that mathlib CI checks that there are no sorries, but I'm not sure where in the github workflow it does that...

[Edward van de Meent]

in order to check if a declaration uses sorry you can use #print axioms foo. however, i believe mathlib uses other ways to guard against this.