3.2 KiB
Testing Inferno
The inferno codebases uses different kinds of tests:
-
We used to have server-only tests, but we don't have any right now. Those could go in
src/test
. -
The example client has tests in
client/test
:- TestF.ml has small unit tests for type-checking of System F terms
- TestML.ml has small unit tests for ML programs
- TestMLRandom.ml performs property-based testing on a small fragment of the client language (we don't know how to generate pattern-matching code randomly).
- [suite.t/run.t][] uses dune Cram tests for more unit tests of ML programs, including failure scenarios.
Cram tests provide a readable way to specify test outcomes, and they encourage us to develop a user-friendly binary frontend for the client. Future ML unit tests should go to suite.t rather than TestML.ml. To work with suite.t, we recommend reading the dune documentation on Cram tests first.
Finally, performance benchmarks are included in BenchMLRandom.ml. It is a good idea to run them to evaluate changes that have a potential for degrading performances.
Running tests
Some tests are rather slow, so we have a "fast" and "slow" mode to run the tests. The "fast" tests should be pleasant to use during interactive edit-test loops, a few seconds at most. The "slow" tests currently take about 30s on a typical machine.
You can run tests using either make
or dune
. Using the makefile:
make quick # only the fast tests
make test # all tests
Using dune:
INFERNO_SLOW_TESTS=0 dune runtest # only the fast tests
dune runtest # all tests
Note that dune
runs tests incrementally: it will only re-run tests
that depend on code that has changed. If you want to run all tests
each time, use dune runtest --force
. The Makefile rules pass
--force
by default.
Running individual tests
You can run each test individually. (You may want to pass --force
if the code has not changed.)
dune exec client/test/TestF.exe
dune exec client/test/TestML.exe
dune exec client/test/TestMLRandom.exe # consider passing INFERNO_SLOW_TESTS=0
The dune invocation is a bit different from cram tests:
dune build @client/test/suite
Note that this command shows nothing if the tests pass. If you are not sure it tests as expected, go break the suite.t testsuite and see what happens :-)
Promoting cram tests
Cram tests compare the current behavior with a pre-recorded reference output. If the output of a test changes, but the change is correct/expected, you can fix the test automatically by running
dune promote
which will update the reference output with the current behavior.
For more details, see the dune documentation.
Running the benchmark
make benchmark
will print performance statistics. If you do a performance-impacting change, you are expected to run the benchmark before and after, and compare the results by yourself. (Merge Requests to make this more convenient are of course welcome.)