Zulip Chat Archive

Stream: mathlib4

Topic: Running a single test case?

Louis Cabarion (Oct 08 2025 at 16:10):

lake test runs the entire Mathlib test suite. Is there a way to run only a specific test within MathlibTest/?

Kenny Lau (Oct 08 2025 at 16:12):

lake build MathlibTest/modulename.lean

Louis Cabarion (Oct 08 2025 at 19:56):

Oh, so running a test is exactly the same as building the test case?

Last updated: Dec 20 2025 at 21:32 UTC