From 8c1aa693f718414bba8cd1400d2b49ff39eeb828 Mon Sep 17 00:00:00 2001 From: Jasper Hugunin Date: Sat, 6 Jan 2018 21:40:02 +0900 Subject: First stab at documenting the test suite. --- test-suite/README.md | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 test-suite/README.md (limited to 'test-suite') diff --git a/test-suite/README.md b/test-suite/README.md new file mode 100644 index 0000000000..30a71ed87e --- /dev/null +++ b/test-suite/README.md @@ -0,0 +1,17 @@ +# Coq Test Suite + +The test suite can be run from the root directory by `make test-suite`. + +From this directory, `make aaa/bbb/ccc.v.log` runs one test (if not already run), storing the output in the named `.log` file. +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. + -- cgit v1.2.3 From 2a483f7c7ef7ac0cecaef48b3bad3920cea31bb5 Mon Sep 17 00:00:00 2001 From: Jasper Hugunin Date: Sun, 7 Jan 2018 00:54:04 +0900 Subject: Mention -B argument of make to rerun tests --- test-suite/README.md | 1 + 1 file changed, 1 insertion(+) (limited to 'test-suite') diff --git a/test-suite/README.md b/test-suite/README.md index 30a71ed87e..159697a7e1 100644 --- a/test-suite/README.md +++ b/test-suite/README.md @@ -3,6 +3,7 @@ The test suite can be run from the root directory by `make test-suite`. From this directory, `make aaa/bbb/ccc.v.log` runs one test (if not already run), storing the output in the named `.log` file. +`make -B` can be used to rerun the test (`-B` meaning always remake). See [`test-suite/Makefile`](/test-suite/Makefile) for more information. ## Adding a test -- cgit v1.2.3 From 2e0b408b69d40ab457c998854e43d0b60dd1c68b Mon Sep 17 00:00:00 2001 From: Jasper Hugunin Date: Wed, 10 Jan 2018 12:39:09 +0900 Subject: Add comments by @psteckler to test-suite/README.md --- test-suite/README.md | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) (limited to 'test-suite') diff --git a/test-suite/README.md b/test-suite/README.md index 159697a7e1..2e288ff730 100644 --- a/test-suite/README.md +++ b/test-suite/README.md @@ -1,9 +1,18 @@ # Coq Test Suite -The test suite can be run from the root directory by `make 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. +Logs are stored in said `.log` file. +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 this directory, `make aaa/bbb/ccc.v.log` runs one test (if not already run), storing the output in the named `.log` file. -`make -B` can be used to rerun the test (`-B` meaning always remake). See [`test-suite/Makefile`](/test-suite/Makefile) for more information. ## Adding a test -- cgit v1.2.3 From 25f910c9229218e08b1a4bbfa22c02fa43bb2394 Mon Sep 17 00:00:00 2001 From: Jasper Hugunin Date: Thu, 11 Jan 2018 12:04:48 +0900 Subject: Lint and remove redundant line --- test-suite/README.md | 2 -- 1 file changed, 2 deletions(-) (limited to 'test-suite') diff --git a/test-suite/README.md b/test-suite/README.md index 2e288ff730..1ec5d667e9 100644 --- a/test-suite/README.md +++ b/test-suite/README.md @@ -8,7 +8,6 @@ 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. -Logs are stored in said `.log` file. 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). @@ -24,4 +23,3 @@ 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. - -- cgit v1.2.3