blob: 1ec5d667e9d348885e09084568febb8b214e74cf (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
# 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).
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.
|
