Further fixup and enable guard messages in the test.

Mathlib.lean

@@ -3841,7 +3841,6 @@ import Mathlib.Tactic.Simps.NotationClass
 import Mathlib.Tactic.SlimCheck
 import Mathlib.Tactic.SplitIfs
 import Mathlib.Tactic.Spread
-import Mathlib.Tactic.StyleLinters
 import Mathlib.Tactic.Substs
 import Mathlib.Tactic.SuccessIfFailWithMsg
 import Mathlib.Tactic.SudoSetOption

Mathlib/Tactic.lean

@@ -187,7 +187,6 @@ import Mathlib.Tactic.Simps.NotationClass
 import Mathlib.Tactic.SlimCheck
 import Mathlib.Tactic.SplitIfs
 import Mathlib.Tactic.Spread
-import Mathlib.Tactic.StyleLinters
 import Mathlib.Tactic.Substs
 import Mathlib.Tactic.SuccessIfFailWithMsg
 import Mathlib.Tactic.SudoSetOption

Mathlib/Tactic/Linter.lean

@@ -1,7 +1,8 @@
 /-
 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.
 -/

test/lint_style.lean

@@ -1,56 +1,105 @@
-import Mathlib.Tactic.StyleLinters
+import Mathlib.Tactic.Linter.Style
 import Mathlib.Tactic.Common
 
 /-! Tests for all the style linters. -/
 
 /-! Tests for the `setOption` linter -/
 section setOption
 
-set_option linter.setOption false -- TODO: enable, once the guard message bug is fixed
+-- 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.
 
--- TODO: why does this guard_msg fail? how to suppress the output?
--- /--
--- 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 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"
 
--- This does not lint on arbitrary options.
+-- The lint does not fire on arbitrary options.
 set_option autoImplicit false
 
 -- We also cover set_option tactics.
 
--- -- TODO: why does this not work?
--- set_option linter.setOption false in
--- /--
--- 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 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