What is wrong
Currently, regression tests rely on both Minisat and SPASS. The regression test suite thus reports 8 total failures when run on a freshly cloned repository:
2 reported failures are from book code examples that are meant to raise errors.
1 reported failure is due to proof search failing when using a build generated by SML/NJ. This failure is not due to problems with Athena, rather, the non-deterministic nature of proof search procedures, possible timeouts, etc.
1 reported failure is due to missing the minisat_out.txt file in the ATHENA_HOME directory.
The other four failures are due to external calls to either Minisat or SPASS, which fail when they have not been installed.
How to fix
First, we will remove the intentionally incorrect code examples since they are meant for pedagogical purposes. Later, we might add to the python regression script an ability to expect an error from the Athena proof-checking.
Next, we will add to the regression testing script(s) an initial procedure that checks for Minisat and SPASS in the user's path. If Minisat is present, the original tests will be used, otherwise, it will trigger equivalent tests that use an Athena-native sat procedure. If SPASS is absent, tests that rely on SPASS will simply be skipped.
What is wrong
Currently, regression tests rely on both Minisat and SPASS. The regression test suite thus reports 8 total failures when run on a freshly cloned repository:
2 reported failures are from
bookcode examples that are meant to raise errors.1 reported failure is due to proof search failing when using a build generated by SML/NJ. This failure is not due to problems with Athena, rather, the non-deterministic nature of proof search procedures, possible timeouts, etc.
1 reported failure is due to missing the
minisat_out.txtfile in theATHENA_HOMEdirectory.The other four failures are due to external calls to either Minisat or SPASS, which fail when they have not been installed.
How to fix
First, we will remove the intentionally incorrect code examples since they are meant for pedagogical purposes. Later, we might add to the python regression script an ability to expect an error from the Athena proof-checking.
Next, we will add to the regression testing script(s) an initial procedure that checks for Minisat and SPASS in the user's path. If Minisat is present, the original tests will be used, otherwise, it will trigger equivalent tests that use an Athena-native
satprocedure. If SPASS is absent, tests that rely on SPASS will simply be skipped.