Exit status on un-proved goals
When why3 prove
leaves non proven goals, its exit status is 1
.
This is very confusing because this exit code is also used for syntax errors, incorrect command line arguments, etc. Having an « unknown » goal is a normal outcome, and shall not be meld with syntactic errors!
Although, it can be interesting to known with an exit code whether all goals have been proven or not, and it shall be different from 1
. Better: what about some -exit-unproved <n>
option on the command line, that would exit with status code <n>
in this case?
Sincerely yours, L.