feat: rewrite set_option style linter in lean (#12928)

Unlike the Python version, this script also supports set_option tactics and terms, and we add a couple of tests.

Mathlib.lean

@@ -3888,6 +3888,7 @@ import Mathlib.Tactic.Linter
 import Mathlib.Tactic.Linter.GlobalAttributeIn
 import Mathlib.Tactic.Linter.HashCommandLinter
 import Mathlib.Tactic.Linter.Lint
+import Mathlib.Tactic.Linter.Style
 import Mathlib.Tactic.Measurability
 import Mathlib.Tactic.Measurability.Init
 import Mathlib.Tactic.MkIffOfInductiveProp

Mathlib/Tactic.lean

@@ -117,6 +117,7 @@ import Mathlib.Tactic.Linter
 import Mathlib.Tactic.Linter.GlobalAttributeIn
 import Mathlib.Tactic.Linter.HashCommandLinter
 import Mathlib.Tactic.Linter.Lint
+import Mathlib.Tactic.Linter.Style
 import Mathlib.Tactic.Measurability
 import Mathlib.Tactic.Measurability.Init
 import Mathlib.Tactic.MkIffOfInductiveProp

Mathlib/Tactic/Linter.lean

@@ -2,11 +2,12 @@
 This is the `Linter`s file: it only imports files defining linters and is
 intended to be imported fairly early in `Mathlib`.
 
-This file is ignored by `Shake`:
+This file is ignored by `shake`:
 * it is in `ignoreAll`, meaning that all its imports are considered necessary;
 * it is in `ignoreImport`, meaning that where it is imported, it is considered necessary.
 -/
 
 import Mathlib.Tactic.Linter.GlobalAttributeIn
 import Mathlib.Tactic.Linter.HashCommandLinter
 import Mathlib.Tactic.Linter.Lint
+import Mathlib.Tactic.Linter.Style

Mathlib/Tactic/Linter/Style.lean

@@ -0,0 +1,72 @@
+/-
+Copyright (c) 2024 Michael Rothgang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michael Rothgang
+-/
+
+import Lean.Elab.Command
+import Lean.Linter.Util
+
+/-!
+## Style linters
+
+This file contains (currently one, eventually more) linters about stylistic aspects:
+these are only about coding style, but do not affect correctness nor global coherence of mathlib.
+
+Historically, these were ported from the `lint-style.py` Python script.
+-/
+
+open Lean Elab Command
+
+namespace Mathlib.Linter
+
+/-- The `setOption` linter emits a warning on a `set_option` command, term or tactic
+which sets a `pp`, `profiler` or `trace` option. -/
+register_option linter.setOption : Bool := {
+  defValue := true
+  descr := "enable the `setOption` linter"
+}
+
+namespace Style.SetOption
+
+/-- Whether a syntax element is a `set_option` command, tactic or term:
+Return the name of the option being set, if any. -/
+def parse_set_option : Syntax → Option (Ident)
+  -- This handles all four possibilities of `_val`: a string, number, `true` and `false`.
+  | `(command|set_option $name:ident $_val) => some name
+  | `(set_option $name:ident $_val in $_x) => some name
+  | `(tactic|set_option $name:ident $_val in $_x) => some name
+  | _ => none
+
+/-- Whether a given piece of syntax is a `set_option` command, tactic or term. -/
+def is_set_option : Syntax → Bool :=
+  fun stx ↦ parse_set_option stx matches some _name
+
+/-- Gets the value of the `linter.setOption` option. -/
+def getLinterHash (o : Options) : Bool := Linter.getLinterValue linter.setOption o
+
+/-- The `setOption` linter: this lints any `set_option` command, term or tactic
+which sets a `pp`, `profiler` or `trace` option.
+
+**Why is this bad?** These options are good for debugging, but should not be
+used in production code.
+**How to fix this?** Remove these options: usually, they are not necessary for production code.
+(Some tests will intentionally use one of these options; in this case, simply allow the linter.)
+-/
+def setOptionLinter : Linter where run := withSetOptionIn fun stx => do
+    unless getLinterHash (← getOptions) do
+      return
+    if (← MonadState.get).messages.hasErrors then
+      return
+    if let some (head) := stx.find? is_set_option then
+      if let some (name) := parse_set_option head then
+        -- Drop a leading backtick.
+        let name := (toString name).drop 1
+        if name.startsWith "pp." || name.startsWith "profiler." || name.startsWith "trace." then
+          Linter.logLint linter.setOption head m!"Forbidden set_option `{name}`; please remove"
+
+initialize addLinter setOptionLinter
+
+end Style.SetOption
+
+end Mathlib.Linter

scripts/lint-style.py

@@ -40,7 +40,6 @@
 ERR_COP = 0 # copyright header
 ERR_MOD = 2 # module docstring
 ERR_LIN = 3 # line length
-ERR_OPT = 6 # set_option
 ERR_AUT = 7 # malformed authors list
 ERR_TAC = 9 # imported Mathlib.Tactic
 ERR_TAC2 = 10 # imported Lake in Mathlib
@@ -148,20 +147,6 @@ def annotate_strings(enumerate_lines):
                 continue
         yield line_nr, line, *rem, False
 
-def set_option_check(lines, path):
-    errors = []
-    newlines = []
-    for line_nr, line, in_comment, in_string in annotate_strings(annotate_comments(lines)):
-        if line.strip().startswith('set_option') and not in_comment and not in_string:
-            option_prefix = line.strip().split(' ', 2)[1].split('.', 1)[0]
-            # forbidden options: pp, profiler, trace
-            if option_prefix in {'pp', 'profiler', 'trace'}:
-                errors += [(ERR_OPT, line_nr, path)]
-                # skip adding this line to newlines so that we suggest removal
-                continue
-        newlines.append((line_nr, line))
-    return errors, newlines
-
 def line_endings_check(lines, path):
     errors = []
     newlines = []
@@ -392,8 +377,6 @@ def format_errors(errors):
             output_message(path, line_nr, "ERR_MOD", "Module docstring missing, or too late")
         if errno == ERR_LIN:
             output_message(path, line_nr, "ERR_LIN", "Line has more than 100 characters")
-        if errno == ERR_OPT:
-            output_message(path, line_nr, "ERR_OPT", "Forbidden set_option command")
         if errno == ERR_AUT:
             output_message(path, line_nr, "ERR_AUT", "Authors line should look like: 'Authors: Jean Dupont, Иван Иванович Иванов'")
         if errno == ERR_TAC:
@@ -433,7 +416,6 @@ def lint(path, fix=False):
                             four_spaces_in_second_line,
                             long_lines_check,
                             isolated_by_dot_semicolon_check,
-                            set_option_check,
                             left_arrow_check,
                             adaptation_note_check,
                             nonterminal_simp_check]:

test/Explode.lean

@@ -24,6 +24,7 @@ info: true_iff : ∀ (p : Prop), (True ↔ p) = p
 -/
 #guard_msgs in #explode true_iff
 
+set_option linter.setOption false
 -- On command line, tests format functions with => rather than ↦ without this.
 set_option pp.unicode.fun true
 

test/LibrarySearch/IsCompact.lean

@@ -1,8 +1,6 @@
 import Mathlib.Topology.Instances.Real
 import Mathlib.Topology.Algebra.Order.Compact
 
-set_option pp.unicode.fun true
-
 -- TODO: uses sorry, but is hidden behind the `apply?`
 /-- warning: declaration uses 'sorry' -/
 #guard_msgs(warning, drop info) in

test/LibrarySearch/basic.lean

@@ -6,6 +6,7 @@ import Mathlib.Data.Real.Basic
 
 set_option autoImplicit true
 
+set_option linter.setOption false
 -- Enable this option for tracing:
 -- set_option trace.Tactic.librarySearch true
 -- And this option to trace all candidate lemmas before application.

test/Recall.lean

@@ -3,6 +3,7 @@ import Mathlib.Analysis.Calculus.Deriv.Basic
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
 import Mathlib.Data.Complex.Exponential
 
+set_option linter.setOption false
 -- Remark: When the test is run by make/CI, this option is not set, so we set it here.
 set_option pp.unicode.fun true
 set_option autoImplicit true

test/delabLinearIndependent.lean

@@ -1,5 +1,6 @@
 import Mathlib.LinearAlgebra.LinearIndependent
 
+set_option linter.setOption false
 set_option pp.unicode.fun true
 
 variable {K V : Type*} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} {x : V}

test/lint_style.lean

@@ -0,0 +1,108 @@
+import Mathlib.Tactic.Linter.Style
+import Mathlib.Tactic.Common
+
+/-! Tests for all the style linters. -/
+
+/-! Tests for the `setOption` linter -/
+section setOption
+
+-- The warning generated by `linter.setOption` is not suppressed by `#guard_msgs`,
+-- because the linter is run on `#guard_msgs` itself. This is a known issue, see e.g.
+-- https://leanprover.zulipchat.com/#narrow/stream/348111-batteries/topic/unreachableTactic.20linter.20not.20suppressed.20by.20.60.23guard_msgs.60
+-- We jump through an extra hoop here to silence the warning.
+
+-- All types of options are supported: boolean, numeric and string-valued.
+-- On the top level, i.e. as commands.
+
+set_option linter.setOption false in
+/--
+warning: Forbidden set_option `pp.all`; please remove
+note: this linter can be disabled with `set_option linter.setOption false`
+-/
+#guard_msgs in
+set_option linter.setOption true in
+set_option pp.all true
+
+set_option linter.setOption false in
+/--
+warning: Forbidden set_option `pp.all`; please remove
+note: this linter can be disabled with `set_option linter.setOption false`
+-/
+#guard_msgs in
+set_option linter.setOption true in
+set_option pp.all false
+
+set_option linter.setOption false in
+/--
+warning: Forbidden set_option `pp.raw.maxDepth`; please remove
+note: this linter can be disabled with `set_option linter.setOption false`
+-/
+#guard_msgs in
+set_option linter.setOption true in
+set_option pp.raw.maxDepth 32
+
+set_option linter.setOption false in
+/--
+warning: Forbidden set_option `trace.profiler.output`; please remove
+note: this linter can be disabled with `set_option linter.setOption false`
+-/
+#guard_msgs in
+set_option linter.setOption true in
+set_option trace.profiler.output "foo"
+
+-- The lint does not fire on arbitrary options.
+set_option autoImplicit false
+
+-- We also cover set_option tactics.
+
+set_option linter.setOption false in
+/--
+warning: Forbidden set_option `pp.all`; please remove
+note: this linter can be disabled with `set_option linter.setOption false`
+-/
+#guard_msgs in
+set_option linter.setOption true in
+lemma tactic : True := by
+  set_option pp.all true in
+  trivial
+
+set_option linter.setOption false in
+/--
+warning: Forbidden set_option `pp.raw.maxDepth`; please remove
+note: this linter can be disabled with `set_option linter.setOption false`
+-/
+#guard_msgs in
+set_option linter.setOption true in
+lemma tactic2 : True := by
+  set_option pp.raw.maxDepth 32 in
+  trivial
+
+set_option linter.setOption false in
+/--
+warning: Forbidden set_option `pp.all`; please remove
+note: this linter can be disabled with `set_option linter.setOption false`
+-/
+#guard_msgs in
+set_option linter.setOption true in
+lemma tactic3 : True := by
+  set_option pp.all false in
+  trivial
+
+set_option linter.setOption false in
+/--
+warning: Forbidden set_option `trace.profiler.output`; please remove
+note: this linter can be disabled with `set_option linter.setOption false`
+-/
+#guard_msgs in
+set_option linter.setOption true in
+lemma tactic4 : True := by
+  set_option trace.profiler.output "foo" in
+  trivial
+
+-- This option is not affected, hence does not throw an error.
+set_option autoImplicit true in
+lemma foo' : True := trivial
+
+-- TODO: add terms for the term form
+
+end setOption

test/vec_notation.lean

@@ -8,6 +8,7 @@ open Lean
 open Lean.Meta
 open Qq
 
+set_option linter.setOption false in
 set_option pp.unicode.fun false
 
 /-! These tests are testing `PiFin.toExpr` and fail with