max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: In testing doc, suggest make to pick up new tests (#2815)

Browse source
This commit is contained in:
Joachim Breitner 2023-12-04 11:29:49 +01:00 • committed by GitHub
parent 14296ae720
commit 5c2292a923
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 9 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
doc/dev/testing.md
View file

@ -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 <name of test>` 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