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
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
|
# 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.
|
