feat: remove redundant deprecation warnings

src/Lean/Elab/DeclModifiers.lean

@@ -345,4 +345,21 @@ def expandDeclId (currNamespace : Name) (currLevelNames : List Name) (declId : S
 
 end Methods
 
+namespace Term
+
+/--
+If `attrs` contains an `@[deprecated]` attribute, runs the action with `Term.Context.checkDeprecated`
+disabled, suppressing the `linter.deprecated` warning that would otherwise fire when a deprecated
+constant is referenced. Otherwise, runs the action unchanged.
+
+This implements the suppression rule from RFC #8942: deprecation warnings should not fire inside
+the body of a declaration that is itself marked `@[deprecated]`, since the references will go away
+along with the declaration.
+-/
+@[inline] def withDeprecationContextFromAttrs [MonadWithReaderOf Term.Context m]
+    (attrs : Array Attribute) : m α → m α :=
+  if attrs.any (·.name == `deprecated) then withoutCheckDeprecated else id
+
+end Term
+
 end Lean.Elab

src/Lean/Elab/Declaration.lean

@@ -108,7 +108,7 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
     addDeclarationRangesForBuiltin declName modifiers.stx stx
     Term.withAutoBoundImplicit do
     Term.withAutoBoundImplicitForbiddenPred (fun n => shortName == n) do
-    Term.withDeclName declName <| Term.withLevelNames allUserLevelNames <| Term.elabBinders binders.getArgs fun xs => do
+    Term.withDeprecationContextFromAttrs modifiers.attrs <| Term.withDeclName declName <| Term.withLevelNames allUserLevelNames <| Term.elabBinders binders.getArgs fun xs => do
       Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.beforeElaboration
       let type ← Term.elabType typeStx
       Term.synthesizeSyntheticMVarsNoPostponing

src/Lean/Elab/MutualDef.lean

@@ -252,6 +252,7 @@ private def elabHeaders (views : Array DefView) (expandedDeclIds : Array ExpandD
         withTraceNode `Elab.definition.header (fun _ => pure declName) do
         withRestoreOrSaveFull reusableResult? none do
         withReuseContext view.headerRef do
+        withDeprecationContextFromAttrs view.modifiers.attrs do
         applyAttributesAt declName view.modifiers.attrs .beforeElaboration
         withDeclName declName <| withAutoBoundImplicit <| withLevelNames levelNames <|
           elabBindersEx view.binders.getArgs fun xs => do
@@ -528,7 +529,7 @@ private def elabFunValues (headers : Array DefViewElabHeader) (vars : Array Expr
     let (val, state) ← withRestoreOrSaveFull reusableResult? header.tacSnap? do
       withReuseContext header.value do
       withTraceNode `Elab.definition.value (fun _ => pure header.declName) do
-      withDeclName header.declName <| withLevelNames header.levelNames do
+      withDeprecationContextFromAttrs header.modifiers.attrs <| withDeclName header.declName <| withLevelNames header.levelNames do
       let valStx ← declValToTerm header.value header.type
       (if header.kind.isTheorem && !deprecated.oldSectionVars.get (← getOptions) then withHeaderSecVars vars sc #[header] else fun x => x #[]) fun vars => do
       withLCtx' ((← getLCtx).modifyLocalDecls fun decl => decl.setType decl.type.cleanupAnnotations) do
@@ -669,7 +670,8 @@ private def ExprWithHoles.getHoles (e : ExprWithHoles) : TermElabM (Array MVarId
   let goals ← goals.mapM fun goal => return ((← goal.getDecl).index, goal)
   return goals.insertionSort (·.fst < ·.fst) |>.map (·.snd)
 
-private def fillHolesFromWhereFinally (name : Name) (es : Array ExprWithHoles) (whereFinally : WhereFinallyView) : TermElabM PUnit := do
+private def fillHolesFromWhereFinally (name : Name) (es : Array ExprWithHoles) (whereFinally : WhereFinallyView)
+    (attrs : Array Attribute) : TermElabM PUnit := do
   if whereFinally.isNone then return
   let goals := (← es.mapM fun e => e.getHoles).flatten
 
@@ -689,6 +691,7 @@ private def fillHolesFromWhereFinally (name : Name) (es : Array ExprWithHoles) (
 
   withExporting (isExporting := wasExporting && !isNoLongerExporting) do
   Lean.Elab.Term.TermElabM.run' do
+  withDeprecationContextFromAttrs attrs do
   Term.withDeclName name do
   withRef whereFinally.ref do
     unless goals.isEmpty do
@@ -1293,6 +1296,8 @@ where
       async.commitSignature { name := header.declName, levelParams, type }
 
     -- attributes should be applied on the main thread; see below
+    -- save before clearing so the deprecation-silencing wrap below can still see `@[deprecated]`
+    let oldAttrs := header.modifiers.attrs
     let header := { header with modifiers.attrs := #[] }
 
     -- insert a hole for the proof info trees in the main info tree
@@ -1308,6 +1313,7 @@ where
     let act ←
       -- NOTE: We must set the decl name before going async to ensure that the `auxDeclNGen` is
       -- forked correctly.
+      withDeprecationContextFromAttrs oldAttrs do
       withDeclName header.declName do
       wrapAsyncAsSnapshot (desc := s!"elaborating proof of {declId.declName}")
         (cancelTk? := cancelTk) fun _ => do profileitM Exception "elaboration" (← getOptions) do
@@ -1329,8 +1335,9 @@ where
     Core.logSnapshotTask { stx? := none, cancelTk? := none, task := (← getEnv).checked.map fun _ =>
       default
     }
-    applyAttributesAt declId.declName view.modifiers.attrs .afterTypeChecking
-    applyAttributesAt declId.declName view.modifiers.attrs .afterCompilation
+    withDeprecationContextFromAttrs view.modifiers.attrs do
+      applyAttributesAt declId.declName view.modifiers.attrs .afterTypeChecking
+      applyAttributesAt declId.declName view.modifiers.attrs .afterCompilation
   finishElab headers := withFunLocalDecls headers fun funFVars => do
     let env ← getEnv
     let inExposeSection := sc.attrs.any (· matches `(attrInstance| expose))
@@ -1405,7 +1412,7 @@ where
     for header in headers, value in values do
       let whereFinally ← declValToWhereFinally header.value
       let exprsWithHoles := (exprsWithHoles.getD header.declName #[]).push { ref := header.ref, expr := value }
-      fillHolesFromWhereFinally header.declName exprsWithHoles whereFinally
+      fillHolesFromWhereFinally header.declName exprsWithHoles whereFinally header.modifiers.attrs
     -- Compilation should take place without unused section vars, but all section vars should be
     -- present when elaborating documentation.
     let docCtx := (← getLCtx, ← getLocalInstances)

src/Lean/Elab/MutualInductive.lean

@@ -324,7 +324,8 @@ private def elabHeadersAux (views : Array InductiveView) (i : Nat) (acc : Array
   Term.withAutoBoundImplicitForbiddenPred (fun n => views.any (·.shortDeclName == n)) do
     if h : i < views.size then
       let view := views[i]
-      let acc ← withRef view.ref <| Term.withAutoBoundImplicit <| Term.elabBinders view.binders.getArgs fun params => do
+      let acc ← withRef view.ref <| Term.withDeprecationContextFromAttrs view.modifiers.attrs <|
+          Term.withAutoBoundImplicit <| Term.elabBinders view.binders.getArgs fun params => do
         let (type, _) ← Term.withAutoBoundImplicit do
           let typeStx ← view.type?.getDM `(Sort _)
           let type ← Term.elabType typeStx
@@ -1458,7 +1459,8 @@ private def mkInductiveDeclCore
     for h : i in *...views.size do
       Term.addLocalVarInfo views[i].declId indFVars[i]!
       let r     := rs[i]!
-      let elab' ← elabs[i]!.elabCtors rs r params
+      let elab' ← Term.withDeprecationContextFromAttrs views[i].modifiers.attrs <|
+        elabs[i]!.elabCtors rs r params
       elabs'    := elabs'.push elab'
       indTypesArray := indTypesArray.push { name := r.view.declName, type := r.type, ctors := elab'.ctors }
     Term.synthesizeSyntheticMVarsNoPostponing

tests/elab/redundantDeprecatedWarnings.lean

@@ -0,0 +1,62 @@
+set_option linter.deprecated true
+
+def foo (x : Nat) := x + 1
+
+theorem bar (x : Nat) : foo x = x + 1 := rfl
+
+@[deprecated foo (since:="2025-06-23")]
+def baz (x : Nat) := x + 1
+
+@[deprecated foo (since:="2025-06-23")]
+def baz2 (x : Nat) := x + 1
+
+@[simp,deprecated bar (since:="2025-06-23")]
+theorem qux (x : Nat) : foo x = baz x := rfl
+
+@[deprecated bar (since:="2025-06-23")]
+theorem quux (x : Nat) : foo x = x + 1 := by
+  rw [qux x]
+  rfl
+
+@[simp, deprecated bar (since:="2025-06-23")]
+theorem qux2 (x : Nat) : foo x = baz x := rfl
+
+@[deprecated "test" (since:="2025-06-23")]
+inductive Hello : Prop where
+  | mk (n : Nat) : baz n = 7 → Hello
+
+@[deprecated "test" (since:="2025-06-23")]
+coinductive Hello2 : Prop where
+  | mk (n : Nat) : baz n = 7 → Hello2
+
+@[deprecated "test" (since:="2025-06-23")]
+inductive Hello3 (h : baz n = 7) where
+
+@[deprecated "test" (since:="2025-06-23")]
+axiom ax : baz n = 7
+
+@[deprecated "test" (since:="2025-06-23")]
+structure MyStruct where
+  n : Nat
+  hp : baz n = 7
+
+@[deprecated "test" (since:="2025-06-23")]
+structure MyStruct2 (n : Nat) (hp : baz n = 7) where
+
+@[deprecated "test" (since:="2025-06-23")]
+def myFun (n : Nat) : Nat := Id.run do
+  return baz n
+
+@[deprecated "test" (since:="2025-06-23")]
+instance : BEq Nat where
+  beq m n := m == baz n
+
+/-- warning: `baz` has been deprecated: Use `foo` instead -/
+#guard_msgs in
+mutual
+  inductive NotDep : Prop where
+    | mk : baz 0 = 0 → NotDep → DepInd → NotDep
+  @[deprecated "test" (since:="2025-06-23")]
+  inductive DepInd : Prop where
+    | mk : baz2 0 = 0 → NotDep → DepInd → DepInd
+end