fix: make the omit, unusedSectionVars and loopingSimpArgs linter respect linter.all (#12563)

This PR makes the `omit`, `unusedSectionVars` and `loopingSimpArgs`
linters respect the `linter.all` option:
when `linter.all` is set to false (and the respective linter option is
unset), the linter should not report errors.

Similarly to #12559, these linters should honour the linter.all flag
being set to false. These are all remaining occurrences of this pattern.

This fixes an issue analogous to #12559.
This PR and #12560 fix all occurrences of this pattern. (The only
question is around `RCases.linter.unusedRCasesPattern`: should this also
respect this? I have left this alone for now.)

Co-authored-by: fiforeach <249703130+fiforeach@users.noreply.github.com>

src/Lean/Elab/MutualDef.lean

@@ -561,7 +561,7 @@ private def elabFunValues (headers : Array DefViewElabHeader) (vars : Array Expr
           withExporting do
             let type ← instantiateMVars type
             Meta.check type
-        if linter.unusedSectionVars.get (← getOptions) && !header.type.hasSorry && !val.hasSorry then
+        if Linter.getLinterValue linter.unusedSectionVars (← Linter.getLinterOptions) && !header.type.hasSorry && !val.hasSorry then
           let unusedVars ← vars.filterMapM fun var => do
             let varDecl ← var.fvarId!.getDecl
             return if sc.includedVars.contains varDecl.userName ||

src/Lean/Linter/Omit.lean

@@ -21,7 +21,7 @@ register_builtin_option linter.omit : Bool := {
 
 def «omit» : Linter where
   run stx := do
-    unless linter.omit.get (← getOptions) do
+    unless getLinterValue linter.omit (← getLinterOptions) do
       return
     if let some stx := stx.find? (·.isOfKind ``Lean.Parser.Command.«omit») then
       logLint linter.omit stx m!"`omit` should be avoided in favor of restructuring your \

src/Lean/Meta/Tactic/Simp/LoopProtection.lean

@@ -54,7 +54,7 @@ def mkLoopWarningMsg (thm : SimpTheorem) : SimpM MessageData := do
 def shouldCheckLoops (force : Bool) (ctxt : Simp.Context) : CoreM Bool := do
   if ctxt.config.singlePass then return false
   if force then return true
-  return linter.loopingSimpArgs.get (← getOptions)
+  return Linter.getLinterValue linter.loopingSimpArgs (← Linter.getLinterOptions)
 
 /--
 Main entry point to the loop protection mechanism: Checks if the given theorem is looping in the

tests/elab/12563.lean

@@ -0,0 +1,195 @@
+/-!
+# Make the `unusedSectionVars`, `omit` and `loopingSimpArgs` linters honour the `linter.all` option
+
+When e.g. `linter.unusedSectionVars` is not set explicitly, but the `linter.all` option is set,
+the linter should behave accordingly; similarly for `linter.omit` and `linter.loopingSimpArgs`.
+-/
+
+/-! ## `linter.unusedSectionVars` -/
+
+namespace UnusedSectionVars
+
+section
+
+set_option linter.unusedSectionVars true
+
+variable {α : Type} [ToString α]
+
+/--
+warning: automatically included section variable(s) unused in theorem `UnusedSectionVars.myTheorem1`:
+  [ToString α]
+consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
+  omit [ToString α] in theorem ...
+
+Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
+-/
+#guard_msgs in
+theorem myTheorem1 (a : α) : a = a := rfl
+
+end
+
+section
+
+set_option linter.all true
+
+variable {α : Type} [ToString α]
+
+/--
+warning: automatically included section variable(s) unused in theorem `UnusedSectionVars.myTheorem2`:
+  [ToString α]
+consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
+  omit [ToString α] in theorem ...
+
+Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
+-/
+#guard_msgs in
+theorem myTheorem2 (a : α) : a = a := rfl
+
+end
+
+section
+
+set_option linter.unusedSectionVars false
+
+variable {α : Type} [ToString α]
+
+theorem myTheorem3 (a : α) : a = a := rfl
+
+end
+
+section
+
+set_option linter.all false
+
+variable {α : Type} [ToString α]
+
+theorem myTheorem4 (a : α) : a = a := rfl
+
+end
+
+end UnusedSectionVars
+
+/-! ## `linter.omit` -/
+
+namespace Omit
+
+section
+
+set_option linter.omit true
+
+variable (α : Type)
+
+/--
+warning: `omit` should be avoided in favor of restructuring your `variable` declarations
+
+Note: This linter can be disabled with `set_option linter.omit false`
+-/
+#guard_msgs in
+omit α
+
+end
+
+section
+
+set_option linter.all true
+
+variable (α : Type)
+
+/--
+warning: `omit` should be avoided in favor of restructuring your `variable` declarations
+
+Note: This linter can be disabled with `set_option linter.omit false`
+-/
+#guard_msgs in
+omit α
+
+end
+
+section
+
+set_option linter.omit false
+
+variable (α : Type)
+
+omit α
+
+end
+
+section
+
+set_option linter.all false
+
+variable (α : Type)
+
+omit α
+
+end
+
+end Omit
+
+/-! ## `linter.loopingSimpArgs` -/
+
+namespace LoopingSimpArgs
+
+set_option linter.unusedSimpArgs false -- can be removed after merging #12560
+
+axiom testSorry : α
+
+opaque a : Nat
+
+theorem aa : a = id a := testSorry
+
+section
+
+set_option linter.loopingSimpArgs true
+
+/--
+warning: Possibly looping simp theorem: `aa`
+
+Note: Possibly caused by: `id`
+
+Hint: You can disable a simp theorem from the default simp set by passing `- theoremName` to `simp`.
+
+Note: This linter can be disabled with `set_option linter.loopingSimpArgs false`
+-/
+#guard_msgs in
+example : True := by simp -failIfUnchanged only [aa, id]
+
+end
+
+section
+
+set_option linter.all true
+
+/--
+warning: Possibly looping simp theorem: `aa`
+
+Note: Possibly caused by: `id`
+
+Hint: You can disable a simp theorem from the default simp set by passing `- theoremName` to `simp`.
+
+Note: This linter can be disabled with `set_option linter.loopingSimpArgs false`
+-/
+#guard_msgs in
+example : True := by simp -failIfUnchanged only [aa, id]
+
+end
+section
+
+set_option linter.loopingSimpArgs false
+
+#guard_msgs in
+example : True := by simp -failIfUnchanged only [aa, id]
+
+end
+
+section
+
+set_option linter.all false
+
+#guard_msgs in
+example : True := by simp -failIfUnchanged only [aa, id]
+
+end
+
+end LoopingSimpArgs

tests/elab/calc.lean.out.expected

@@ -1,51 +1 @@
 calc.lean:15:0-15:8: warning: declaration uses `sorry`
-calc.lean:18:0-25:3: warning: automatically included section variable(s) unused in theorem `foo₁`:
-  pf23
-consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
-  omit pf23 in theorem ...
-
-Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
-calc.lean:28:0-32:20: warning: automatically included section variable(s) unused in theorem `foo₂`:
-  pf23
-consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
-  omit pf23 in theorem ...
-
-Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
-calc.lean:35:0-40:19: warning: automatically included section variable(s) unused in theorem `foo₃`:
-  pf23
-consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
-  omit pf23 in theorem ...
-
-Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
-calc.lean:43:0-47:23: warning: automatically included section variable(s) unused in theorem `foo₄`:
-  pf23
-consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
-  omit pf23 in theorem ...
-
-Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
-calc.lean:50:0-57:19: warning: automatically included section variable(s) unused in theorem `foo₅`:
-  pf23'
-  pf45'
-consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
-  omit pf23' pf45' in theorem ...
-
-Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
-calc.lean:60:0-65:19: warning: automatically included section variable(s) unused in theorem `foo₆`:
-  pf23'
-  pf45'
-consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
-  omit pf23' pf45' in theorem ...
-
-Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
-calc.lean:68:0-73:19: warning: automatically included section variable(s) unused in theorem `foo₇`:
-  pf23
-consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
-  omit pf23 in theorem ...
-
-Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
-calc.lean:76:0-81:19: warning: automatically included section variable(s) unused in theorem `foo₈`:
-  pf23
-consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
-  omit pf23 in theorem ...
-
-Note: This linter can be disabled with `set_option linter.unusedSectionVars false`

tests/elab/grind_11545.lean.out.expected

@@ -1,11 +1,5 @@
 op_comp: [@Quiver.Hom.op #7 _ #4 #2 (@CategoryStruct.comp _ #6 #4 #3 #2 #1 #0)]
 op_comp: [@CategoryStruct.comp (Opposite #7) _ (@op _ #2) (@op _ #3) (@op _ #4) (@Quiver.Hom.op _ _ #3 #2 #0) (@Quiver.Hom.op _ _ #4 #3 #1)]
-grind_11545.lean:100:0-100:85: warning: automatically included section variable(s) unused in theorem `op_comp`:
-  [Category C]
-consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
-  omit [Category C] in theorem ...
-
-Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
 grind_11545.lean:132:4-132:14: warning: declaration uses `sorry`
 grind_11545.lean:148:4-148:13: warning: declaration uses `sorry`
 grind_11545.lean:148:4-148:13: warning: declaration uses `sorry`

tests/elab/variable.lean

@@ -1,5 +1,7 @@
 /-! # Basic section variable tests -/
 
+set_option linter.unusedSectionVars true
+
 /-! Directly referenced variables should be included. -/
 variable {n : Nat} in
 theorem t1 : n = n := by induction n <;> rfl