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
|
# 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.
There are unit tests of OCaml code in `test-suite/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.
|
