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:

```bash $ 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 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.

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.