Adding tests

Stream: lean4 dev

[Joachim Breitner]

When I add a new test file to, say, tests/lean/run/foo.lean, what do I have to do to make ctest pick it up? All tests seem to be put into build/release/stage1/shell/CTestTestfile.cmake at some stage. Is there something better than rm-rf build to generate that file?

[Sebastian Ullrich]

make test should rerun cmake automatically I think

[Joachim Breitner]

Hmm, I thought I even ran cmake ../.. manually and it didn’t help. But somehow the test has appeared now. Odd.
But thanks, I’m unblocked until I can complain better.

[Sebastian Ullrich]

I don't think that reconfigures the CMake project in stage1/

[Joachim Breitner]

Classical case of “I thought I tried that”, but even running make in stage1 suffices:

~/build/lean/lean4 $ cp tests/lean/run/2810.lean tests/lean/run/2810-copy.lean
~/build/lean/lean4 $ ctest --test-dir ~/build/lean/lean4/build/release/stage1 -R 2810-copy
Internal ctest changing into directory: /home/jojo/build/lean/lean4/build/release/stage1
Test project /home/jojo/build/lean/lean4/build/release/stage1
No tests were found!!!
~/build/lean/lean4 $ make -C build/release/stage1 -j8
…
[100%] Built target lean
make: Verzeichnis „/home/jojo/build/lean/lean4/build/release/stage1“ wird verlassen
~/build/lean/lean4 $ ctest --test-dir ~/build/lean/lean4/build/release/stage1 -R 2810-copy
Internal ctest changing into directory: /home/jojo/build/lean/lean4/build/release/stage1
Test project /home/jojo/build/lean/lean4/build/release/stage1
    Start 738: leanruntest_2810-copy.lean
1/1 Test #738: leanruntest_2810-copy.lean .......   Passed    0.11 sec

100% tests passed, 0 tests failed out of 1

Total Test time (real) =   0.14 sec

[Joachim Breitner]

Left a short note at the documentation: https://github.com/leanprover/lean4/pull/2815
(Are those super-trivial PRs welcome?)