error out on `sorry`

Stream: lean4

[Tudor achim]

Is there a way to get lean to return a non-zero error code if there's a sorry in a given file? Currently it just prints a warning and returns 0. I looked at the flags that lean accepts and also searched in zulip for a set_option that might do this but didn't find anything.

[Mac Malone]

Do you want an non-zero error code only in the case of sorry or would a non-zero for all warnings also be okay? If the later, the warningAsError option can solve this problem:

$ echo "example : Nat := sorry" | lean --stdin -DwarningAsError=true; echo $?
<stdin>:1:0: error: declaration uses 'sorry'
1

[Tudor achim]

Non-zero for all warnings is totally cool! Thanks!

[Tudor achim]

Is there a way to enumerate all the options registered with register_builtin_option ?

[Alex J. Best]

You can use

import Lean
import Mathlib.Tactic.HelpCmd

#help option

this well get you all options, not just the builtins, but it should be close enough (the list will grow if you import Mathlib I presume)