First stab at documenting the test suite.

1 files changed, 17 insertions, 0 deletions

diff --git a/test-suite/README.md b/test-suite/README.md
new file mode 100644
index 000000000..30a71ed87
--- /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.
+