# 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`](/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.