Exit with failure code with faults were found

[raymyers]

Fault is a CLI tool run by developers to check their work. Therefore it's reasonable to assume it will someday be used in CI builds. In that situation, a user would expect the default behavior to return non-zero exit code failing the pipeline.

If I've understood the various modes of execution correctly, this change will cause fault to return 1 when faults were found.

Alternatives

Other conventions worth considering: allow an option to disable the meaningful return code (e.g. --quiet), or default to returning 0 and provide --exit-code option like git-diff does.

I opted for what seemed like the best default and avoiding customization unless it proved necessary, open to other ways.

[mbellotti]

I'm pondering whether it's better to make this a configuration option or not.

Traditionally model checkers are supposed to find failure cases and non-zero exit reads to me as the program failed to run correctly ... on the other hand I get your point: this makes it possible to integrate models with CI/CD pipelines and other tooling which would require a non-zero exit code in order to know something happened. I can't think of a scenario where a non-zero exit would negatively effect the utility of someone just running the model checker as a model checker.

[raymyers]

I'm pondering whether it's better to make this a configuration option or not.

Understood. Whenever you've mulled it over I'm happy to update it to reflect the direction.

[eaon]

Traditionally model checkers are supposed to find failure cases and non-zero exit reads to me as the program failed to run correctly ...

I believe the semantics for return codes are down to the application itself, at least in practice. As an example, echo hi | grep bye will exit with return code 1, but for all intents and purposes, grep (probably) ran correctly. But I've definitely encountered commands that treat return codes like you describe, so likely just a matter of preference in the end.

PS: Loved the Strange Loop talk @mbellotti!