fix: disable linters in tests

doc/examples/test_single.sh

@@ -1,4 +1,4 @@
 #!/usr/bin/env bash
 source ../../tests/common.sh
 
-exec_check lean -j 0 "$f"
+exec_check lean -j 0 -Dlinter.nolint=true "$f"

tests/compiler/test_single_interpret.sh

@@ -1,5 +1,5 @@
 #!/usr/bin/env bash
 source ../common.sh
 
-exec_check lean --run "$f"
+exec_check lean -Dlinter.nolint=true --run "$f"
 diff_produced

tests/lean/interactive/test_single.sh

@@ -6,5 +6,5 @@ source ../../common.sh
 export ASAN_OPTIONS=detect_leaks=0
 
 # these tests don't have to succeed
-exec_capture lean --run run.lean "$f" || true
+exec_capture lean -Dlinter.nolint=true --run run.lean "$f" || true
 diff_produced

tests/lean/run/test_single.sh

@@ -1,4 +1,4 @@
 #!/usr/bin/env bash
 source ../../common.sh
 
-exec_check lean -j 0 "$f"
+exec_check lean -j 0 -Dlinter.nolint=true "$f"

tests/lean/server/diags.lean

@@ -2,7 +2,7 @@ import Lean.Data.Lsp
 open IO Lean Lsp
 
 def main : IO Unit := do
-  Ipc.runWith (←IO.appPath) #["--server"] do
+  Ipc.runWith (←IO.appPath) #["--server", "-Dlinter.nolint=true"] do
     let hIn ← Ipc.stdin
     hIn.write (←FS.readBinFile "init_vscode_1_47_2.log")
     hIn.flush

tests/lean/server/test_single.sh

@@ -1,4 +1,4 @@
 #!/usr/bin/env bash
 source ../../common.sh
 
-exec_check lean -j 0 --run "$f"
+exec_check lean -j 0 -Dlinter.nolint=true --run "$f"

tests/lean/test_single.sh

@@ -2,5 +2,5 @@
 source ../common.sh
 
 # these tests don't have to succeed
-exec_capture lean -DprintMessageEndPos=true "$f" || true
+exec_capture lean -DprintMessageEndPos=true -Dlinter.nolint=true "$f" || true
 diff_produced

tests/lean/trust0/test_single.sh

@@ -1,4 +1,4 @@
 #!/usr/bin/env bash
 source ../../common.sh
 
-exec_check lean -t0 "$f"
+exec_check lean -t0 -Dlinter.nolint=true "$f"

tests/plugin/test_single.sh

@@ -3,5 +3,5 @@ source ../common.sh
 
 compile_lean -shared -o "${f%.lean}.so"
 expected_ret=1
-exec_check lean --plugin="${f%.lean}.so" "$f"
+exec_check lean -Dlinter.nolint=true --plugin="${f%.lean}.so" "$f"
 diff_produced