turn off linter again

src/Init/Data/Array/Subarray.lean

@@ -15,13 +15,13 @@ structure Subarray (α : Type u)  where
   start_le_stop : start ≤ stop
   stop_le_array_size : stop ≤ array.size
 
-@[deprecated Subarray.array]
+@[deprecated Subarray.array (since := "2024-04-13")]
 abbrev Subarray.as (s : Subarray α) : Array α := s.array
 
-@[deprecated Subarray.start_le_stop]
+@[deprecated Subarray.start_le_stop (since := "2024-04-13")]
 theorem Subarray.h₁ (s : Subarray α) : s.start ≤ s.stop := s.start_le_stop
 
-@[deprecated Subarray.stop_le_array_size]
+@[deprecated Subarray.stop_le_array_size (since := "2024-04-13")]
 theorem Subarray.h₂ (s : Subarray α) : s.stop ≤ s.array.size := s.stop_le_array_size
 
 namespace Subarray

src/Init/Data/BitVec/Basic.lean

@@ -34,7 +34,8 @@ structure BitVec (w : Nat) where
   O(1), because we use `Fin` as the internal representation of a bitvector. -/
   toFin : Fin (2^w)
 
-@[deprecated] protected abbrev Std.BitVec := _root_.BitVec
+@[deprecated (since := "2024-04-12")]
+protected abbrev Std.BitVec := _root_.BitVec
 
 -- We manually derive the `DecidableEq` instances for `BitVec` because
 -- we want to have builtin support for bit-vector literals, and we
@@ -73,7 +74,7 @@ protected def toNat (a : BitVec n) : Nat := a.toFin.val
 /-- Return the bound in terms of toNat. -/
 theorem isLt (x : BitVec w) : x.toNat < 2^w := x.toFin.isLt
 
-@[deprecated isLt]
+@[deprecated isLt (since := "2024-03-12")]
 theorem toNat_lt (x : BitVec n) : x.toNat < 2^n := x.isLt
 
 /-- Theorem for normalizing the bit vector literal representation. -/

src/Init/Data/BitVec/Lemmas.lean

@@ -146,7 +146,8 @@ theorem getLsb_ofNat (n : Nat) (x : Nat) (i : Nat) :
   getLsb (x#n) i = (i < n && x.testBit i) := by
   simp [getLsb, BitVec.ofNat, Fin.val_ofNat']
 
-@[simp, deprecated toNat_ofNat] theorem toNat_zero (n : Nat) : (0#n).toNat = 0 := by trivial
+@[simp, deprecated toNat_ofNat (since := "2024-02-22")]
+theorem toNat_zero (n : Nat) : (0#n).toNat = 0 := by trivial
 
 @[simp] theorem getLsb_zero : (0#w).getLsb i = false := by simp [getLsb]
 

src/Init/Data/Bool.lean

@@ -360,7 +360,8 @@ def toNat (b:Bool) : Nat := cond b 1 0
 theorem toNat_le (c : Bool) : c.toNat ≤ 1 := by
   cases c <;> trivial
 
-@[deprecated toNat_le] abbrev toNat_le_one := toNat_le
+@[deprecated toNat_le (since := "2024-02-23")]
+abbrev toNat_le_one := toNat_le
 
 theorem toNat_lt (b : Bool) : b.toNat < 2 :=
   Nat.lt_succ_of_le (toNat_le _)

src/Init/Data/Fin/Lemmas.lean

@@ -62,7 +62,8 @@ theorem mk_val (i : Fin n) : (⟨i, i.isLt⟩ : Fin n) = i := Fin.eta ..
 @[simp] theorem val_ofNat' (a : Nat) (is_pos : n > 0) :
   (Fin.ofNat' a is_pos).val = a % n := rfl
 
-@[deprecated ofNat'_zero_val] theorem ofNat'_zero_val : (Fin.ofNat' 0 h).val = 0 := Nat.zero_mod _
+@[deprecated ofNat'_zero_val (since := "2024-02-22")]
+theorem ofNat'_zero_val : (Fin.ofNat' 0 h).val = 0 := Nat.zero_mod _
 
 @[simp] theorem mod_val (a b : Fin n) : (a % b).val = a.val % b.val :=
   rfl

src/Init/Data/Nat/Lemmas.lean

@@ -137,14 +137,14 @@ protected theorem sub_le_iff_le_add' {a b c : Nat} : a - b ≤ c ↔ a ≤ b + c
 protected theorem le_sub_iff_add_le {n : Nat} (h : k ≤ m) : n ≤ m - k ↔ n + k ≤ m :=
   ⟨Nat.add_le_of_le_sub h, Nat.le_sub_of_add_le⟩
 
-@[deprecated Nat.le_sub_iff_add_le]
+@[deprecated Nat.le_sub_iff_add_le (since := "2024-02-19")]
 protected theorem add_le_to_le_sub (n : Nat) (h : m ≤ k) : n + m ≤ k ↔ n ≤ k - m :=
   (Nat.le_sub_iff_add_le h).symm
 
 protected theorem add_le_of_le_sub' {n k m : Nat} (h : m ≤ k) : n ≤ k - m → m + n ≤ k :=
   Nat.add_comm .. ▸ Nat.add_le_of_le_sub h
 
-@[deprecated Nat.add_le_of_le_sub']
+@[deprecated Nat.add_le_of_le_sub' (since := "2024-02-19")]
 protected theorem add_le_of_le_sub_left {n k m : Nat} (h : m ≤ k) : n ≤ k - m → m + n ≤ k :=
   Nat.add_le_of_le_sub' h
 
@@ -401,11 +401,11 @@ protected theorem mul_min_mul_left (a b c : Nat) : min (a * b) (a * c) = a * min
 
 /-! ### mul -/
 
-@[deprecated Nat.mul_le_mul_left]
+@[deprecated Nat.mul_le_mul_left (since := "2024-02-19")]
 protected theorem mul_le_mul_of_nonneg_left {a b c : Nat} : a ≤ b → c * a ≤ c * b :=
   Nat.mul_le_mul_left c
 
-@[deprecated Nat.mul_le_mul_right]
+@[deprecated Nat.mul_le_mul_right (since := "2024-02-19")]
 protected theorem mul_le_mul_of_nonneg_right {a b c : Nat} : a ≤ b → a * c ≤ b * c :=
   Nat.mul_le_mul_right c
 

src/Init/Data/Option/Basic.lean

@@ -18,8 +18,8 @@ def getM [Alternative m] : Option α → m α
   | none     => failure
   | some a   => pure a
 
-@[deprecated getM] def toMonad [Monad m] [Alternative m] : Option α → m α :=
-  getM
+@[deprecated getM (since := "2024-04-17")]
+def toMonad [Monad m] [Alternative m] : Option α → m α := getM
 
 /-- Returns `true` on `some x` and `false` on `none`. -/
 @[inline] def isSome : Option α → Bool

src/Lean/Meta/Basic.lean

@@ -629,7 +629,7 @@ Return `none` if `mvarId` has no declaration in the current metavariable context
 def _root_.Lean.MVarId.findDecl? (mvarId : MVarId) : MetaM (Option MetavarDecl) :=
   return (← getMCtx).findDecl? mvarId
 
-@[deprecated MVarId.findDecl?]
+@[deprecated MVarId.findDecl? (since := "2022-07-15")]
 def findMVarDecl? (mvarId : MVarId) : MetaM (Option MetavarDecl) :=
   mvarId.findDecl?
 
@@ -642,7 +642,7 @@ def _root_.Lean.MVarId.getDecl (mvarId : MVarId) : MetaM MetavarDecl := do
   | some d => pure d
   | none   => throwError "unknown metavariable '?{mvarId.name}'"
 
-@[deprecated MVarId.getDecl]
+@[deprecated MVarId.getDecl (since := "2022-07-15")]
 def getMVarDecl (mvarId : MVarId) : MetaM MetavarDecl := do
   mvarId.getDecl
 
@@ -652,7 +652,7 @@ Return `mvarId` kind. Throw an exception if `mvarId` is not declared in the curr
 def _root_.Lean.MVarId.getKind (mvarId : MVarId) : MetaM MetavarKind :=
   return (← mvarId.getDecl).kind
 
-@[deprecated MVarId.getKind]
+@[deprecated MVarId.getKind (since := "2022-07-15")]
 def getMVarDeclKind (mvarId : MVarId) : MetaM MetavarKind :=
   mvarId.getKind
 
@@ -669,7 +669,7 @@ Set `mvarId` kind in the current metavariable context.
 def _root_.Lean.MVarId.setKind (mvarId : MVarId) (kind : MetavarKind) : MetaM Unit :=
   modifyMCtx fun mctx => mctx.setMVarKind mvarId kind
 
-@[deprecated MVarId.setKind]
+@[deprecated MVarId.setKind (since := "2022-07-15")]
 def setMVarKind (mvarId : MVarId) (kind : MetavarKind) : MetaM Unit :=
   mvarId.setKind kind
 
@@ -678,7 +678,7 @@ def setMVarKind (mvarId : MVarId) (kind : MetavarKind) : MetaM Unit :=
 def _root_.Lean.MVarId.setType (mvarId : MVarId) (type : Expr) : MetaM Unit := do
   modifyMCtx fun mctx => mctx.setMVarType mvarId type
 
-@[deprecated MVarId.setType]
+@[deprecated MVarId.setType (since := "2022-07-15")]
 def setMVarType (mvarId : MVarId) (type : Expr) : MetaM Unit := do
   mvarId.setType type
 
@@ -689,7 +689,7 @@ That is, its `depth` is different from the current metavariable context depth.
 def _root_.Lean.MVarId.isReadOnly (mvarId : MVarId) : MetaM Bool := do
   return (← mvarId.getDecl).depth != (← getMCtx).depth
 
-@[deprecated MVarId.isReadOnly]
+@[deprecated MVarId.isReadOnly (since := "2022-07-15")]
 def isReadOnlyExprMVar (mvarId : MVarId) : MetaM Bool := do
   mvarId.isReadOnly
 
@@ -704,7 +704,7 @@ def _root_.Lean.MVarId.isReadOnlyOrSyntheticOpaque (mvarId : MVarId) : MetaM Boo
   | MetavarKind.syntheticOpaque => return !(← getConfig).assignSyntheticOpaque
   | _ => return mvarDecl.depth != (← getMCtx).depth
 
-@[deprecated MVarId.isReadOnlyOrSyntheticOpaque]
+@[deprecated MVarId.isReadOnlyOrSyntheticOpaque (since := "2022-07-15")]
 def isReadOnlyOrSyntheticOpaqueExprMVar (mvarId : MVarId) : MetaM Bool := do
   mvarId.isReadOnlyOrSyntheticOpaque
 
@@ -716,7 +716,7 @@ def _root_.Lean.LMVarId.getLevel (mvarId : LMVarId) : MetaM Nat := do
   | some depth => return depth
   | _          => throwError "unknown universe metavariable '?{mvarId.name}'"
 
-@[deprecated LMVarId.getLevel]
+@[deprecated LMVarId.getLevel (since := "2022-07-15")]
 def getLevelMVarDepth (mvarId : LMVarId) : MetaM Nat :=
   mvarId.getLevel
 
@@ -727,7 +727,7 @@ That is, its `depth` is different from the current metavariable context depth.
 def _root_.Lean.LMVarId.isReadOnly (mvarId : LMVarId) : MetaM Bool :=
   return (← mvarId.getLevel) < (← getMCtx).levelAssignDepth
 
-@[deprecated LMVarId.isReadOnly]
+@[deprecated LMVarId.isReadOnly (since := "2022-07-15")]
 def isReadOnlyLevelMVar (mvarId : LMVarId) : MetaM Bool := do
   mvarId.isReadOnly
 
@@ -737,7 +737,7 @@ Set the user-facing name for the given metavariable.
 def _root_.Lean.MVarId.setUserName (mvarId : MVarId) (newUserName : Name) : MetaM Unit :=
   modifyMCtx fun mctx => mctx.setMVarUserName mvarId newUserName
 
-@[deprecated MVarId.setUserName]
+@[deprecated MVarId.setUserName (since := "2022-07-15")]
 def setMVarUserName (mvarId : MVarId) (userNameNew : Name) : MetaM Unit :=
   mvarId.setUserName userNameNew
 
@@ -747,7 +747,7 @@ Throw an exception saying `fvarId` is not declared in the current local context.
 def _root_.Lean.FVarId.throwUnknown (fvarId : FVarId) : CoreM α :=
   throwError "unknown free variable '{mkFVar fvarId}'"
 
-@[deprecated FVarId.throwUnknown]
+@[deprecated FVarId.throwUnknown (since := "2022-07-15")]
 def throwUnknownFVar (fvarId : FVarId) : MetaM α :=
   fvarId.throwUnknown
 
@@ -757,7 +757,7 @@ Return `some decl` if `fvarId` is declared in the current local context.
 def _root_.Lean.FVarId.findDecl? (fvarId : FVarId) : MetaM (Option LocalDecl) :=
   return (← getLCtx).find? fvarId
 
-@[deprecated FVarId.findDecl?]
+@[deprecated FVarId.findDecl? (since := "2022-07-15")]
 def findLocalDecl? (fvarId : FVarId) : MetaM (Option LocalDecl) :=
   fvarId.findDecl?
 
@@ -770,7 +770,7 @@ def _root_.Lean.FVarId.getDecl (fvarId : FVarId) : MetaM LocalDecl := do
   | some d => return d
   | none   => fvarId.throwUnknown
 
-@[deprecated FVarId.getDecl]
+@[deprecated FVarId.getDecl (since := "2022-07-15")]
 def getLocalDecl (fvarId : FVarId) : MetaM LocalDecl := do
   fvarId.getDecl
 
@@ -837,7 +837,7 @@ contain a metavariable `?m` s.t. local context of `?m` contains a free variable
 def _root_.Lean.Expr.abstractRangeM (e : Expr) (n : Nat) (xs : Array Expr) : MetaM Expr :=
   liftMkBindingM <| MetavarContext.abstractRange e n xs
 
-@[deprecated Expr.abstractRangeM]
+@[deprecated Expr.abstractRangeM (since := "2022-07-15")]
 def abstractRange (e : Expr) (n : Nat) (xs : Array Expr) : MetaM Expr :=
   e.abstractRangeM n xs
 
@@ -848,7 +848,7 @@ Similar to `Expr.abstract`, but handles metavariables correctly.
 def _root_.Lean.Expr.abstractM (e : Expr) (xs : Array Expr) : MetaM Expr :=
   e.abstractRangeM xs.size xs
 
-@[deprecated Expr.abstractM]
+@[deprecated Expr.abstractM (since := "2022-07-15")]
 def abstract (e : Expr) (xs : Array Expr) : MetaM Expr :=
   e.abstractM xs
 
@@ -1487,7 +1487,7 @@ private def withMVarContextImp (mvarId : MVarId) (x : MetaM α) : MetaM α := do
 def _root_.Lean.MVarId.withContext (mvarId : MVarId) : n α → n α :=
   mapMetaM <| withMVarContextImp mvarId
 
-@[deprecated MVarId.withContext]
+@[deprecated MVarId.withContext (since := "2022-07-15")]
 def withMVarContext (mvarId : MVarId) : n α → n α :=
   mvarId.withContext
 

src/Lean/Meta/Tactic/Apply.lean

@@ -185,7 +185,7 @@ def _root_.Lean.MVarId.apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig :=
     result.forM (·.headBetaType)
     return result
 
-@[deprecated MVarId.apply]
+@[deprecated MVarId.apply (since := "2022-07-15")]
 def apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig := {}) : MetaM (List MVarId) :=
   mvarId.apply e cfg
 
@@ -227,7 +227,7 @@ Apply `And.intro` as much as possible to goal `mvarId`.
 abbrev splitAnd (mvarId : MVarId) : MetaM (List MVarId) :=
   splitAndCore mvarId
 
-@[deprecated splitAnd]
+@[deprecated splitAnd] -- 2024-03-17
 def _root_.Lean.Meta.splitAnd (mvarId : MVarId) : MetaM (List MVarId) :=
   mvarId.splitAnd
 

src/Lean/Meta/Tactic/Assert.lean

@@ -24,7 +24,7 @@ def _root_.Lean.MVarId.assert (mvarId : MVarId) (name : Name) (type : Expr) (val
     mvarId.assign (mkApp newMVar val)
     return newMVar.mvarId!
 
-@[deprecated MVarId.assert]
+@[deprecated MVarId.assert (since := "2022-07-15")]
 def assert (mvarId : MVarId) (name : Name) (type : Expr) (val : Expr) : MetaM MVarId :=
   mvarId.assert name type val
 
@@ -46,7 +46,7 @@ def _root_.Lean.MVarId.define (mvarId : MVarId) (name : Name) (type : Expr) (val
     mvarId.assign newMVar
     return newMVar.mvarId!
 
-@[deprecated MVarId.define]
+@[deprecated MVarId.define (since := "2022-07-15")]
 def define (mvarId : MVarId) (name : Name) (type : Expr) (val : Expr) : MetaM MVarId := do
   mvarId.define name type val
 
@@ -66,7 +66,7 @@ def _root_.Lean.MVarId.assertExt (mvarId : MVarId) (name : Name) (type : Expr) (
     mvarId.assign (mkApp2 newMVar val rflPrf)
     return newMVar.mvarId!
 
-@[deprecated MVarId.assertExt]
+@[deprecated MVarId.assertExt (since := "2022-07-15")]
 def assertExt (mvarId : MVarId) (name : Name) (type : Expr) (val : Expr) (hName : Name := `h) : MetaM MVarId := do
   mvarId.assertExt name type val hName
 
@@ -90,7 +90,7 @@ def _root_.Lean.MVarId.assertAfter (mvarId : MVarId) (fvarId : FVarId) (userName
     subst := subst.insert f (mkFVar fNew)
   return { fvarId := fvarIdNew, mvarId, subst }
 
-@[deprecated MVarId.assertAfter]
+@[deprecated MVarId.assertAfter (since := "2022-07-15")]
 def assertAfter (mvarId : MVarId) (fvarId : FVarId) (userName : Name) (type : Expr) (val : Expr) : MetaM AssertAfterResult := do
   mvarId.assertAfter fvarId userName type val
 
@@ -116,7 +116,7 @@ def _root_.Lean.MVarId.assertHypotheses (mvarId : MVarId) (hs : Array Hypothesis
     mvarId.assign val
     mvarNew.mvarId!.introNP hs.size
 
-@[deprecated MVarId.assertHypotheses]
+@[deprecated MVarId.assertHypotheses (since := "2022-07-15")]
 def assertHypotheses (mvarId : MVarId) (hs : Array Hypothesis) : MetaM (Array FVarId × MVarId) := do
   mvarId.assertHypotheses hs
 

src/Lean/Meta/Tactic/Assumption.lean

@@ -26,7 +26,7 @@ def _root_.Lean.MVarId.assumptionCore (mvarId : MVarId) : MetaM Bool :=
     | none => return false
     | some fvarId => mvarId.assign (mkFVar fvarId); return true
 
-@[deprecated MVarId.assumptionCore]
+@[deprecated MVarId.assumptionCore (since := "2022-07-15")]
 def assumptionCore (mvarId : MVarId) : MetaM Bool :=
   mvarId.assumptionCore
 
@@ -35,7 +35,7 @@ def _root_.Lean.MVarId.assumption (mvarId : MVarId) : MetaM Unit :=
   unless (← mvarId.assumptionCore) do
     throwTacticEx `assumption mvarId
 
-@[deprecated MVarId.assumption]
+@[deprecated MVarId.assumption (since := "2022-07-15")]
 def assumption (mvarId : MVarId) : MetaM Unit :=
   mvarId.assumption
 

src/Lean/Meta/Tactic/Cases.lean

@@ -269,7 +269,7 @@ Apply `casesOn` using the free variable `majorFVarId` as the major premise (aka
 def _root_.Lean.MVarId.cases (mvarId : MVarId) (majorFVarId : FVarId) (givenNames : Array AltVarNames := #[]) (useNatCasesAuxOn : Bool := false) : MetaM (Array CasesSubgoal) :=
   Cases.cases mvarId majorFVarId givenNames (useNatCasesAuxOn := useNatCasesAuxOn)
 
-@[deprecated MVarId.cases]
+@[deprecated MVarId.cases (since := "2022-07-15")]
 def cases (mvarId : MVarId) (majorFVarId : FVarId) (givenNames : Array AltVarNames := #[]) : MetaM (Array CasesSubgoal) :=
   Cases.cases mvarId majorFVarId givenNames
 

src/Lean/Meta/Tactic/Cleanup.lean

@@ -72,7 +72,7 @@ where
 abbrev _root_.Lean.MVarId.cleanup (mvarId : MVarId) (toPreserve : Array FVarId := #[]) (indirectProps : Bool := true) : MetaM MVarId := do
   cleanupCore mvarId toPreserve indirectProps
 
-@[deprecated MVarId.cleanup]
+@[deprecated MVarId.cleanup (since := "2022-07-15")]
 abbrev cleanup (mvarId : MVarId) : MetaM MVarId := do
   mvarId.cleanup
 

src/Lean/Meta/Tactic/Clear.lean

@@ -35,7 +35,7 @@ def _root_.Lean.MVarId.clear (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId
     pure newMVar.mvarId!
 
 
-@[deprecated MVarId.clear]
+@[deprecated MVarId.clear (since := "2022-07-15")]
 def clear (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId :=
   mvarId.clear fvarId
 
@@ -46,7 +46,7 @@ cannot be erased due to forward dependencies.
 def _root_.Lean.MVarId.tryClear (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId :=
   mvarId.clear fvarId <|> pure mvarId
 
-@[deprecated MVarId.tryClear]
+@[deprecated MVarId.tryClear (since := "2022-07-15")]
 def tryClear (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId :=
   mvarId.tryClear fvarId
 
@@ -56,7 +56,7 @@ Try to erase the given free variables from the goal `mvarId`.
 def _root_.Lean.MVarId.tryClearMany (mvarId : MVarId) (fvarIds : Array FVarId) : MetaM MVarId := do
   fvarIds.foldrM (init := mvarId) fun fvarId mvarId => mvarId.tryClear fvarId
 
-@[deprecated MVarId.tryClearMany]
+@[deprecated MVarId.tryClearMany (since := "2022-07-15")]
 def tryClearMany (mvarId : MVarId) (fvarIds : Array FVarId) : MetaM MVarId := do
   mvarId.tryClearMany fvarIds
 

src/Lean/Meta/Tactic/Constructor.lean

@@ -28,7 +28,7 @@ def _root_.Lean.MVarId.constructor (mvarId : MVarId) (cfg : ApplyConfig := {}) :
             pure ()
         throwTacticEx `constructor mvarId "no applicable constructor found"
 
-@[deprecated MVarId.constructor]
+@[deprecated MVarId.constructor (since := "2022-07-15")]
 def constructor (mvarId : MVarId) (cfg : ApplyConfig := {}) : MetaM (List MVarId) := do
   mvarId.constructor cfg
 
@@ -50,7 +50,7 @@ def _root_.Lean.MVarId.existsIntro (mvarId : MVarId) (w : Expr) : MetaM MVarId :
           | throwTacticEx `exists mvarId "unexpected number of subgoals"
         pure mvarId
 
-@[deprecated MVarId.existsIntro]
+@[deprecated MVarId.existsIntro (since := "2022-07-15")]
 def existsIntro (mvarId : MVarId) (w : Expr) : MetaM MVarId := do
   mvarId.existsIntro w
 

src/Lean/Meta/Tactic/Contradiction.lean

@@ -226,7 +226,7 @@ def _root_.Lean.MVarId.contradiction (mvarId : MVarId) (config : Contradiction.C
   unless (← mvarId.contradictionCore config) do
     throwTacticEx `contradiction mvarId
 
-@[deprecated MVarId.contradiction]
+@[deprecated MVarId.contradiction (since := "2022-07-15")]
 def contradiction (mvarId : MVarId) (config : Contradiction.Config := {}) : MetaM Unit :=
   mvarId.contradiction config
 

src/Lean/Meta/Tactic/Delta.lean

@@ -32,7 +32,7 @@ def _root_.Lean.MVarId.deltaTarget (mvarId : MVarId) (p : Name → Bool) : MetaM
     mvarId.checkNotAssigned `delta
     mvarId.change (← deltaExpand (← mvarId.getType) p) (checkDefEq := false)
 
-@[deprecated MVarId.deltaTarget]
+@[deprecated MVarId.deltaTarget (since := "2022-07-15")]
 def deltaTarget (mvarId : MVarId) (p : Name → Bool) : MetaM MVarId :=
   mvarId.deltaTarget p
 
@@ -44,7 +44,7 @@ def _root_.Lean.MVarId.deltaLocalDecl (mvarId : MVarId) (fvarId : FVarId) (p : N
     mvarId.checkNotAssigned `delta
     mvarId.changeLocalDecl fvarId (← deltaExpand (← mvarId.getType) p) (checkDefEq := false)
 
-@[deprecated MVarId.deltaLocalDecl]
+@[deprecated MVarId.deltaLocalDecl (since := "2022-07-15")]
 def deltaLocalDecl (mvarId : MVarId) (fvarId : FVarId) (p : Name → Bool) : MetaM MVarId :=
   mvarId.deltaLocalDecl fvarId p
 

src/Lean/Meta/Tactic/Generalize.lean

@@ -125,7 +125,7 @@ def _root_.Lean.MVarId.generalize (mvarId : MVarId) (args : Array GeneralizeArg)
     (transparency := TransparencyMode.instances) : MetaM (Array FVarId × MVarId) :=
   generalizeCore mvarId args transparency
 
-@[inherit_doc generalizeCore, deprecated MVarId.generalize]
+@[inherit_doc generalizeCore, deprecated MVarId.generalize (since := "2022-07-15")]
 def generalize (mvarId : MVarId) (args : Array GeneralizeArg)
     (transparency := TransparencyMode.instances) : MetaM (Array FVarId × MVarId) :=
   generalizeCore mvarId args transparency

src/Lean/Meta/Tactic/Induction.lean

@@ -207,7 +207,7 @@ def _root_.Lean.MVarId.induction (mvarId : MVarId) (majorFVarId : FVarId) (recur
           | _ =>
            throwTacticEx `induction mvarId "major premise is not of the form (C ...)"
 
-@[deprecated MVarId.induction]
+@[deprecated MVarId.induction (since := "2022-07-15")]
 def induction (mvarId : MVarId) (majorFVarId : FVarId) (recursorName : Name) (givenNames : Array AltVarNames := #[]) : MetaM (Array InductionSubgoal) :=
   mvarId.induction majorFVarId recursorName givenNames
 

src/Lean/Meta/Tactic/Intro.lean

@@ -132,7 +132,7 @@ Introduce `n` binders in the goal `mvarId`.
 abbrev _root_.Lean.MVarId.introN (mvarId : MVarId) (n : Nat) (givenNames : List Name := []) (useNamesForExplicitOnly := false) : MetaM (Array FVarId × MVarId) :=
   introNCore mvarId n givenNames (useNamesForExplicitOnly := useNamesForExplicitOnly) (preserveBinderNames := false)
 
-@[deprecated MVarId.introN]
+@[deprecated MVarId.introN (since := "2022-07-15")]
 abbrev introN (mvarId : MVarId) (n : Nat) (givenNames : List Name := []) (useNamesForExplicitOnly := false) : MetaM (Array FVarId × MVarId) :=
   mvarId.introN n givenNames useNamesForExplicitOnly
 
@@ -143,7 +143,7 @@ The suffix `P` stands for "preserving`.
 abbrev _root_.Lean.MVarId.introNP (mvarId : MVarId) (n : Nat) : MetaM (Array FVarId × MVarId) :=
   introNCore mvarId n [] (useNamesForExplicitOnly := false) (preserveBinderNames := true)
 
-@[deprecated MVarId.introNP]
+@[deprecated MVarId.introNP (since := "2022-07-15")]
 abbrev introNP (mvarId : MVarId) (n : Nat) : MetaM (Array FVarId × MVarId) :=
   mvarId.introNP n
 
@@ -154,7 +154,7 @@ def _root_.Lean.MVarId.intro (mvarId : MVarId) (name : Name) : MetaM (FVarId ×
   let (fvarIds, mvarId) ← mvarId.introN 1 [name]
   return (fvarIds[0]!, mvarId)
 
-@[deprecated MVarId.intro]
+@[deprecated MVarId.intro (since := "2022-07-15")]
 def intro (mvarId : MVarId) (name : Name) : MetaM (FVarId × MVarId) := do
   mvarId.intro name
 
@@ -169,7 +169,7 @@ does not start with a forall, lambda or let. -/
 abbrev _root_.Lean.MVarId.intro1 (mvarId : MVarId) : MetaM (FVarId × MVarId) :=
   intro1Core mvarId false
 
-@[deprecated MVarId.intro1]
+@[deprecated MVarId.intro1 (since := "2022-07-15")]
 abbrev intro1 (mvarId : MVarId) : MetaM (FVarId × MVarId) :=
   mvarId.intro1
 
@@ -180,7 +180,7 @@ does not start with a forall, lambda or let. -/
 abbrev _root_.Lean.MVarId.intro1P (mvarId : MVarId) : MetaM (FVarId × MVarId) :=
   intro1Core mvarId true
 
-@[deprecated MVarId.intro1P]
+@[deprecated MVarId.intro1P (since := "2022-07-15")]
 abbrev intro1P (mvarId : MVarId) : MetaM (FVarId × MVarId) :=
   mvarId.intro1P
 
@@ -206,7 +206,7 @@ def _root_.Lean.MVarId.intros (mvarId : MVarId) : MetaM (Array FVarId × MVarId)
   else
     mvarId.introN n
 
-@[deprecated MVarId.intros]
+@[deprecated MVarId.intros (since := "2022-07-15")]
 def intros (mvarId : MVarId) : MetaM (Array FVarId × MVarId) := do
   mvarId.intros
 

src/Lean/Meta/Tactic/Refl.lean

@@ -37,11 +37,11 @@ def _root_.Lean.MVarId.refl (mvarId : MVarId) : MetaM Unit := do
     let α := targetType.appFn!.appFn!.appArg!
     mvarId.assign (mkApp2 (mkConst ``Eq.refl  us) α lhs)
 
-@[deprecated MVarId.refl]
+@[deprecated MVarId.refl (since := "2022-07-15")]
 def refl (mvarId : MVarId) : MetaM Unit := do
   mvarId.refl
 
-@[deprecated MVarId.refl]
+@[deprecated MVarId.refl (since := "2022-07-15")]
 def _root_.Lean.MVarId.applyRefl (mvarId : MVarId) (msg : MessageData := "refl failed") : MetaM Unit :=
   try mvarId.refl catch _ => throwError msg
 

src/Lean/Meta/Tactic/Rename.lean

@@ -18,7 +18,7 @@ def _root_.Lean.MVarId.rename (mvarId : MVarId) (fvarId : FVarId) (userNameNew :
   mvarId.assign mvarNew
   return mvarNew.mvarId!
 
-@[deprecated MVarId.rename]
+@[deprecated MVarId.rename (since := "2022-07-15")]
 def rename (mvarId : MVarId) (fvarId : FVarId) (newUserName : Name) : MetaM MVarId :=
   mvarId.rename fvarId newUserName
 

src/Lean/Meta/Tactic/Replace.lean

@@ -32,7 +32,7 @@ def _root_.Lean.MVarId.replaceTargetEq (mvarId : MVarId) (targetNew : Expr) (eqP
     mvarId.assign val
     return mvarNew.mvarId!
 
-@[deprecated MVarId.replaceTargetEq]
+@[deprecated MVarId.replaceTargetEq (since := "2022-07-15")]
 def replaceTargetEq (mvarId : MVarId) (targetNew : Expr) (eqProof : Expr) : MetaM MVarId :=
   mvarId.replaceTargetEq targetNew eqProof
 
@@ -56,7 +56,7 @@ def _root_.Lean.MVarId.replaceTargetDefEq (mvarId : MVarId) (targetNew : Expr) :
       mvarId.assign newVal
       return mvarNew.mvarId!
 
-@[deprecated MVarId.replaceTargetDefEq]
+@[deprecated MVarId.replaceTargetDefEq (since := "2022-07-15")]
 def replaceTargetDefEq (mvarId : MVarId) (targetNew : Expr) : MetaM MVarId :=
   mvarId.replaceTargetDefEq targetNew
 
@@ -102,7 +102,7 @@ where
 abbrev _root_.Lean.MVarId.replaceLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) (eqProof : Expr) : MetaM AssertAfterResult :=
   replaceLocalDeclCore mvarId fvarId typeNew eqProof
 
-@[deprecated MVarId.replaceLocalDecl]
+@[deprecated MVarId.replaceLocalDecl (since := "2022-07-15")]
 abbrev replaceLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) (eqProof : Expr) : MetaM AssertAfterResult :=
   mvarId.replaceLocalDecl fvarId typeNew eqProof
 
@@ -121,7 +121,7 @@ def _root_.Lean.MVarId.replaceLocalDeclDefEq (mvarId : MVarId) (fvarId : FVarId)
       mvarId.assign mvarNew
       return mvarNew.mvarId!
 
-@[deprecated MVarId.replaceLocalDeclDefEq]
+@[deprecated MVarId.replaceLocalDeclDefEq (since := "2022-07-15")]
 def replaceLocalDeclDefEq (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) : MetaM MVarId := do
   mvarId.replaceLocalDeclDefEq fvarId typeNew
 
@@ -137,7 +137,7 @@ def _root_.Lean.MVarId.change (mvarId : MVarId) (targetNew : Expr) (checkDefEq :
       throwTacticEx `change mvarId m!"given type{indentExpr targetNew}\nis not definitionally equal to{indentExpr target}"
   mvarId.replaceTargetDefEq targetNew
 
-@[deprecated MVarId.change]
+@[deprecated MVarId.change (since := "2022-07-15")]
 def change (mvarId : MVarId) (targetNew : Expr) (checkDefEq := true) : MetaM MVarId := mvarId.withContext do
   mvarId.change targetNew checkDefEq
 
@@ -222,7 +222,7 @@ def _root_.Lean.MVarId.modifyTarget (mvarId : MVarId) (f : Expr → MetaM Expr)
     mvarId.checkNotAssigned `modifyTarget
     mvarId.change (← f (← mvarId.getType)) (checkDefEq := false)
 
-@[deprecated modifyTarget]
+@[deprecated modifyTarget (since := "2022-07-15")]
 def modifyTarget (mvarId : MVarId) (f : Expr → MetaM Expr) : MetaM MVarId := do
   mvarId.modifyTarget f
 
@@ -237,7 +237,7 @@ def _root_.Lean.MVarId.modifyTargetEqLHS (mvarId : MVarId) (f : Expr → MetaM E
      else
        throwTacticEx `modifyTargetEqLHS mvarId m!"equality expected{indentExpr target}"
 
-@[deprecated MVarId.modifyTargetEqLHS]
+@[deprecated MVarId.modifyTargetEqLHS (since := "2022-07-15")]
 def modifyTargetEqLHS (mvarId : MVarId) (f : Expr → MetaM Expr) : MetaM MVarId := do
   mvarId.modifyTargetEqLHS f
 

src/Lean/Meta/Tactic/Revert.lean

@@ -53,7 +53,7 @@ def _root_.Lean.MVarId.revertAfter (mvarId : MVarId) (fvarId : FVarId) : MetaM (
     let fvarIds := (← getLCtx).foldl (init := #[]) (start := localDecl.index+1) fun fvarIds decl => fvarIds.push decl.fvarId
     mvarId.revert fvarIds (preserveOrder := true) (clearAuxDeclsInsteadOfRevert := true)
 
-@[deprecated MVarId.revert]
+@[deprecated MVarId.revert (since := "2022-07-15")]
 def revert (mvarId : MVarId) (fvarIds : Array FVarId) (preserveOrder : Bool := false) : MetaM (Array FVarId × MVarId) := do
   mvarId.revert fvarIds preserveOrder
 

src/Lean/Meta/Tactic/Rewrite.lean

@@ -74,7 +74,7 @@ def _root_.Lean.MVarId.rewrite (mvarId : MVarId) (e : Expr) (heq : Expr)
     | none =>
       cont heq heqType
 
-@[deprecated MVarId.rewrite]
+@[deprecated MVarId.rewrite (since := "2022-07-15")]
 def rewrite (mvarId : MVarId) (e : Expr) (heq : Expr)
     (symm : Bool := false) (config := { : Rewrite.Config }) : MetaM RewriteResult :=
   mvarId.rewrite e heq symm config

src/Lean/Meta/Tactic/Util.lean

@@ -15,14 +15,14 @@ namespace Lean.Meta
 def _root_.Lean.MVarId.getTag (mvarId : MVarId) : MetaM Name :=
   return (← mvarId.getDecl).userName
 
-@[deprecated MVarId.getTag]
+@[deprecated MVarId.getTag (since := "2022-07-15")]
 def getMVarTag (mvarId : MVarId) : MetaM Name :=
   mvarId.getTag
 
 def _root_.Lean.MVarId.setTag (mvarId : MVarId) (tag : Name) : MetaM Unit := do
   modify fun s => { s with mctx := s.mctx.setMVarUserName mvarId tag }
 
-@[deprecated MVarId.setTag]
+@[deprecated MVarId.setTag (since := "2022-07-15")]
 def setMVarTag (mvarId : MVarId) (tag : Name) : MetaM Unit := do
   mvarId.setTag tag
 
@@ -49,7 +49,7 @@ def _root_.Lean.MVarId.checkNotAssigned (mvarId : MVarId) (tacticName : Name) :
   if (← mvarId.isAssigned) then
     throwTacticEx tacticName mvarId "metavariable has already been assigned"
 
-@[deprecated MVarId.checkNotAssigned]
+@[deprecated MVarId.checkNotAssigned (since := "2022-07-15")]
 def checkNotAssigned (mvarId : MVarId) (tacticName : Name) : MetaM Unit := do
   mvarId.checkNotAssigned tacticName
 
@@ -57,7 +57,7 @@ def checkNotAssigned (mvarId : MVarId) (tacticName : Name) : MetaM Unit := do
 def _root_.Lean.MVarId.getType (mvarId : MVarId) : MetaM Expr :=
   return (← mvarId.getDecl).type
 
-@[deprecated MVarId.getType]
+@[deprecated MVarId.getType (since := "2022-07-15")]
 def getMVarType (mvarId : MVarId) : MetaM Expr :=
   mvarId.getType
 
@@ -69,7 +69,7 @@ weak head normal form. -/
 def _root_.Lean.MVarId.getType' (mvarId : MVarId) : MetaM Expr := do
   instantiateMVars (← whnf (← mvarId.getType))
 
-@[deprecated MVarId.getType']
+@[deprecated MVarId.getType' (since := "2022-07-15")]
 def getMVarType' (mvarId : MVarId) : MetaM Expr := do
   mvarId.getType'
 
@@ -83,7 +83,7 @@ def _root_.Lean.MVarId.admit (mvarId : MVarId) (synthetic := true) : MetaM Unit
     let val ← mkSorry mvarType synthetic
     mvarId.assign val
 
-@[deprecated MVarId.admit]
+@[deprecated MVarId.admit (since := "2022-07-15")]
 def admit (mvarId : MVarId) (synthetic := true) : MetaM Unit :=
   mvarId.admit synthetic
 
@@ -91,7 +91,7 @@ def admit (mvarId : MVarId) (synthetic := true) : MetaM Unit :=
 def _root_.Lean.MVarId.headBetaType (mvarId : MVarId) : MetaM Unit := do
   mvarId.setType (← mvarId.getType).headBeta
 
-@[deprecated MVarId.headBetaType]
+@[deprecated MVarId.headBetaType (since := "2022-07-15")]
 def headBetaMVarType (mvarId : MVarId) : MetaM Unit := do
   mvarId.headBetaType
 
@@ -123,7 +123,7 @@ def _root_.Lean.MVarId.getNondepPropHyps (mvarId : MVarId) : MetaM (Array FVarId
           result := result.push localDecl.fvarId
       return result
 
-@[deprecated MVarId.getNondepPropHyps]
+@[deprecated MVarId.getNondepPropHyps (since := "2022-07-15")]
 def getNondepPropHyps (mvarId : MVarId) : MetaM (Array FVarId) :=
   mvarId.getNondepPropHyps
 

src/Lean/MetavarContext.lean

@@ -383,14 +383,14 @@ def isLevelMVarAssigned [Monad m] [MonadMCtx m] (mvarId : LMVarId) : m Bool :=
 def _root_.Lean.MVarId.isAssigned [Monad m] [MonadMCtx m] (mvarId : MVarId) : m Bool :=
   return (← getMCtx).eAssignment.contains mvarId
 
-@[deprecated MVarId.isAssigned]
+@[deprecated MVarId.isAssigned (since := "2022-07-15")]
 def isExprMVarAssigned [Monad m] [MonadMCtx m] (mvarId : MVarId) : m Bool := do
   mvarId.isAssigned
 
 def _root_.Lean.MVarId.isDelayedAssigned [Monad m] [MonadMCtx m] (mvarId : MVarId) : m Bool :=
   return (← getMCtx).dAssignment.contains mvarId
 
-@[deprecated MVarId.isDelayedAssigned]
+@[deprecated MVarId.isDelayedAssigned (since := "2022-07-15")]
 def isMVarDelayedAssigned [Monad m] [MonadMCtx m] (mvarId : MVarId) : m Bool := do
   mvarId.isDelayedAssigned
 
@@ -422,7 +422,7 @@ def _root_.Lean.MVarId.isAssignable [Monad m] [MonadMCtx m] (mvarId : MVarId) :
   let decl := mctx.getDecl mvarId
   return decl.depth == mctx.depth
 
-@[deprecated MVarId.isAssignable]
+@[deprecated MVarId.isAssignable (since := "2022-07-15")]
 def isExprMVarAssignable [Monad m] [MonadMCtx m] (mvarId : MVarId) : m Bool := do
   mvarId.isAssignable
 
@@ -492,7 +492,7 @@ This is a low-level API, and it is safer to use `isDefEq (mkMVar mvarId) x`.
 def _root_.Lean.MVarId.assign [MonadMCtx m] (mvarId : MVarId) (val : Expr) : m Unit :=
   modifyMCtx fun m => { m with eAssignment := m.eAssignment.insert mvarId val }
 
-@[deprecated MVarId.assign]
+@[deprecated MVarId.assign (since := "2022-07-15")]
 def assignExprMVar [MonadMCtx m] (mvarId : MVarId) (val : Expr) : m Unit :=
   mvarId.assign val
 

src/Lean/Widget/UserWidget.lean

@@ -346,12 +346,13 @@ structure UserWidgetDefinition where
 instance : ToModule UserWidgetDefinition where
   toModule uwd := { uwd with }
 
-private def widgetAttrImpl : AttributeImpl where
+@[deprecated (since := "2023-12-21")] private def widgetAttrImpl : AttributeImpl where
   name := `widget
   descr := "The `@[widget]` attribute has been deprecated, use `@[widget_module]` instead."
   applicationTime := AttributeApplicationTime.afterCompilation
   add := widgetModuleAttrImpl.add
 
+set_option linter.deprecated false in
 builtin_initialize registerBuiltinAttribute widgetAttrImpl
 
 private unsafe def evalUserWidgetDefinitionUnsafe [Monad m] [MonadEnv m] [MonadOptions m] [MonadError m]
@@ -364,7 +365,7 @@ opaque evalUserWidgetDefinition [Monad m] [MonadEnv m] [MonadOptions m] [MonadEr
 
 /-- Save a user-widget instance to the infotree.
     The given `widgetId` should be the declaration name of the widget definition. -/
-@[deprecated savePanelWidgetInfo] def saveWidgetInfo (widgetId : Name) (props : Json)
+@[deprecated savePanelWidgetInfo (since := "2023-12-21")] def saveWidgetInfo (widgetId : Name) (props : Json)
     (stx : Syntax) : CoreM Unit := do
   let uwd ← evalUserWidgetDefinition widgetId
   savePanelWidgetInfo (ToModule.toModule uwd).javascriptHash (pure props) stx
@@ -439,6 +440,6 @@ def getWidgets (pos : Lean.Lsp.Position) : RequestM (RequestTask (GetWidgetsResp
 builtin_initialize
   Server.registerBuiltinRpcProcedure ``getWidgets _ _ getWidgets
 
-attribute [deprecated Module] UserWidgetDefinition
+attribute [deprecated Module (since := "2023-12-21")] UserWidgetDefinition
 
 end Lean.Widget