Regression tests
Celf has the ability to check multiple files without producing any output, which is helpful for quickly checking lots of Celf code for errors or changes in the behavior of Celf. Celf's regression testing infrastructure is invoked by passing "regression" as the first argument to Celf. For instance, the following command
$ ./celf regression tests/sources.test
will check most of the files in the tests directory.
Multiple .test files are fine: ./celf regression foo.test bar.test baz.test will run all the tests in foo.test, bar.test, and baz.test and will generate a single report for all the tests in the three files.
The following is an example .test file:
# Some tests
success alloc-sem.clf
success arith.clf # Note
# Some other tests
success atp.clf
modeErr -d bigstep.clf # double-check!
parseErr ccc.clf
Anything on a line after the # character is treated as whitespace, and every line must be either entirely whitespace or must have the format <outcome> <arguments to celf>. Any valid command-line arguments to Celf can be given. For instance, the -d on the next-to-last line tells Celf to double-check that reconstructed terms have valid types (this double check is done automatically for tests that have the outcome success).
Filenames are relative to the directory where the relevant .test file lives (as opposed to the directory where the Celf binary lives or the directory you were in when you ran celf regression ...).
The following are valid outcomes; they are somewhat ad-hoc, as they are mostly based off of which kind of exception is thrown in what place within the implementation.
-
ambigType- expect a failure to determine the type of some free variable -
generalErr- "general errors" (raised for random things like duplicate mode declarations and malformed queries) -
kindErr- expect a kind error -
modeErr- expect a mode error -
parseErr- expect the file to not even parse -
queryFailed- expect a query to fail -
success- expect no errors -
typeErr- expect a type error -
undeclId- expect an undeclared identifier error
There are two other kinds of outcomes that cannot be specified in a .test file. The first is an error from an unexpected source, such as Fail, which generally indicates the violation of an internal invariant in Celf. The second is a file that has the outcome success but that then, when rerun with the -d option, has some other outcome. This "double-checking" failure should never happen and so will always be treated as an unexpected outcome by the Celf regression tester.