Skip to content

Commit cc89a85

Browse files
authored
doc: note that tests/lean/run disables linters (#11595)
This PR documents that tests in `tests/lean/run/` run with `-Dlinter.all=false`, and explains how to enable specific linters when testing linter behavior. 🤖 Prepared with Claude Code
1 parent 1c1bd8e commit cc89a85

File tree

1 file changed

+4
-0
lines changed

1 file changed

+4
-0
lines changed

doc/dev/testing.md

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -51,6 +51,10 @@ All these tests are included by [src/shell/CMakeLists.txt](https://github.com/le
5151
codes and do not check the expected output even though output is
5252
produced, it is ignored.
5353

54+
**Note:** Tests in this directory run with `-Dlinter.all=false` to reduce noise.
55+
If your test needs to verify linter behavior (e.g., deprecation warnings),
56+
explicitly enable the relevant linter with `set_option linter.<name> true`.
57+
5458
- [`tests/lean/interactive`](https://github.com/leanprover/lean4/tree/master/tests/lean/interactive/): are designed to test server requests at a
5559
given position in the input file. Each .lean file contains comments
5660
that indicate how to simulate a client request at that position.

0 commit comments

Comments
 (0)