How to run and add tests to Personoj

This guide shows you how to run the test suites of Personoj and how to add new tests to these test suites.

How to run the test suites

Run the unit tests:

$ cd tests/unit_tests
$ pvs -raw -L test.lisp -E '(runall) (uiop:quit)'

Translate and typecheck a portion of the prelude of PVS (requires Lambdapi with the encodings installed):

$ cd tests/prelude
$ pvs -raw -L test.lisp -E '(runall :without-proof-p t) (uiop:quit)'

If you have updated Personoj, you may have to correct some unit tests. To update the test, say, eqtype:

Run the test:

$ pvs -raw -L test.lisp -E '(runtest "eqtype")'

Review the diff between the output of Personoj and the current eqtype.lp.expected that is displayed. Answer y to apply the displayed patch to eqtype.lp.expected, or n to do nothing.

If you want to add a new test:

cd tests/unit_tests/
Write some PVS you want to translate in a new theory inside the file simple.pvs
In test.lisp, add the name of your new theory to the list *theories*.
Run the new test as described above, and apply the diff by answering y.

If a theory, say real_defs is not translated when running the prelude test and you want to test it,

Find its corresponding section in theories.json

{
 	 "name": "real_defs",
 	 "disabled": true,
 	 "comments": "...",
  }

Switch "disabled" from true to false (or remove the line)

{
 	 "name": "real_defs",
 	 "disabled": false,
 	 "comments": "...",
}

For more information about the file theories.json, see the documentation of tests/prelude/test.lisp.