This exercise lets students implement a resolution prover to propositional logic that provides certificates (a series of resolution steps or a model) for its proofs. Instructions can be found here, exercise H9.2, and some optimisations submitted by our students and further discussion can be found here.
Tests are run using stack.
The executables specified in test.cabal expect the solution repository checked out in the solution subdirectory and the submission checked out in the assignment subdirectory.
Moreover, test.cabal provides an executable to test the template repository locally.
For this, it expects the template repository in the template subdirectory.
Refer to test.cabal for detailed information about the targets and flags provided.
You can run executables specified in test.cabal using stack run <executableName>.
By default, Artemis runs ./run.sh -s to execute the tests.
You can modify run.sh to adapt the build and test process.