# Coq Test Suite

The test suite can be run from the Coq root directory by `make test-suite`.
However, for incremental test suite builds, we recommend running `make`
from the test-suite directory (or with `make -C test-suite`).
This Makefile is compatible with both Dune
and legacy hybrid builds.

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`](Makefile) for more information.

## Adding a test

Regression tests for closed bugs should be added to
[`bugs`](bugs), 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`](bugs) failed to
compile.

There are also output tests in [`output`](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`](output-coqtop)
work the same way, but are run with coqtop.

There are unit tests of OCaml code in [`unit-tests`](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`](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`](../plugins/micromega/micromega.ml) in the plugin
source directory. Automatic approval will incorrectly update the copy.