chore: move linter.setOption to the style namespace (#16212)

Extracted from #15971.

Author: grunweg

Mathlib/Tactic/Linter/Style.lean

@@ -23,12 +23,12 @@ 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 := {
+register_option linter.style.setOption : Bool := {
   defValue := false
   descr := "enable the `setOption` linter"
 }
 
-namespace Style.SetOption
+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. -/
@@ -52,22 +52,22 @@ used in 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 Linter.getLinterValue linter.setOption (← getOptions) do
+    unless Linter.getLinterValue linter.style.setOption (← 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
         let forbidden := [`debug, `pp, `profiler, `trace]
         if forbidden.contains name.getRoot then
-          Linter.logLint linter.setOption head
+          Linter.logLint linter.style.setOption head
             m!"Setting options starting with '{"', '".intercalate (forbidden.map (·.toString))}' \
                is only intended for development and not for final code. \
                If you intend to submit this contribution to the Mathlib project, \
                please remove 'set_option {name}'."
 
 initialize addLinter setOptionLinter
 
-end Style.SetOption
+end Style.setOption
 
 end Mathlib.Linter

lakefile.lean

@@ -31,7 +31,7 @@ abbrev mathlibOnlyLinters : Array LeanOption := #[
   ⟨`linter.longLine, true⟩,
   ⟨`linter.oldObtain, true,⟩,
   ⟨`linter.refine, true⟩,
-  ⟨`linter.setOption, true⟩
+  ⟨`linter.style.setOption, true⟩
 ]
 
 /-- These options are passed as `leanOptions` to building mathlib, as well as the

test/Explode.lean

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

test/LibrarySearch/basic.lean

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

test/LintStyle.lean

@@ -6,11 +6,11 @@ import Mathlib.Tactic.Common
 /-! Tests for the `setOption` linter -/
 section setOption
 
--- The warning generated by `linter.setOption` is not suppressed by `#guard_msgs`,
+-- The warning generated by `linter.style.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.
-set_option linter.setOption false
+set_option linter.style.setOption false
 
 -- All types of options are supported: boolean, numeric and string-valued.
 -- On the top level, i.e. as commands.
@@ -19,60 +19,60 @@ set_option linter.setOption false
 warning: Setting options starting with 'debug', 'pp', 'profiler', 'trace' is only intended
 for development and not for final code. If you intend to submit this contribution to the
 Mathlib project, please remove 'set_option pp.all'.
-note: this linter can be disabled with `set_option linter.setOption false`
+note: this linter can be disabled with `set_option linter.style.setOption false`
 -/
 #guard_msgs in
-set_option linter.setOption true in
+set_option linter.style.setOption true in
 set_option pp.all true
 
 /--
 warning: Setting options starting with 'debug', 'pp', 'profiler', 'trace' is only intended
 for development and not for final code. If you intend to submit this contribution to the
 Mathlib project, please remove 'set_option profiler'.
-note: this linter can be disabled with `set_option linter.setOption false`
+note: this linter can be disabled with `set_option linter.style.setOption false`
 -/
 #guard_msgs in
-set_option linter.setOption true in
+set_option linter.style.setOption true in
 set_option profiler false
 
 /--
 warning: Setting options starting with 'debug', 'pp', 'profiler', 'trace' is only intended
 for development and not for final code. If you intend to submit this contribution to the
 Mathlib project, please remove 'set_option pp.all'.
-note: this linter can be disabled with `set_option linter.setOption false`
+note: this linter can be disabled with `set_option linter.style.setOption false`
 -/
 #guard_msgs in
-set_option linter.setOption true in
+set_option linter.style.setOption true in
 set_option pp.all false
 
 /--
 warning: Setting options starting with 'debug', 'pp', 'profiler', 'trace' is only intended
 for development and not for final code. If you intend to submit this contribution to the
 Mathlib project, please remove 'set_option profiler.threshold'.
-note: this linter can be disabled with `set_option linter.setOption false`
+note: this linter can be disabled with `set_option linter.style.setOption false`
 -/
 #guard_msgs in
-set_option linter.setOption true in
+set_option linter.style.setOption true in
 set_option profiler.threshold 50
 
 /--
 warning: Setting options starting with 'debug', 'pp', 'profiler', 'trace' is only intended
 for development and not for final code. If you intend to submit this contribution to the
 Mathlib project, please remove 'set_option trace.profiler.output'.
-note: this linter can be disabled with `set_option linter.setOption false`
+note: this linter can be disabled with `set_option linter.style.setOption false`
 -/
 #guard_msgs in
-set_option linter.setOption true in
+set_option linter.style.setOption true in
 set_option trace.profiler.output "foo"
 
 /--
 warning: Setting options starting with 'debug', 'pp', 'profiler', 'trace' is only intended
 for development and not for final code. If you intend to submit this contribution to the
 Mathlib project, please remove 'set_option debug.moduleNameAtTimeout'.
-note: this linter can be disabled with `set_option linter.setOption false`
+note: this linter can be disabled with `set_option linter.style.setOption false`
 -/
 #guard_msgs in
-set_option linter.setOption true in
+set_option linter.style.setOption true in
 set_option debug.moduleNameAtTimeout false
 
 -- The lint does not fire on arbitrary options.
@@ -84,10 +84,10 @@ set_option autoImplicit false
 warning: Setting options starting with 'debug', 'pp', 'profiler', 'trace' is only intended
 for development and not for final code. If you intend to submit this contribution to the
 Mathlib project, please remove 'set_option pp.all'.
-note: this linter can be disabled with `set_option linter.setOption false`
+note: this linter can be disabled with `set_option linter.style.setOption false`
 -/
 #guard_msgs in
-set_option linter.setOption true in
+set_option linter.style.setOption true in
 lemma tactic : True := by
   set_option pp.all true in
   trivial
@@ -96,10 +96,10 @@ lemma tactic : True := by
 warning: Setting options starting with 'debug', 'pp', 'profiler', 'trace' is only intended
 for development and not for final code. If you intend to submit this contribution to the
 Mathlib project, please remove 'set_option pp.raw.maxDepth'.
-note: this linter can be disabled with `set_option linter.setOption false`
+note: this linter can be disabled with `set_option linter.style.setOption false`
 -/
 #guard_msgs in
-set_option linter.setOption true in
+set_option linter.style.setOption true in
 lemma tactic2 : True := by
   set_option pp.raw.maxDepth 32 in
   trivial
@@ -108,10 +108,10 @@ lemma tactic2 : True := by
 warning: Setting options starting with 'debug', 'pp', 'profiler', 'trace' is only intended
 for development and not for final code. If you intend to submit this contribution to the
 Mathlib project, please remove 'set_option pp.all'.
-note: this linter can be disabled with `set_option linter.setOption false`
+note: this linter can be disabled with `set_option linter.style.setOption false`
 -/
 #guard_msgs in
-set_option linter.setOption true in
+set_option linter.style.setOption true in
 lemma tactic3 : True := by
   set_option pp.all false in
   trivial
@@ -120,10 +120,10 @@ lemma tactic3 : True := by
 warning: Setting options starting with 'debug', 'pp', 'profiler', 'trace' is only intended
 for development and not for final code. If you intend to submit this contribution to the
 Mathlib project, please remove 'set_option trace.profiler.output'.
-note: this linter can be disabled with `set_option linter.setOption false`
+note: this linter can be disabled with `set_option linter.style.setOption false`
 -/
 #guard_msgs in
-set_option linter.setOption true in
+set_option linter.style.setOption true in
 lemma tactic4 : True := by
   set_option trace.profiler.output "foo" in
   trivial

test/Recall.lean

@@ -3,7 +3,7 @@ import Mathlib.Analysis.Calculus.Deriv.Basic
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
 import Mathlib.Data.Complex.Exponential
 
-set_option linter.setOption false
+set_option linter.style.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,6 +1,6 @@
 import Mathlib.LinearAlgebra.LinearIndependent
 
-set_option linter.setOption false
+set_option linter.style.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/vec_notation.lean

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