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. --- CONTRIBUTING.md | 2 ++ dev/ci/README.md | 2 ++ test-suite/README.md | 17 +++++++++++++++++ 3 files changed, 21 insertions(+) create mode 100644 test-suite/README.md diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 37b556c553..1a769333cc 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -28,6 +28,8 @@ Please make pull requests against the `master` branch. It's helpful to run the Coq test suite with `make test-suite` before submitting your change. Travis CI runs this test suite and a much larger one including external Coq developments on every pull request, but these results take significantly longer to come back (on the order of a few hours). Running the test suite locally will take somewhere around 10-15 minutes. Refer to [`dev/ci/README.md`](/dev/ci/README.md#information-for-developers) for more information on Travis CI tests. +If your pull request fixes a bug, please consider adding a regression test as well. See [`test-suite/README.md`](/test-suite/README.md) for how to do so. + Don't be alarmed if the pull request process takes some time. It can take a few days to get feedback, approval on the final changes, and then a merge. Coq doesn't release new versions very frequently so it can take a few months for your change to land in a released version. That said, you can start using the latest Coq `master` branch to take advantage of all the new features, improvements, and fixes. Here are a few tags Coq developers may add to your PR and what they mean. In general feedback and requests for you as the pull request author will be in the comments and tags are only used to organize pull requests. diff --git a/dev/ci/README.md b/dev/ci/README.md index f4423558cc..bb13587e94 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -103,6 +103,8 @@ The process to merge your PR is then to submit PRs to the external development repositories, merge the latter first (if the fixes are backward-compatible), drop the overlay commit and merge the PR on Coq then. +See also [`test-suite/README.md`](/test-suite/README.md) for information about adding new tests to the test-suite. + Travis specific information --------------------------- 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(+) 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(-) 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(-) 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