fix: avoid unnecessary error throwing

[Paul-Lez]

This PR changes the behaviour of the safe_verify binary to avoid throwing an error if the check was run successfully but the solution file didn't pass the check. The proposal is the following: we should keep error throwing for cases where the user input is ill-formed, and communicate failure in passing the check in some other way (e.g. in the output that is printed). This ensures that a Json output file can always be created (currently this is only created when the check succeeds, which does make it a little less useful!).

As a drive-by, the logging is now done using IO.eprintln rather than IO.println.

[GasStationManager]

Thanks for the PR!

I agree that we should provide informative output text (or JSON). However, at the same time I would also prefer to emit a nonzero exit code when check fails. Part of the reason is that this makes downstream scripts (eg. in CI) easier to check for the outcomes (and this is in line with other tools in this space including lean4checker and comparator).

If you prefer, we could even emit different nonzero exit codes for check fails vs other errors.

Could we output the JSON file, and then throw an error if there was a failure?
A complication is that some checks (notably the Environment.replay call), will emit exceptions for check failures. Can we catch the exception, do the output to file, then throw?

[Paul-Lez]

@GasStationManager That's a good point! I've fixed this so that it still throws an error but saves JSON first. For the environment replay errors, I could address those in another PR (I have another one coming that makes most of Main.lean monadic, so merging that one first will probably make such refactors easier to handle cleanly)

[GasStationManager]

Superseded by #21, which rebases this onto current main (post security hardening). Merged.