From 5c2292a9238a669a83442ff333bc93b529325291 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 4 Dec 2023 11:29:49 +0100 Subject: [PATCH] doc: In testing doc, suggest `make` to pick up new tests (#2815) --- doc/dev/testing.md | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/doc/dev/testing.md b/doc/dev/testing.md index 3c4fb197c5..b4ec0658a5 100644 --- a/doc/dev/testing.md +++ b/doc/dev/testing.md @@ -5,7 +5,6 @@ After [building Lean](../make/index.md) you can run all the tests using cd build/release make test ARGS=-j4 ``` - Change the 4 to the maximum number of parallel tests you want to allow. The best choice is the number of CPU cores on your machine as the tests are mostly CPU bound. You can find the number of processors @@ -17,6 +16,12 @@ adding the `-C stageN` argument. The default when run as above is stage 1. The Lean tests will automatically use that stage's corresponding Lean executables +Runnign `make test` will not pick up new test files; run +```bash +cmake build/release/stage1 +``` +to update the list of tests. + You can also use `ctest` directly if you are in the right folder. So to run stage1 tests with a 300 second timeout run this: @@ -24,6 +29,9 @@ to run stage1 tests with a 300 second timeout run this: cd build/release/stage1 ctest -j 4 --output-on-failure --timeout 300 ``` +Useful `ctest` flags are `-R ` to run a single test, and +`--rerun-failed` to run all tests that failed during the last run. +You can also pass `ctest` flags via `make test ARGS="--rerun-failed"`. To get verbose output from ctest pass the `--verbose` command line option. Test output is normally suppressed and only summary