make test for specific tests

Stream: lean4 dev

[Alexander Bentkamp]

How do I run a specific test instead of running all tests with make test?

[Sebastian Ullrich]

See ctest -R. Not sure I ever tried, but make test ARGS="-R foo" should be equivalent

[Alexander Bentkamp]

lean4/build/release$ ctest -R leancomptest_534.lean
Test project /home/alex/Projects/test/lean4/build/release
No tests were found!!!

Maybe I have to call this from a different directory?

But make test ARGS="-R foo" works great!

[Henrik Böving]

I usually enter the stageN directory and run ctest there @Alexander Bentkamp

[Sebastian Ullrich]

See also https://lean-lang.org/lean4/doc/dev/testing.html. Which doesn't mention -R yet.

[Alexander Bentkamp]

Ah, that works, thanks!