Coq Test Suite

The test suite can be run from the Coq root directory by make test-suite. This does a clean step first, so if you've already run it, then change something, you'll have to do a lot of work again.

If you run make from the test-suite directory, there is no clean step. You can also run make aaa/bbb/ccc.v.log to build the log for one test, or make ddd where ddd is on of the sub-directories of test-suite to just build the logs for that directory. In these cases, a summary is not printed, but can be generated by make summary.

make -B can be used to rerun tests ( -B meaning always remake).

From the test-suite directory, make report (included in make all) prints a summary of which tests failed using the produced log files (this still works when only some tests are built as described above). Setting the PRINT_LOGS variable will make it print the logs of the failing tests.

For instance, running the following in the test-suite directory:

$ echo Fail. > success/fail.v # make some failing test

$ make
TEST      prerequisite/make_local.v
...
TEST      success/fail.v
...
BUILDING SUMMARY FILE
FAILURES
    success/fail.v...Error! (should be accepted)
Makefile:189: recipe for target 'all failed
make: *** [report] Error 1

$ make report PRINT_LOGS=1
BUILDING SUMMARY FILE
logs/success/fail.v.log
==========> TESTING success/fail.v <==========
Welcome to Coq (version information)
Skipping rcfile loading.
File "/path/to/success/fail.v", line 1, characters 4-5:
Error:
Syntax error: [vernac:Vernac.vernac_control] expected after 'Fail' (in [vernac:Vernac.vernac_control]).

0m0.000000s 0m0.000000s
0m0.040000s 0m0.000000s
==========> FAILURE <==========
    success/fail.v...Error! (should be accepted)

FAILURES
    success/fail.v...Error! (should be accepted)
Makefile:189: recipe for target 'report' failed
make: *** [report] Error 1

$ echo 'Comments "foo".' > success/fail.v

$ make
TEST      success/fail.v
BUILDING SUMMARY FILE
NO FAILURES

See test-suite/Makefile for more information.

Adding a test

Regression tests for closed bugs should be added to bugs/closed, as bug_1234.v where 1234 is the bug number. Files in this directory are tested for successful compilation. When you fix a bug, you should usually add a regression test here as well.

The error "(bug seems to be opened, please check)" when running make test-suite means that a test in bugs/closed failed to compile.

There are also output tests in output which consist of a .v file and a .out file with the expected output. Output tests in this directory are run with coqc in -test-mode. Output tests in output-coqtop work the same way, but are run with coqtop.

There are unit tests of OCaml code in unit-tests. These tests are contained in .ml files, and rely on the OUnit unit-test framework, as described at http://ounit.forge.ocamlcore.org/. Use make unit-tests in the unit-tests directory to run them.

Fixing output tests

When an output test output/foo.v fails, the output is stored in output/foo.out.real. Move that file to the reference file output/foo.out to update the test, approving the new output. Target approve-output will do this for all failing output tests automatically.

Don't forget to check the updated .out files into git!

Note that output/MExtraction.out is special: it is copied from micromega/micromega.ml in the plugin source directory. Automatic approval will incorrectly update the copy.