use (and modify!) logLintIf

leanprover · Oct 8, 2024 · 89ba3be · 89ba3be
1 parent 9a030d9
commit 89ba3be
Show file tree

Hide file tree

Showing 4 changed files with 18 additions and 16 deletions.
diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
@@ -169,10 +169,8 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : Comm
   let classes ← liftCoreM <| getOptDerivingClasses decl[6]
   if decl[3][0].isToken ":=" then
     -- https://github.com/leanprover/lean4/issues/5236
-    if Linter.getLinterValue Linter.linter.deprecated (← getOptions) then
-      withRef decl[0] <| withRef decl[3] <| logWarning <| .tagged ``Linter.deprecatedAttr "\
-        'inductive ... :=' has been deprecated in favor of 'inductive ... where'.\n\
-        You can disable this warning with 'set_option linter.deprecated false'."
+    withRef decl[0] <| Linter.logLintIf Linter.linter.deprecated decl[3]
+      "'inductive ... :=' has been deprecated in favor of 'inductive ... where'."
   return {
     ref             := decl
     shortDeclName   := name

diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
@@ -140,11 +140,9 @@ def structFields         := leading_parser many (structExplicitBinder <|> struct
 private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (structDeclName : Name) : TermElabM (Array StructFieldView) := do
   if structStx[5][0].isToken ":=" then
     -- https://github.com/leanprover/lean4/issues/5236
-    if Linter.getLinterValue Linter.linter.deprecated (← getOptions) then
-      let cmd := if structStx[0].getKind == ``Parser.Command.classTk then "class" else "structure"
-      withRef structStx[0] <| withRef structStx[5][0] <| logWarning <| .tagged ``Linter.deprecatedAttr s!"\
-        '{cmd} ... :=' has been deprecated in favor of '{cmd} ... where'.\n\
-        You can disable this warning with 'set_option linter.deprecated false'."
+    let cmd := if structStx[0].getKind == ``Parser.Command.classTk then "class" else "structure"
+    withRef structStx[0] <| Linter.logLintIf Linter.linter.deprecated structStx[5][0]
+      s!"{cmd} ... :=' has been deprecated in favor of '{cmd} ... where'."
   let fieldBinders := if structStx[5].isNone then #[] else structStx[5][2][0].getArgs
   fieldBinders.foldlM (init := #[]) fun (views : Array StructFieldView) fieldBinder => withRef fieldBinder do
     let mut fieldBinder := fieldBinder

diff --git a/src/Lean/Linter/Basic.lean b/src/Lean/Linter/Basic.lean
@@ -23,8 +23,14 @@ def logLint [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m]
   let disable := m!"note: this linter can be disabled with `set_option {linterOption.name} false`"
   logWarningAt stx (.tagged linterOption.name m!"{msg}\n{disable}")
 
-/-- If `linterOption` is true, print a linter warning message at the position determined by `stx`.
+/--
+If `linterOption` is enabled, print a linter warning message at the position determined by `stx`.
+
+Whether a linter option is enabled or not is determined by the following sequence:
+1. If it is set, then the value determines whether or not it is enabled.
+2. Otherwise, if `linter.all` is set, then its value determines whether or not the option is enabled.
+3. Otherwise, the default value determines whether or not it is enabled.
 -/
 def logLintIf [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m]
     (linterOption : Lean.Option Bool) (stx : Syntax) (msg : MessageData) : m Unit := do
-  if linterOption.get (← getOptions) then logLint linterOption stx msg
+  if getLinterValue linterOption (← getOptions) then logLint linterOption stx msg
diff --git a/tests/lean/run/5236.lean b/tests/lean/run/5236.lean
@@ -6,24 +6,24 @@ set_option linter.deprecated true
 
 /--
 warning: 'inductive ... :=' has been deprecated in favor of 'inductive ... where'.
-You can disable this warning with 'set_option linter.deprecated false'.
+note: this linter can be disabled with `set_option linter.deprecated false`
 -/
 #guard_msgs in
 inductive DogSound' :=
   | woof
   | grr
 
 /--
-warning: 'structure ... :=' has been deprecated in favor of 'structure ... where'.
-You can disable this warning with 'set_option linter.deprecated false'.
+warning: structure ... :=' has been deprecated in favor of 'structure ... where'.
+note: this linter can be disabled with `set_option linter.deprecated false`
 -/
 #guard_msgs in
 structure S :=
   (n : Nat)
 
 /--
-warning: 'class ... :=' has been deprecated in favor of 'class ... where'.
-You can disable this warning with 'set_option linter.deprecated false'.
+warning: class ... :=' has been deprecated in favor of 'class ... where'.
+note: this linter can be disabled with `set_option linter.deprecated false`
 -/
 #guard_msgs in
 class C :=