diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean index ad43c494ee72..465e302d0caf 100644 --- a/src/Lean/Elab/DeclModifiers.lean +++ b/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 diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean index 38ecb9c28550..1034f13fa1a1 100644 --- a/src/Lean/Elab/Declaration.lean +++ b/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 diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 328d22c79936..e5ff695706fd 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/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) diff --git a/src/Lean/Elab/MutualInductive.lean b/src/Lean/Elab/MutualInductive.lean index 9ec41f655a08..2991bae5f1e6 100644 --- a/src/Lean/Elab/MutualInductive.lean +++ b/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 diff --git a/tests/elab/redundantDeprecatedWarnings.lean b/tests/elab/redundantDeprecatedWarnings.lean new file mode 100644 index 000000000000..d16f7ede570b --- /dev/null +++ b/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