From fe3ba4dc4c5b794578df3ea66d399e0203ba73fe Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Mon, 9 Mar 2026 12:58:02 +0100 Subject: [PATCH] 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 | 2 +- src/Lean/Linter/Omit.lean | 2 +- src/Lean/Meta/Tactic/Simp/LoopProtection.lean | 2 +- tests/elab/12563.lean | 195 ++++++++++++++++++ tests/elab/calc.lean.out.expected | 50 ----- tests/elab/grind_11545.lean.out.expected | 6 - tests/elab/variable.lean | 2 + 7 files changed, 200 insertions(+), 59 deletions(-) create mode 100644 tests/elab/12563.lean diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index a61040ac94..685534cb48 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/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 || diff --git a/src/Lean/Linter/Omit.lean b/src/Lean/Linter/Omit.lean index 089bfc4891..5d0db9725c 100644 --- a/src/Lean/Linter/Omit.lean +++ b/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 \ diff --git a/src/Lean/Meta/Tactic/Simp/LoopProtection.lean b/src/Lean/Meta/Tactic/Simp/LoopProtection.lean index aad1fa503e..500afcf56d 100644 --- a/src/Lean/Meta/Tactic/Simp/LoopProtection.lean +++ b/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 diff --git a/tests/elab/12563.lean b/tests/elab/12563.lean new file mode 100644 index 0000000000..bb693ddfd1 --- /dev/null +++ b/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 diff --git a/tests/elab/calc.lean.out.expected b/tests/elab/calc.lean.out.expected index 9d441d0ecf..396df0925a 100644 --- a/tests/elab/calc.lean.out.expected +++ b/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` diff --git a/tests/elab/grind_11545.lean.out.expected b/tests/elab/grind_11545.lean.out.expected index b7c9aabaa5..526a11acea 100644 --- a/tests/elab/grind_11545.lean.out.expected +++ b/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` diff --git a/tests/elab/variable.lean b/tests/elab/variable.lean index 61ba914043..edc8b57199 100644 --- a/tests/elab/variable.lean +++ b/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