diff options
author | 2018-01-11 18:18:15 +0100 | |
---|---|---|
committer | 2018-01-11 18:18:15 +0100 | |
commit | 3815ec5405976196ff79b6960e65ce5adda66205 (patch) | |
tree | a9db7c4259f79a364cb15e41363a4d9fd11c2aad /test-suite | |
parent | 2202808309a6b307d327fd7c76da55b466166864 (diff) | |
parent | 25f910c9229218e08b1a4bbfa22c02fa43bb2394 (diff) |
Merge PR #6557: First stab at documenting the test suite.
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/README.md | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/test-suite/README.md b/test-suite/README.md new file mode 100644 index 000000000..1ec5d667e --- /dev/null +++ b/test-suite/README.md @@ -0,0 +1,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. |