You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

3.7 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:

    • has small unit tests for type-checking of System F terms
    • has small unit tests for ML programs
    • 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 To work with suite.t, we recommend reading the dune documentation on Cram tests first.

Finally, performance benchmarks are included in 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 midml program

[midml.ML] is a very simple frontend program that parses, infers and type-checks a source file in the "mid-ML" language supported by our example client. You can run it to check small programs.

This program can be invoked using dune. You can refer to it using either its internal path, client/bin/midml.exe, or its installation path, midml:

echo "let id = fun x -> x" > foo.midml
dune exec -- client/bin/midml.exe foo.midml
dune exec -- midml foo.midml

Running the benchmark

make bench

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.)