Where to put tests related to Lake

Stream: lean4 dev

[Maxwell Tang]

Hi, I'm working on a fix for an issue with Lean's TOML template.
Are tests necessary for this pull request?
If they are, where should they be placed and how should I run them? It seems like there are a bunch of tests for Lake at tests/lake/tests, but testing.md suggests that these aren't supported. Also, following testing.md,

# -R lake should filter for tests that are related to Lake.
ctest -R lake --output-on-failure --timeout 300

only runs 9 tests, so it seems Lake either doesn't have tests or I'm doing something wrong.

[Mac Malone]

Due to some flakiness issues, part of the Lake test suite is, by default, disabled. It can be re-enabled by uncommenting this line.