From c4cbefce11241bfdf193b0be60598dfafe402fc7 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Fri, 21 Oct 2022 23:44:17 -0400 Subject: [PATCH] feat: add `linter.deprecated` option to silence deprecation warnings --- src/Lean.lean | 1 - src/Lean/Elab/Term.lean | 5 ++-- src/Lean/Linter.lean | 1 + src/Lean/Linter/Basic.lean | 12 +++++++++ src/Lean/Linter/Builtin.lean | 1 + src/Lean/{ => Linter}/Deprecated.lean | 26 ++++++++++--------- src/Lean/Linter/MissingDocs.lean | 1 + src/Lean/Linter/UnusedVariables.lean | 2 ++ src/Lean/Linter/Util.lean | 28 ++++++--------------- tests/lean/deprecated.lean | 4 +++ tests/lean/deprecated.lean.expected.out | 13 +++++----- tests/lean/warningAsError.lean | 2 ++ tests/lean/warningAsError.lean.expected.out | 6 ++--- 13 files changed, 57 insertions(+), 45 deletions(-) create mode 100644 src/Lean/Linter/Basic.lean rename src/Lean/{ => Linter}/Deprecated.lean (61%) diff --git a/src/Lean.lean b/src/Lean.lean index 05d39440c85a..74de8f0ba2fc 100644 --- a/src/Lean.lean +++ b/src/Lean.lean @@ -35,4 +35,3 @@ import Lean.Widget import Lean.Log import Lean.Linter import Lean.SubExpr -import Lean.Deprecated diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index ccad3e2455c9..21a3da14ecdd 100644 --- a/src/Lean/Elab/Term.lean +++ b/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 diff --git a/src/Lean/Linter.lean b/src/Lean/Linter.lean index 1bd94951cb40..7939686c32b6 100644 --- a/src/Lean/Linter.lean +++ b/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 diff --git a/src/Lean/Linter/Basic.lean b/src/Lean/Linter/Basic.lean new file mode 100644 index 000000000000..8e532008d820 --- /dev/null +++ b/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) diff --git a/src/Lean/Linter/Builtin.lean b/src/Lean/Linter/Builtin.lean index eb9d469ba07a..cb5a4b7bc0f2 100644 --- a/src/Lean/Linter/Builtin.lean +++ b/src/Lean/Linter/Builtin.lean @@ -1,4 +1,5 @@ import Lean.Linter.Util +import Lean.Elab.Command namespace Lean.Linter diff --git a/src/Lean/Deprecated.lean b/src/Lean/Linter/Deprecated.lean similarity index 61% rename from src/Lean/Deprecated.lean rename to src/Lean/Linter/Deprecated.lean index 9a52fe2a23fc..b154439b7656 100644 --- a/src/Lean/Deprecated.lean +++ b/src/Lean/Linter/Deprecated.lean @@ -3,11 +3,16 @@ 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 + +register_builtin_option linter.deprecated : Bool := { + defValue := true + descr := "if true, generate deprecation warnings" +} builtin_initialize deprecatedAttr : ParametricAttribute (Option Name) ← registerParametricAttribute { @@ -25,18 +30,15 @@ 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 + (deprecatedAttr.getParam? env declName).getD 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" - -end Lean + 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" diff --git a/src/Lean/Linter/MissingDocs.lean b/src/Lean/Linter/MissingDocs.lean index 7c3f5f697723..3d8200fc4748 100644 --- a/src/Lean/Linter/MissingDocs.lean +++ b/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 diff --git a/src/Lean/Linter/UnusedVariables.lean b/src/Lean/Linter/UnusedVariables.lean index 9ee71bed4bc2..6d81671e3fbf 100644 --- a/src/Lean/Linter/UnusedVariables.lean +++ b/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 #[] diff --git a/src/Lean/Linter/Util.lean b/src/Lean/Linter/Util.lean index 0bf9bd054abb..5d5fa8870122 100644 --- a/src/Lean/Linter/Util.lean +++ b/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 diff --git a/tests/lean/deprecated.lean b/tests/lean/deprecated.lean index 97faa83124a6..ba76e764d0c3 100644 --- a/tests/lean/deprecated.lean +++ b/tests/lean/deprecated.lean @@ -1,3 +1,5 @@ +set_option linter.deprecated true + def g (x : Nat) := x + 1 @[deprecated g] @@ -25,5 +27,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 diff --git a/tests/lean/deprecated.lean.expected.out b/tests/lean/deprecated.lean.expected.out index 65fa33d42615..40a428f3d456 100644 --- a/tests/lean/deprecated.lean.expected.out +++ b/tests/lean/deprecated.lean.expected.out @@ -1,10 +1,11 @@ -deprecated.lean:9:6-9:7: warning: `f` has been deprecated, use `g` instead +deprecated.lean:11:6-11:7: warning: `f` has been deprecated, use `g` instead 2 -deprecated.lean:11:6-11:7: warning: `h` has been deprecated +deprecated.lean:13:6-13:7: warning: `h` has been deprecated 1 -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 +deprecated.lean:15:13-15:15: error: unknown constant 'g1' +deprecated.lean:23:13-23:15: error: unknown constant 'g1' +deprecated.lean:30:6-30: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 +2 +deprecated.lean:33:6-33:8: warning: `f4` has been deprecated, use `Foo.g1` instead 2 diff --git a/tests/lean/warningAsError.lean b/tests/lean/warningAsError.lean index cd35d1f68806..7768da79d245 100644 --- a/tests/lean/warningAsError.lean +++ b/tests/lean/warningAsError.lean @@ -1,3 +1,5 @@ +set_option linter.deprecated true + def f (x : Nat) := x + 1 @[deprecated f] diff --git a/tests/lean/warningAsError.lean.expected.out b/tests/lean/warningAsError.lean.expected.out index aba481ace96c..648ec65610fd 100644 --- a/tests/lean/warningAsError.lean.expected.out +++ b/tests/lean/warningAsError.lean.expected.out @@ -1,5 +1,5 @@ -warningAsError.lean:6:6-6:7: warning: `g` has been deprecated, use `f` instead +warningAsError.lean:8:6-8:7: warning: `g` has been deprecated, use `f` instead 1 -warningAsError.lean:10:6-10:7: error: `g` has been deprecated, use `f` instead +warningAsError.lean:12:6-12:7: error: `g` has been deprecated, use `f` instead 1 -warningAsError.lean:13:7-13:13: error: unused variable `unused` [linter.unusedVariables] +warningAsError.lean:15:7-15:13: error: unused variable `unused` [linter.unusedVariables]