From cc89a853e57726577a2357c161d4991476ff5050 Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Thu, 11 Dec 2025 12:33:07 +1100 Subject: [PATCH] doc: note that tests/lean/run disables linters (#11595) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- doc/dev/testing.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/doc/dev/testing.md b/doc/dev/testing.md index ed2efc1bb5..abb11ef263 100644 --- a/doc/dev/testing.md +++ b/doc/dev/testing.md @@ -51,6 +51,10 @@ All these tests are included by [src/shell/CMakeLists.txt](https://github.com/le codes and do not check the expected output even though output is produced, it is ignored. + **Note:** Tests in this directory run with `-Dlinter.all=false` to reduce noise. + If your test needs to verify linter behavior (e.g., deprecation warnings), + explicitly enable the relevant linter with `set_option linter. true`. + - [`tests/lean/interactive`](https://github.com/leanprover/lean4/tree/master/tests/lean/interactive/): are designed to test server requests at a given position in the input file. Each .lean file contains comments that indicate how to simulate a client request at that position.