feat: add [deprecated] attribute

RELEASES.md

@@ -1,6 +1,19 @@
 Unreleased
 ---------
 
+* Add attribute `[deprecated]` for marking deprecated declarations. Examples:
+  ```lean
+  def g (x : Nat) := x + 1
+
+  -- Whenever `f` is used, a warning message is generated suggestiong to use `g` instead.
+  @[deprecated g]
+  def f (x : Nat) := x + 1
+
+  -- Whenever `h` is used, a warning message is generated.
+  @[deprecated]
+  def h (x : Nat) := x + 1
+  ```
+
 * Add type `LevelMVarId` (and abbreviation `LMVarId`) for universe level metavariable ids.
   Motivation: prevent meta-programmers from mixing up universe and expression metavariable ids.
 

src/Lean.lean

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

src/Lean/Deprecated.lean

@@ -0,0 +1,38 @@
+/-
+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.Attributes
+
+namespace Lean
+
+builtin_initialize deprecatedAttr : ParametricAttribute (Option Name) ←
+  registerParametricAttribute {
+    name := `deprecated
+    descr := "mark declaration as deprecated",
+    getParam := fun _ stx => do
+     match stx with
+     | `(attr| deprecated $[$id?]?) =>
+       let some id := id? | return none
+       let declNameNew ← resolveGlobalConstNoOverload id
+       return some declNameNew
+     | _  => throwError "invalid `[deprecated]` attribute"
+  }
+
+def isDeprecated (env : Environment) (declName : Name) : Bool :=
+  Option.isSome <| deprecatedAttr.getParam? env declName
+
+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 m!"`{declName}` has been deprecated"
+  | some (some newName) => logWarning m!"`{declName}` has been deprecated, use `{newName}` instead"
+
+end Lean

src/Lean/Elab/Term.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 import Lean.ResolveName
 import Lean.Log
+import Lean.Deprecated
 import Lean.Util.Sorry
 import Lean.Util.ReplaceExpr
 import Lean.Structure
@@ -1670,9 +1671,10 @@ def mkConst (constName : Name) (explicitLevels : List Level := []) : TermElabM E
     return Lean.mkConst constName (explicitLevels ++ us)
 
 private def mkConsts (candidates : List (Name × List String)) (explicitLevels : List Level) : TermElabM (List (Expr × List String)) := do
-  candidates.foldlM (init := []) fun result (constName, projs) => do
-    -- TODO: better suppor for `mkConst` failure. We may want to cache the failures, and report them if all candidates fail.
-   let const ← mkConst constName explicitLevels
+  candidates.foldlM (init := []) fun result (declName, projs) => do
+   -- TODO: better suppor 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
+   let const ← mkConst declName explicitLevels
    return (const, projs) :: result
 
 def resolveName (stx : Syntax) (n : Name) (preresolved : List (Name × List String)) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (List (Expr × List String)) := do
@@ -1689,15 +1691,16 @@ def resolveName (stx : Syntax) (n : Name) (preresolved : List (Name × List Stri
     process (← resolveGlobalName n)
   else
     process preresolved
-where process (candidates : List (Name × List String)) : TermElabM (List (Expr × List String)) := do
-  if candidates.isEmpty then
-    if (← read).autoBoundImplicit &&
-         !(← read).autoBoundImplicitForbidden n &&
-         isValidAutoBoundImplicitName n (relaxedAutoImplicit.get (← getOptions)) then
-      throwAutoBoundImplicitLocal n
-    else
-      throwError "unknown identifier '{Lean.mkConst n}'"
-  mkConsts candidates explicitLevels
+where
+  process (candidates : List (Name × List String)) : TermElabM (List (Expr × List String)) := do
+    if candidates.isEmpty then
+      if (← read).autoBoundImplicit &&
+           !(← read).autoBoundImplicitForbidden n &&
+           isValidAutoBoundImplicitName n (relaxedAutoImplicit.get (← getOptions)) then
+        throwAutoBoundImplicitLocal n
+      else
+        throwError "unknown identifier '{Lean.mkConst n}'"
+    mkConsts candidates explicitLevels
 
 /--
   Similar to `resolveName`, but creates identifiers for the main part and each projection with position information derived from `ident`.
@@ -1705,7 +1708,7 @@ where process (candidates : List (Name × List String)) : TermElabM (List (Expr
   `(v.head, id, [f₁, f₂])` where `id` is an identifier for `v.head`, and `f₁` and `f₂` are identifiers for fields `"bla"` and `"boo"`. -/
 def resolveName' (ident : Syntax) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (List (Expr × Syntax × List Syntax)) := do
   match ident with
-  | Syntax.ident _    _      n preresolved =>
+  | .ident _ _ n preresolved =>
     let r ← resolveName ident n preresolved explicitLevels expectedType?
     r.mapM fun (c, fields) => do
       let ids := ident.identComponents (nFields? := fields.length)
@@ -1714,7 +1717,7 @@ def resolveName' (ident : Syntax) (explicitLevels : List Level) (expectedType? :
 
 def resolveId? (stx : Syntax) (kind := "term") (withInfo := false) : TermElabM (Option Expr) :=
   match stx with
-  | Syntax.ident _ _ val preresolved => do
+  | .ident _ _ val preresolved => do
     let rs ← try resolveName stx val preresolved [] catch _ => pure []
     let rs := rs.filter fun ⟨_, projs⟩ => projs.isEmpty
     let fs := rs.map fun (f, _) => f

tests/lean/deprecated.lean

@@ -0,0 +1,29 @@
+def g (x : Nat) := x + 1
+
+@[deprecated g]
+def f (x : Nat) := x + 1
+
+@[deprecated]
+def h (x : Nat) := x + 1
+
+#eval f 0 + 1
+
+#eval h 0
+
+@[deprecated g1]
+def f1 (x : Nat) := x + 1
+
+def Foo.g1 := 10
+
+@[deprecated Foo.g1]
+def f2 (x : Nat) := x + 1
+
+@[deprecated g1]
+def f3 (x : Nat) := x + 1
+
+open Foo
+@[deprecated g1]
+def f4 (x : Nat) := x + 1
+
+#eval f2 0 + 1
+#eval f4 0 + 1

tests/lean/deprecated.lean.expected.out

@@ -0,0 +1,10 @@
+deprecated.lean:9:6-9:7: warning: `f` has been deprecated, use `g` instead
+2
+deprecated.lean:11:6-11: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
+2
+deprecated.lean:29:6-29:8: warning: `f4` has been deprecated, use `Foo.g1` instead
+2