feat: rewrite set_option style linter in lean

Unlike the Python version, this script also supports set_option tactics
and terms.

Mathlib.lean

@@ -3767,6 +3767,7 @@ import Mathlib.Tactic.Linarith.Verification
 import Mathlib.Tactic.LinearCombination
 import Mathlib.Tactic.Linter
 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

@@ -113,6 +113,7 @@ import Mathlib.Tactic.Linarith.Verification
 import Mathlib.Tactic.LinearCombination
 import Mathlib.Tactic.Linter
 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,7 +2,7 @@
 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.
 -/

Mathlib/Tactic/Linter/Style.lean

@@ -0,0 +1,69 @@
+/-
+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.Style.SetOption
+
+/-- Whether a syntax element is a `set_option` call:
+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
+
+/-- 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"
+}
+
+/-- 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
+    match stx.findStack? (fun _ ↦ true) is_set_option with
+    | some ((head, _n)::_chain) =>
+      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"
+    | _ => return
+
+initialize addLinter setOptionLinter
+
+end Mathlib.Linter.Style.SetOption

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_IBY = 11 # isolated by
@@ -142,20 +141,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 = []
@@ -373,8 +358,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:
@@ -410,7 +393,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,
                             nonterminal_simp_check]:
             errs, newlines = error_check(newlines, path)

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