Skip to content

Latest commit

 

History

History
75 lines (58 loc) · 2.56 KB

README.md

File metadata and controls

75 lines (58 loc) · 2.56 KB
Raw

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 test-suite/bugs/closed, as 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 test-suite/output which consist of a .v file and a .out file with the expected output.