feat: add linter.deprecated option to silence deprecation warnings

src/Lean.lean

@@ -35,4 +35,3 @@ import Lean.Widget
 import Lean.Log
 import Lean.Linter
 import Lean.SubExpr
-import Lean.Deprecated

src/Lean/Elab/Term.lean

@@ -3,11 +3,10 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
-import Lean.Deprecated
 import Lean.Meta.AppBuilder
 import Lean.Meta.CollectMVars
 import Lean.Meta.Coe
-
+import Lean.Linter.Deprecated
 import Lean.Elab.Config
 import Lean.Elab.Level
 import Lean.Elab.DeclModifiers
@@ -1527,7 +1526,7 @@ def mkConst (constName : Name) (explicitLevels : List Level := []) : TermElabM E
 private def mkConsts (candidates : List (Name × List String)) (explicitLevels : List Level) : TermElabM (List (Expr × List String)) := do
   candidates.foldlM (init := []) fun result (declName, projs) => do
     -- TODO: better support for `mkConst` failure. We may want to cache the failures, and report them if all candidates fail.
-    checkDeprecated declName -- TODO: check is occurring too early if there are multiple alternatives. Fix if it is not ok in practice
+    Linter.checkDeprecated declName -- TODO: check is occurring too early if there are multiple alternatives. Fix if it is not ok in practice
     let const ← mkConst declName explicitLevels
     return (const, projs) :: result
 

src/Lean/Linter.lean

@@ -1,4 +1,5 @@
 import Lean.Linter.Util
 import Lean.Linter.Builtin
+import Lean.Linter.Deprecated
 import Lean.Linter.UnusedVariables
 import Lean.Linter.MissingDocs

src/Lean/Linter/Basic.lean

@@ -0,0 +1,12 @@
+import Lean.Data.Options
+
+namespace Lean.Linter
+
+register_builtin_option linter.all : Bool := {
+  defValue := false
+  descr := "enable all linters"
+}
+
+def getLinterAll (o : Options) (defValue := linter.all.defValue) : Bool := o.get linter.all.name defValue
+
+def getLinterValue (opt : Lean.Option Bool) (o : Options) : Bool := o.get opt.name (getLinterAll o opt.defValue)

src/Lean/Linter/Builtin.lean

@@ -1,4 +1,5 @@
 import Lean.Linter.Util
+import Lean.Elab.Command
 
 namespace Lean.Linter
 

src/Lean/Deprecated.lean → src/Lean/Linter/Deprecated.lean

@@ -3,11 +3,11 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import Lean.Log
+import Lean.Linter.Basic
 import Lean.Attributes
 import Lean.Elab.InfoTree.Main
 
-namespace Lean
+namespace Lean.Linter
 
 builtin_initialize deprecatedAttr : ParametricAttribute (Option Name) ←
   registerParametricAttribute {
@@ -25,18 +25,22 @@ builtin_initialize deprecatedAttr : ParametricAttribute (Option Name) ←
 def isDeprecated (env : Environment) (declName : Name) : Bool :=
   Option.isSome <| deprecatedAttr.getParam? env declName
 
-def MessageData.isDeprecationWarning (msg : MessageData) : Bool :=
+def _root_.Lean.MessageData.isDeprecationWarning (msg : MessageData) : Bool :=
   msg.hasTag (· == ``deprecatedAttr)
 
 def getDeprecatedNewName (env : Environment) (declName : Name) : Option Name :=
   match deprecatedAttr.getParam? env declName with
   | some newName? => newName?
   | none => none
 
-def checkDeprecated [Monad m] [MonadEnv m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (declName : Name) : m Unit := do
-  match deprecatedAttr.getParam? (← getEnv) declName with
-  | none => pure ()
-  | some none => logWarning <| .tagged ``deprecatedAttr m!"`{declName}` has been deprecated"
-  | some (some newName) => logWarning <| .tagged ``deprecatedAttr m!"`{declName}` has been deprecated, use `{newName}` instead"
+register_builtin_option linter.deprecated : Bool := {
+  defValue := true
+  descr := "if true, do not generate deprecation warnings"
+}
 
-end Lean
+def checkDeprecated [Monad m] [MonadEnv m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (declName : Name) : m Unit := do
+  if getLinterValue linter.deprecated (← getOptions) then
+    match deprecatedAttr.getParam? (← getEnv) declName with
+    | none => pure ()
+    | some none => logWarning <| .tagged ``deprecatedAttr m!"`{declName}` has been deprecated"
+    | some (some newName) => logWarning <| .tagged ``deprecatedAttr m!"`{declName}` has been deprecated, use `{newName}` instead"

src/Lean/Linter/MissingDocs.lean

@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Lean.Meta.Tactic.Simp.SimpTheorems
+import Lean.Elab.Command
 import Lean.Elab.SetOption
 import Lean.Linter.Util
 

src/Lean/Linter/UnusedVariables.lean

@@ -1,3 +1,4 @@
+import Lean.Elab.Command
 import Lean.Linter.Util
 import Lean.Server.References
 
@@ -21,6 +22,7 @@ def getLinterUnusedVariables (o : Options) : Bool := getLinterValue linter.unuse
 def getLinterUnusedVariablesFunArgs (o : Options) : Bool := o.get linter.unusedVariables.funArgs.name (getLinterUnusedVariables o)
 def getLinterUnusedVariablesPatternVars (o : Options) : Bool := o.get linter.unusedVariables.patternVars.name (getLinterUnusedVariables o)
 
+abbrev IgnoreFunction := Syntax → Syntax.Stack → Options → Bool
 
 builtin_initialize builtinUnusedVariablesIgnoreFnsRef : IO.Ref <| Array IgnoreFunction ← IO.mkRef #[]
 

src/Lean/Linter/Util.lean

@@ -1,21 +1,13 @@
 import Lean.Data.Options
-import Lean.Elab.Command
 import Lean.Server.InfoUtils
+import Lean.Linter.Basic
 
 namespace Lean.Linter
 
-register_builtin_option linter.all : Bool := {
-  defValue := false
-  descr := "enable all linters"
-}
+open Lean.Elab
 
-def getLinterAll (o : Options) (defValue := linter.all.defValue) : Bool := o.get linter.all.name defValue
-
-def getLinterValue (opt : Lean.Option Bool) (o : Options) : Bool := o.get opt.name (getLinterAll o opt.defValue)
-
-open Lean.Elab Lean.Elab.Command
-
-def logLint (linterOption : Lean.Option Bool) (stx : Syntax) (msg : MessageData) : CommandElabM Unit :=
+def logLint [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m]
+    (linterOption : Lean.Option Bool) (stx : Syntax) (msg : MessageData) : m Unit :=
   logWarningAt stx (.tagged linterOption.name m!"{msg} [{linterOption.name}]")
 
 /-- Go upwards through the given `tree` starting from the smallest node that
@@ -26,10 +18,10 @@ The result is `some []` if no `MacroExpansionInfo` was found on the way and
 Return the result reversed, s.t. the macro expansion that would be applied to
 the original syntax first is the first element of the returned list. -/
 def collectMacroExpansions? {m} [Monad m] (range : String.Range) (tree : Elab.InfoTree) : m <| Option <| List Elab.MacroExpansionInfo := do
-    if let .some <| .some result ← go then
-      return some result.reverse
-    else
-      return none
+  if let .some <| .some result ← go then
+    return some result.reverse
+  else
+    return none
 where
   go : m <| Option <| Option <| List Elab.MacroExpansionInfo := tree.visitM (postNode := fun _ i _ results => do
     let results := results |>.filterMap id |>.filterMap id
@@ -47,7 +39,3 @@ where
         return some []
     else
       return none)
-
-abbrev IgnoreFunction := Syntax → Syntax.Stack → Options → Bool
-
-end Lean.Linter

tests/lean/deprecated.lean

@@ -25,5 +25,7 @@ open Foo
 @[deprecated g1]
 def f4 (x : Nat) := x + 1
 
+#eval f2 0 + 1
+set_option linter.deprecated false in
 #eval f2 0 + 1
 #eval f4 0 + 1

tests/lean/deprecated.lean.expected.out

@@ -6,5 +6,5 @@ deprecated.lean:13:13-13:15: error: unknown constant 'g1'
 deprecated.lean:21:13-21:15: error: unknown constant 'g1'
 deprecated.lean:28:6-28:8: warning: `f2` has been deprecated, use `Foo.g1` instead
 2
-deprecated.lean:29:6-29:8: warning: `f4` has been deprecated, use `Foo.g1` instead
+deprecated.lean:31:6-31:8: warning: `f4` has been deprecated, use `Foo.g1` instead
 2