search

metamath / metamath-knife

Metamath-knife can rapidly verify Metamath proofs, providing strong confidence that the proofs are correct.
Apache License 2.0
25 stars 9 forks source link

always report all errors #108

Closed digama0 closed 1 year ago

digama0 commented 1 year ago

As pointed out in https://github.com/david-a-wheeler/metamath-knife/pull/107#discussion_r1181545930, if you use the command line options to e.g. enable the verify pass but not the scope pass, the errors from the scope pass will not be reported (and this could potentially make the program report no errors and give an OK error code even though there were errors).

In this PR we simplify the interface to eliminate the DiagnosticClass enum to filter error results and always report errors from all passes that have been run (and by selecting different options you change which passes run).

david-a-wheeler commented 1 year ago

We definitely want to report all errors!

tirix commented 1 year ago

We definitely want to report all errors!

Don't worry, we will still report all errors in case the --verify command is used, as before.

digama0 commented 1 year ago

And also, the original call was reporting all errors in the case of calling --verify, since the scope check was always enabled. The cases where not all errors are reported are for either obscure commands or things that weren't possible without using the discouraged and axiom_use commands at the same time as e.g. a verify run.