From 4c552309d4405c1676f641c571d464af51aa18ce Mon Sep 17 00:00:00 2001 From: Wojciech Rozowski Date: Thu, 9 Jul 2026 17:17:26 +0000 Subject: [PATCH 1/7] refactor: `registerParametricAttribute` --- src/Lean/Attributes.lean | 36 +++++++++++++++++++++++++++++++----- 1 file changed, 31 insertions(+), 5 deletions(-) diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean index a0dedc7f44f5..9ff8d923c04e 100644 --- a/src/Lean/Attributes.lean +++ b/src/Lean/Attributes.lean @@ -260,22 +260,44 @@ structure ParametricAttributeImpl (α : Type) extends AttributeImplCore where filterExport : Environment → Name → α → Bool := fun env n _ => env.contains (skipRealize := false) n -def registerParametricAttribute (impl : ParametricAttributeImpl α) : IO (ParametricAttribute α) := do - let ext : PersistentEnvExtension (Name × α) (Name × α) (List Name × NameMap α) ← registerPersistentEnvExtension { - name := impl.ref +/-- +Registers the persistent environment extension backing a parametric attribute. + +This takes the extension-relevant fields directly rather than a `ParametricAttributeImpl`, so the +extension can be created independently of the attribute's `getParam`. This lets `getParam` consult +the extension (via `getParam?`) for entries set on other declarations — see +`registerParametricAttributeForExt`. +-/ +def registerParametricAttributeExt (ref : Name) (preserveOrder : Bool := false) + (filterExport : Environment → Name → α → Bool := fun env n _ => + env.contains (skipRealize := false) n) : + IO (PersistentEnvExtension (Name × α) (Name × α) (List Name × NameMap α)) := + registerPersistentEnvExtension { + name := ref mkInitial := pure ([], {}) addImportedFn := fun _ => pure ([], {}) addEntryFn := fun (decls, m) (p : Name × α) => (p.1 :: decls, m.insert p.1 p.2) exportEntriesFnEx := fun env (decls, m) => Id.run do - let all := if impl.preserveOrder then + let all := if preserveOrder then decls.toArray.reverse.filterMap (fun n => return (n, ← m.find? n)) else let r := m.foldl (fun a n p => a.push (n, p)) #[] r.qsort (fun a b => Name.quickLt a.1 b.1) - let exported := all.filter (fun ⟨n, a⟩ => impl.filterExport env n a) + let exported := all.filter (fun ⟨n, a⟩ => filterExport env n a) { exported, server := exported, «private» := all } statsFn := fun (_, m) => "parametric attribute" ++ Format.line ++ "number of local entries: " ++ format m.size } + +/-- +Registers a parametric attribute over an already-created extension `ext` (see +`registerParametricAttributeExt`). + +`ext` must have been created with the same `preserveOrder` as `impl`, otherwise `getParam?` and the +export logic will disagree on how entries are ordered. +-/ +def registerParametricAttributeForExt (impl : ParametricAttributeImpl α) + (ext : PersistentEnvExtension (Name × α) (Name × α) (List Name × NameMap α)) : + IO (ParametricAttribute α) := do let attrImpl : AttributeImpl := { impl.toAttributeImplCore with add := fun decl stx kind => do @@ -290,6 +312,10 @@ def registerParametricAttribute (impl : ParametricAttributeImpl α) : IO (Parame registerBuiltinAttribute attrImpl pure { attr := attrImpl, ext, preserveOrder := impl.preserveOrder } +def registerParametricAttribute (impl : ParametricAttributeImpl α) : IO (ParametricAttribute α) := do + let ext ← registerParametricAttributeExt (α := α) impl.ref impl.preserveOrder impl.filterExport + registerParametricAttributeForExt impl ext + namespace ParametricAttribute def getParam? [Inhabited α] (attr : ParametricAttribute α) (env : Environment) (decl : Name) : Option α := From 441f43ab0377ee2834a8ee49df29a87bdad8dfc5 Mon Sep 17 00:00:00 2001 From: Wojciech Rozowski Date: Thu, 16 Jul 2026 18:47:57 +0000 Subject: [PATCH 2/7] feat: warn on transitive deprecations --- src/Lean/Attributes.lean | 28 +++++-- src/Lean/Linter/Deprecated.lean | 79 ++++++++++++++++- tests/elab/7993.lean | 3 + tests/elab/deprecatedTransitive.lean | 121 +++++++++++++++++++++++++++ 4 files changed, 220 insertions(+), 11 deletions(-) create mode 100644 tests/elab/deprecatedTransitive.lean diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean index 9ff8d923c04e..a0d6c60a498d 100644 --- a/src/Lean/Attributes.lean +++ b/src/Lean/Attributes.lean @@ -318,17 +318,29 @@ def registerParametricAttribute (impl : ParametricAttributeImpl α) : IO (Parame namespace ParametricAttribute -def getParam? [Inhabited α] (attr : ParametricAttribute α) (env : Environment) (decl : Name) : Option α := +/-- +Looks up the parameter stored for `decl` directly in an extension `ext` (see +`registerParametricAttributeExt`), without needing the full `ParametricAttribute`. This lets a +parametric attribute's `getParam` consult its own extension for entries set on *other* declarations, +which is otherwise impossible because the `ParametricAttribute` value does not yet exist while +`getParam` runs. + +`preserveOrder` must match the value the extension was created with. +-/ +def getParamFromExt? [Inhabited α] + (ext : PersistentEnvExtension (Name × α) (Name × α) (List Name × NameMap α)) + (preserveOrder : Bool) (env : Environment) (decl : Name) : Option α := match env.getModuleIdxFor? decl with | some modIdx => - let entry? := if attr.preserveOrder then - (attr.ext.getModuleEntries env modIdx).find? (·.1 == decl) + let entry? := if preserveOrder then + (ext.getModuleEntries env modIdx).find? (·.1 == decl) else - (attr.ext.getModuleEntries env modIdx).binSearch (decl, default) (fun a b => Name.quickLt a.1 b.1) - match entry? with - | some (_, val) => some val - | none => none - | none => (attr.ext.getState env).2.find? decl + (ext.getModuleEntries env modIdx).binSearch (decl, default) (fun a b => Name.quickLt a.1 b.1) + entry?.map (·.2) + | none => (ext.getState env).2.find? decl + +def getParam? [Inhabited α] (attr : ParametricAttribute α) (env : Environment) (decl : Name) : Option α := + getParamFromExt? attr.ext attr.preserveOrder env decl def setParam (attr : ParametricAttribute α) (env : Environment) (decl : Name) (param : α) : Except String Environment := if (env.getModuleIdxFor? decl).isSome then diff --git a/src/Lean/Linter/Deprecated.lean b/src/Lean/Linter/Deprecated.lean index d742eff0bad9..1cfe3cfb00de 100644 --- a/src/Lean/Linter/Deprecated.lean +++ b/src/Lean/Linter/Deprecated.lean @@ -21,22 +21,95 @@ register_builtin_option linter.deprecated : Bool := { descr := "if true, generate deprecation warnings" } +register_builtin_option linter.deprecated.transitiveFuel : Nat := { + defValue := 100 + descr := "maximum number of steps to follow when checking whether a `@[deprecated]` attribute \ + points at a declaration that is itself deprecated; set to 0 to disable that check" +} + structure DeprecationEntry where newName? : Option Name := none text? : Option String := none since? : Option String := none deriving Inhabited -builtin_initialize deprecatedAttr : ParametricAttribute DeprecationEntry ← - registerParametricAttribute { +/-- Outcome of following a chain of `@[deprecated]` redirections. See `followDeprecation`. -/ +inductive TransitiveDeprecation where + /-- The chain ends at `finalName`, which is not itself deprecated. -/ + | replacement (finalName : Name) + /-- The chain ends at `lastName`, which is deprecated without an explicit replacement. -/ + | noReplacement (lastName : Name) + /-- The chain is longer than the allotted fuel. -/ + | exhausted + +/-- +Follows the chain of deprecations starting at `name`, using at most `fuel` steps: as long as the +current declaration is deprecated in favor of another declaration, moves on to that declaration. +`getEntry` looks up the `DeprecationEntry` (if any) for a declaration. +-/ +def followDeprecation (getEntry : Name → Option DeprecationEntry) : + Nat → Name → TransitiveDeprecation + | 0, _ => .exhausted + | fuel + 1, name => + match getEntry name with + | none => .replacement name + | some entry => + match entry.newName? with + | none => .noReplacement name + -- guard against a declaration deprecated in favor of itself + | some next => if next == name then .noReplacement name + else followDeprecation getEntry fuel next + +open Meta in +/-- +If the initial declaration `oldName` and its suggested replacement `newName` have different types +(up to reducible defeq), returns an explanatory note. Used to flag that a transitive replacement may +not be a drop-in substitute. +-/ +def deprecationTypeMismatchNote? (oldName newName : Name) : CoreM (Option MessageData) := do + let env ← getEnv + let some old := env.find? oldName | return none + let some new := env.find? newName | return none + if ← MetaM.run' <| withReducible <| isDefEqGuarded old.type new.type then + return none + return some <| .note m!"The suggested replacement has a different type:{indentExpr new.type}\ + \ninstead of{indentExpr old.type}" + +builtin_initialize deprecatedAttr : ParametricAttribute DeprecationEntry ← do + let ext ← registerParametricAttributeExt (α := DeprecationEntry) `deprecated + registerParametricAttributeForExt (ext := ext) { name := `deprecated descr := "mark declaration as deprecated", - getParam := fun _ stx => do + getParam := fun declName stx => do let `(attr| deprecated $[$id?]? $[$text?]? $[(since := $since?)]?) := stx | throwError "Invalid `[deprecated]` attribute syntax" let newName? ← id?.mapM Elab.realizeGlobalConstNoOverloadWithInfo if let some newName := newName? then recordExtraModUseFromDecl (isMeta := false) newName + -- Warn if `newName` is itself deprecated, so the deprecation points at the ultimate target. + let fuel := linter.deprecated.transitiveFuel.get (← getOptions) + if fuel > 0 && getLinterValue linter.deprecated (← getLinterOptions) then + let env ← getEnv + let getEntry n := ParametricAttribute.getParamFromExt? ext (preserveOrder := false) env n + match followDeprecation getEntry fuel newName with + | .replacement finalName => + if finalName != newName && finalName != declName then + let mut msg := m!"`{.ofConstName newName true}` is itself deprecated in favor of \ + `{.ofConstName finalName true}`; consider deprecating `{.ofConstName declName true}` \ + in favor of `{.ofConstName finalName true}` instead" + if let some note ← deprecationTypeMismatchNote? declName finalName then + msg := msg ++ note + logWarning msg + | .noReplacement lastName => + let via := if lastName == newName then m!"" + else m!" (via a chain of deprecations ending at `{.ofConstName lastName true}`)" + logWarning m!"`{.ofConstName newName true}` is itself deprecated{via}, but without an \ + explicit replacement; `{.ofConstName declName true}` is being deprecated in favor of \ + a deprecated declaration" + | .exhausted => + logWarning m!"the deprecation chain starting at `{.ofConstName newName true}` exceeds \ + {fuel} steps; consider deprecating `{.ofConstName declName true}` in favor of a \ + non-deprecated declaration" let text? := text?.map TSyntax.getString let since? := since?.map TSyntax.getString if id?.isNone && text?.isNone then diff --git a/tests/elab/7993.lean b/tests/elab/7993.lean index a2c354197b6e..467f7fcb53ee 100644 --- a/tests/elab/7993.lean +++ b/tests/elab/7993.lean @@ -35,6 +35,9 @@ example := foo abbrev Bar := Nat +-- `Foo.foo` is itself deprecated in favor of `Foo.bar`, so deprecating `Bar.bar` towards it warns. +/-- warning: `Foo.foo` is itself deprecated in favor of `Foo.bar`; consider deprecating `Bar.bar` in favor of `Foo.bar` instead -/ +#guard_msgs in @[deprecated Foo.foo (since := "2025-01-01")] def Bar.bar : Bar → Bar := id diff --git a/tests/elab/deprecatedTransitive.lean b/tests/elab/deprecatedTransitive.lean new file mode 100644 index 000000000000..a0b57c486088 --- /dev/null +++ b/tests/elab/deprecatedTransitive.lean @@ -0,0 +1,121 @@ +/-! +# Warn when a `@[deprecated]` attribute points at an already-deprecated declaration + +When `A` is deprecated in favor of `B`, and `B` is itself deprecated in favor of `C`, the +deprecation of `A` should point at `C` instead of `B`. The `@[deprecated]` attribute follows the +chain of deprecations (bounded by `linter.deprecated.transitiveFuel`) and warns accordingly. +-/ + +set_option linter.deprecated true + +def c1 : Nat := 0 + +@[deprecated c1 (since := "2020-01-01")] +def b1 : Nat := 0 + +/-- warning: `b1` is itself deprecated in favor of `c1`; consider deprecating `a1` in favor of `c1` instead -/ +#guard_msgs in +@[deprecated b1 (since := "2020-01-01")] +def a1 : Nat := 0 + +/-! Longer chain: `a2 → b2 → c2 → d2`, endpoint `d2`. -/ + +def d2 : Nat := 0 + +set_option linter.deprecated false in +@[deprecated d2 (since := "2020-01-01")] +def c2 : Nat := 0 + +set_option linter.deprecated false in +@[deprecated c2 (since := "2020-01-01")] +def b2 : Nat := 0 + +/-- warning: `b2` is itself deprecated in favor of `d2`; consider deprecating `a2` in favor of `d2` instead -/ +#guard_msgs in +@[deprecated b2 (since := "2020-01-01")] +def a2 : Nat := 0 + +/-! Text-only terminal: `b3` is deprecated without an explicit replacement. -/ + +@[deprecated "no replacement" (since := "2020-01-01")] +def b3 : Nat := 0 + +/-- warning: `b3` is itself deprecated, but without an explicit replacement; `a3` is being deprecated in favor of a deprecated declaration -/ +#guard_msgs in +@[deprecated b3 (since := "2020-01-01")] +def a3 : Nat := 0 + +/-! Chain ending at a text-only deprecation. -/ + +@[deprecated "no replacement" (since := "2020-01-01")] +def c4 : Nat := 0 + +set_option linter.deprecated false in +@[deprecated c4 (since := "2020-01-01")] +def b4 : Nat := 0 + +/-- warning: `b4` is itself deprecated (via a chain of deprecations ending at `c4`), but without an explicit replacement; `a4` is being deprecated in favor of a deprecated declaration -/ +#guard_msgs in +@[deprecated b4 (since := "2020-01-01")] +def a4 : Nat := 0 + +/-! Type disagreement between the initial declaration and the final replacement. -/ + +def c5 : Bool := true + +@[deprecated c5 (since := "2020-01-01")] +def b5 : Bool := true + +/-- +warning: `b5` is itself deprecated in favor of `c5`; consider deprecating `a5` in favor of `c5` instead + +Note: The suggested replacement has a different type: + Bool +instead of + Nat +-/ +#guard_msgs in +@[deprecated b5 (since := "2020-01-01")] +def a5 : Nat := 0 + +/-! No warning when the target is not itself deprecated. -/ + +def c6 : Nat := 0 + +#guard_msgs in +@[deprecated c6 (since := "2020-01-01")] +def a6 : Nat := 0 + +/-! Fuel: a chain longer than the fuel budget reports exhaustion instead of following it fully. -/ + +def e0 : Nat := 0 + +set_option linter.deprecated false in +@[deprecated e0 (since := "2020-01-01")] +def e1 : Nat := 0 + +set_option linter.deprecated false in +@[deprecated e1 (since := "2020-01-01")] +def e2 : Nat := 0 + +set_option linter.deprecated false in +@[deprecated e2 (since := "2020-01-01")] +def e3 : Nat := 0 + +set_option linter.deprecated.transitiveFuel 2 in +/-- warning: the deprecation chain starting at `e3` exceeds 2 steps; consider deprecating `a7` in favor of a non-deprecated declaration -/ +#guard_msgs in +@[deprecated e3 (since := "2020-01-01")] +def a7 : Nat := 0 + +/-! Disabling via fuel 0 suppresses the transitive check. -/ + +def c8 : Nat := 0 + +@[deprecated c8 (since := "2020-01-01")] +def b8 : Nat := 0 + +set_option linter.deprecated.transitiveFuel 0 in +#guard_msgs in +@[deprecated b8 (since := "2020-01-01")] +def a8 : Nat := 0 From 8e4a1e58e7e7129ac0bd51a3fc52f7db7840f9b4 Mon Sep 17 00:00:00 2001 From: Wojciech Rozowski Date: Mon, 20 Jul 2026 11:17:20 +0000 Subject: [PATCH 3/7] chore: refactor `gerParam?` and `setParam` --- src/Lean/Attributes.lean | 44 +++++++++++++++++----------------------- 1 file changed, 19 insertions(+), 25 deletions(-) diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean index 9ff8d923c04e..0dc4a0096c05 100644 --- a/src/Lean/Attributes.lean +++ b/src/Lean/Attributes.lean @@ -260,14 +260,6 @@ structure ParametricAttributeImpl (α : Type) extends AttributeImplCore where filterExport : Environment → Name → α → Bool := fun env n _ => env.contains (skipRealize := false) n -/-- -Registers the persistent environment extension backing a parametric attribute. - -This takes the extension-relevant fields directly rather than a `ParametricAttributeImpl`, so the -extension can be created independently of the attribute's `getParam`. This lets `getParam` consult -the extension (via `getParam?`) for entries set on other declarations — see -`registerParametricAttributeForExt`. --/ def registerParametricAttributeExt (ref : Name) (preserveOrder : Bool := false) (filterExport : Environment → Name → α → Bool := fun env n _ => env.contains (skipRealize := false) n) : @@ -288,13 +280,6 @@ def registerParametricAttributeExt (ref : Name) (preserveOrder : Bool := false) statsFn := fun (_, m) => "parametric attribute" ++ Format.line ++ "number of local entries: " ++ format m.size } -/-- -Registers a parametric attribute over an already-created extension `ext` (see -`registerParametricAttributeExt`). - -`ext` must have been created with the same `preserveOrder` as `impl`, otherwise `getParam?` and the -export logic will disagree on how entries are ordered. --/ def registerParametricAttributeForExt (impl : ParametricAttributeImpl α) (ext : PersistentEnvExtension (Name × α) (Name × α) (List Name × NameMap α)) : IO (ParametricAttribute α) := do @@ -318,25 +303,34 @@ def registerParametricAttribute (impl : ParametricAttributeImpl α) : IO (Parame namespace ParametricAttribute -def getParam? [Inhabited α] (attr : ParametricAttribute α) (env : Environment) (decl : Name) : Option α := +def getParamFromExt? [Inhabited α] + (ext : PersistentEnvExtension (Name × α) (Name × α) (List Name × NameMap α)) + (preserveOrder : Bool) (env : Environment) (decl : Name) : Option α := match env.getModuleIdxFor? decl with | some modIdx => - let entry? := if attr.preserveOrder then - (attr.ext.getModuleEntries env modIdx).find? (·.1 == decl) + let entry? := if preserveOrder then + (ext.getModuleEntries env modIdx).find? (·.1 == decl) else - (attr.ext.getModuleEntries env modIdx).binSearch (decl, default) (fun a b => Name.quickLt a.1 b.1) + (ext.getModuleEntries env modIdx).binSearch (decl, default) (fun a b => Name.quickLt a.1 b.1) match entry? with | some (_, val) => some val | none => none - | none => (attr.ext.getState env).2.find? decl + | none => (ext.getState env).2.find? decl -def setParam (attr : ParametricAttribute α) (env : Environment) (decl : Name) (param : α) : Except String Environment := +def getParam? [Inhabited α] (attr : ParametricAttribute α) (env : Environment) (decl : Name) : Option α := + getParamFromExt? attr.ext attr.preserveOrder env decl + +def setParamFromExt + (ext : PersistentEnvExtension (Name × α) (Name × α) (List Name × NameMap α)) (attr : AttributeImpl) (env : Environment) (decl : Name) (param : α) : Except String Environment := if (env.getModuleIdxFor? decl).isSome then - Except.error (s!"Failed to add parametric attribute `[{attr.attr.name}]` to `{decl}`: Declaration is in an imported module") - else if ((attr.ext.getState env).2.find? decl).isSome then - Except.error (s!"Failed to add parametric attribute `[{attr.attr.name}]` to `{decl}`: Attribute has already been set") + Except.error (s!"Failed to add parametric attribute `[{attr.name}]` to `{decl}`: Declaration is in an imported module") + else if ((ext.getState env).2.find? decl).isSome then + Except.error (s!"Failed to add parametric attribute `[{attr.name}]` to `{decl}`: Attribute has already been set") else - Except.ok (attr.ext.addEntry env (decl, param)) + Except.ok (ext.addEntry env (decl, param)) + +def setParam (attr : ParametricAttribute α) (env : Environment) (decl : Name) (param : α) : Except String Environment := + setParamFromExt attr.ext attr.attr env decl param end ParametricAttribute From ee4b7870682065bab19a300f31e079c38d53c1df Mon Sep 17 00:00:00 2001 From: Wojciech Rozowski Date: Mon, 20 Jul 2026 11:38:21 +0000 Subject: [PATCH 4/7] chore: cleanup --- src/Lean/Linter/Deprecated.lean | 12 +----------- 1 file changed, 1 insertion(+), 11 deletions(-) diff --git a/src/Lean/Linter/Deprecated.lean b/src/Lean/Linter/Deprecated.lean index 1cfe3cfb00de..853707d9d9de 100644 --- a/src/Lean/Linter/Deprecated.lean +++ b/src/Lean/Linter/Deprecated.lean @@ -33,7 +33,6 @@ structure DeprecationEntry where since? : Option String := none deriving Inhabited -/-- Outcome of following a chain of `@[deprecated]` redirections. See `followDeprecation`. -/ inductive TransitiveDeprecation where /-- The chain ends at `finalName`, which is not itself deprecated. -/ | replacement (finalName : Name) @@ -42,11 +41,6 @@ inductive TransitiveDeprecation where /-- The chain is longer than the allotted fuel. -/ | exhausted -/-- -Follows the chain of deprecations starting at `name`, using at most `fuel` steps: as long as the -current declaration is deprecated in favor of another declaration, moves on to that declaration. -`getEntry` looks up the `DeprecationEntry` (if any) for a declaration. --/ def followDeprecation (getEntry : Name → Option DeprecationEntry) : Nat → Name → TransitiveDeprecation | 0, _ => .exhausted @@ -61,11 +55,7 @@ def followDeprecation (getEntry : Name → Option DeprecationEntry) : else followDeprecation getEntry fuel next open Meta in -/-- -If the initial declaration `oldName` and its suggested replacement `newName` have different types -(up to reducible defeq), returns an explanatory note. Used to flag that a transitive replacement may -not be a drop-in substitute. --/ + def deprecationTypeMismatchNote? (oldName newName : Name) : CoreM (Option MessageData) := do let env ← getEnv let some old := env.find? oldName | return none From 1315d2c84b723dd7cba4cd180949a25b85aef910 Mon Sep 17 00:00:00 2001 From: Wojciech Rozowski Date: Mon, 20 Jul 2026 15:28:58 +0000 Subject: [PATCH 5/7] chore: fix the extension name --- src/Lean/Linter/Deprecated.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Linter/Deprecated.lean b/src/Lean/Linter/Deprecated.lean index 853707d9d9de..4e8b0d819d03 100644 --- a/src/Lean/Linter/Deprecated.lean +++ b/src/Lean/Linter/Deprecated.lean @@ -66,7 +66,7 @@ def deprecationTypeMismatchNote? (oldName newName : Name) : CoreM (Option Messag \ninstead of{indentExpr old.type}" builtin_initialize deprecatedAttr : ParametricAttribute DeprecationEntry ← do - let ext ← registerParametricAttributeExt (α := DeprecationEntry) `deprecated + let ext ← registerParametricAttributeExt (α := DeprecationEntry) `Lean.Linter.deprecatedAttr registerParametricAttributeForExt (ext := ext) { name := `deprecated descr := "mark declaration as deprecated", From b0abfd5016ec78ff56abf44124e822d9028c79f3 Mon Sep 17 00:00:00 2001 From: Wojciech Rozowski Date: Tue, 21 Jul 2026 11:41:36 +0000 Subject: [PATCH 6/7] chore: change the check to be one-step only --- src/Lean/Linter/Deprecated.lean | 71 +++++++++------------------- tests/elab/deprecatedTransitive.lean | 50 +++++++------------- 2 files changed, 40 insertions(+), 81 deletions(-) diff --git a/src/Lean/Linter/Deprecated.lean b/src/Lean/Linter/Deprecated.lean index 4e8b0d819d03..e0e02f62dded 100644 --- a/src/Lean/Linter/Deprecated.lean +++ b/src/Lean/Linter/Deprecated.lean @@ -21,10 +21,10 @@ register_builtin_option linter.deprecated : Bool := { descr := "if true, generate deprecation warnings" } -register_builtin_option linter.deprecated.transitiveFuel : Nat := { - defValue := 100 - descr := "maximum number of steps to follow when checking whether a `@[deprecated]` attribute \ - points at a declaration that is itself deprecated; set to 0 to disable that check" +register_builtin_option linter.deprecated.deprecatedTarget : Bool := { + defValue := true + descr := "if true, warn when a `@[deprecated]` attribute points at a declaration that is \ + itself deprecated" } structure DeprecationEntry where @@ -33,29 +33,7 @@ structure DeprecationEntry where since? : Option String := none deriving Inhabited -inductive TransitiveDeprecation where - /-- The chain ends at `finalName`, which is not itself deprecated. -/ - | replacement (finalName : Name) - /-- The chain ends at `lastName`, which is deprecated without an explicit replacement. -/ - | noReplacement (lastName : Name) - /-- The chain is longer than the allotted fuel. -/ - | exhausted - -def followDeprecation (getEntry : Name → Option DeprecationEntry) : - Nat → Name → TransitiveDeprecation - | 0, _ => .exhausted - | fuel + 1, name => - match getEntry name with - | none => .replacement name - | some entry => - match entry.newName? with - | none => .noReplacement name - -- guard against a declaration deprecated in favor of itself - | some next => if next == name then .noReplacement name - else followDeprecation getEntry fuel next - open Meta in - def deprecationTypeMismatchNote? (oldName newName : Name) : CoreM (Option MessageData) := do let env ← getEnv let some old := env.find? oldName | return none @@ -76,30 +54,25 @@ builtin_initialize deprecatedAttr : ParametricAttribute DeprecationEntry ← do let newName? ← id?.mapM Elab.realizeGlobalConstNoOverloadWithInfo if let some newName := newName? then recordExtraModUseFromDecl (isMeta := false) newName - -- Warn if `newName` is itself deprecated, so the deprecation points at the ultimate target. - let fuel := linter.deprecated.transitiveFuel.get (← getOptions) - if fuel > 0 && getLinterValue linter.deprecated (← getLinterOptions) then + if getLinterValue linter.deprecated (← getLinterOptions) + && linter.deprecated.deprecatedTarget.get (← getOptions) then let env ← getEnv - let getEntry n := ParametricAttribute.getParamFromExt? ext (preserveOrder := false) env n - match followDeprecation getEntry fuel newName with - | .replacement finalName => - if finalName != newName && finalName != declName then - let mut msg := m!"`{.ofConstName newName true}` is itself deprecated in favor of \ - `{.ofConstName finalName true}`; consider deprecating `{.ofConstName declName true}` \ - in favor of `{.ofConstName finalName true}` instead" - if let some note ← deprecationTypeMismatchNote? declName finalName then - msg := msg ++ note - logWarning msg - | .noReplacement lastName => - let via := if lastName == newName then m!"" - else m!" (via a chain of deprecations ending at `{.ofConstName lastName true}`)" - logWarning m!"`{.ofConstName newName true}` is itself deprecated{via}, but without an \ - explicit replacement; `{.ofConstName declName true}` is being deprecated in favor of \ - a deprecated declaration" - | .exhausted => - logWarning m!"the deprecation chain starting at `{.ofConstName newName true}` exceeds \ - {fuel} steps; consider deprecating `{.ofConstName declName true}` in favor of a \ - non-deprecated declaration" + match ParametricAttribute.getParamFromExt? ext (preserveOrder := false) env newName with + | none => pure () + | some entry => + match entry.newName? with + | some next => + if next != newName && next != declName then + let mut msg := m!"`{.ofConstName newName true}` is itself deprecated in favor of \ + `{.ofConstName next true}`; consider deprecating `{.ofConstName declName true}` \ + in favor of `{.ofConstName next true}` instead" + if let some note ← deprecationTypeMismatchNote? declName next then + msg := msg ++ note + logWarning msg + | none => + logWarning m!"`{.ofConstName newName true}` is itself deprecated, but without an \ + explicit replacement; `{.ofConstName declName true}` is being deprecated in favor \ + of a deprecated declaration" let text? := text?.map TSyntax.getString let since? := since?.map TSyntax.getString if id?.isNone && text?.isNone then diff --git a/tests/elab/deprecatedTransitive.lean b/tests/elab/deprecatedTransitive.lean index a0b57c486088..e1fdfd404d15 100644 --- a/tests/elab/deprecatedTransitive.lean +++ b/tests/elab/deprecatedTransitive.lean @@ -1,9 +1,10 @@ /-! # Warn when a `@[deprecated]` attribute points at an already-deprecated declaration -When `A` is deprecated in favor of `B`, and `B` is itself deprecated in favor of `C`, the -deprecation of `A` should point at `C` instead of `B`. The `@[deprecated]` attribute follows the -chain of deprecations (bounded by `linter.deprecated.transitiveFuel`) and warns accordingly. +When `A` is deprecated in favor of `B`, and `B` is itself deprecated in favor of `C`, deprecating +`A` towards `B` is discouraged: `B`'s deprecation record points at `C`, so `A` should point at `C` +instead. The `@[deprecated]` attribute inspects `B`'s deprecation record (only one step) and warns +accordingly. The check can be turned off with `linter.deprecated.deprecatedTarget`. -/ set_option linter.deprecated true @@ -18,7 +19,7 @@ def b1 : Nat := 0 @[deprecated b1 (since := "2020-01-01")] def a1 : Nat := 0 -/-! Longer chain: `a2 → b2 → c2 → d2`, endpoint `d2`. -/ +/-! Longer chain `a2 → b2 → c2 → d2`: only one step is followed, so `a2` is pointed at `c2`. -/ def d2 : Nat := 0 @@ -30,7 +31,7 @@ set_option linter.deprecated false in @[deprecated c2 (since := "2020-01-01")] def b2 : Nat := 0 -/-- warning: `b2` is itself deprecated in favor of `d2`; consider deprecating `a2` in favor of `d2` instead -/ +/-- warning: `b2` is itself deprecated in favor of `c2`; consider deprecating `a2` in favor of `c2` instead -/ #guard_msgs in @[deprecated b2 (since := "2020-01-01")] def a2 : Nat := 0 @@ -45,7 +46,7 @@ def b3 : Nat := 0 @[deprecated b3 (since := "2020-01-01")] def a3 : Nat := 0 -/-! Chain ending at a text-only deprecation. -/ +/-! One step at a target that is itself text-only deprecated: `a4` is pointed at `c4`. -/ @[deprecated "no replacement" (since := "2020-01-01")] def c4 : Nat := 0 @@ -54,12 +55,12 @@ set_option linter.deprecated false in @[deprecated c4 (since := "2020-01-01")] def b4 : Nat := 0 -/-- warning: `b4` is itself deprecated (via a chain of deprecations ending at `c4`), but without an explicit replacement; `a4` is being deprecated in favor of a deprecated declaration -/ +/-- warning: `b4` is itself deprecated in favor of `c4`; consider deprecating `a4` in favor of `c4` instead -/ #guard_msgs in @[deprecated b4 (since := "2020-01-01")] def a4 : Nat := 0 -/-! Type disagreement between the initial declaration and the final replacement. -/ +/-! Type disagreement between the initial declaration and the suggested replacement. -/ def c5 : Bool := true @@ -86,36 +87,21 @@ def c6 : Nat := 0 @[deprecated c6 (since := "2020-01-01")] def a6 : Nat := 0 -/-! Fuel: a chain longer than the fuel budget reports exhaustion instead of following it fully. -/ - -def e0 : Nat := 0 - -set_option linter.deprecated false in -@[deprecated e0 (since := "2020-01-01")] -def e1 : Nat := 0 - -set_option linter.deprecated false in -@[deprecated e1 (since := "2020-01-01")] -def e2 : Nat := 0 - -set_option linter.deprecated false in -@[deprecated e2 (since := "2020-01-01")] -def e3 : Nat := 0 - -set_option linter.deprecated.transitiveFuel 2 in -/-- warning: the deprecation chain starting at `e3` exceeds 2 steps; consider deprecating `a7` in favor of a non-deprecated declaration -/ -#guard_msgs in -@[deprecated e3 (since := "2020-01-01")] -def a7 : Nat := 0 - -/-! Disabling via fuel 0 suppresses the transitive check. -/ +/-! Disabling via `linter.deprecated.deprecatedTarget` suppresses the check. -/ def c8 : Nat := 0 @[deprecated c8 (since := "2020-01-01")] def b8 : Nat := 0 -set_option linter.deprecated.transitiveFuel 0 in +set_option linter.deprecated.deprecatedTarget false in #guard_msgs in @[deprecated b8 (since := "2020-01-01")] def a8 : Nat := 0 + +/-! Turning off `linter.deprecated` entirely also suppresses the check. -/ + +set_option linter.deprecated false in +#guard_msgs in +@[deprecated b8 (since := "2020-01-01")] +def a9 : Nat := 0 From 630fdf942f37d8dddd71f7fe3d7799fa3efe118c Mon Sep 17 00:00:00 2001 From: Wojciech Rozowski Date: Wed, 22 Jul 2026 11:46:42 +0000 Subject: [PATCH 7/7] chore: add a disable message --- src/Lean/Linter/Deprecated.lean | 8 +++++--- tests/elab/7993.lean | 6 +++++- tests/elab/deprecatedTransitive.lean | 26 ++++++++++++++++++++++---- 3 files changed, 32 insertions(+), 8 deletions(-) diff --git a/src/Lean/Linter/Deprecated.lean b/src/Lean/Linter/Deprecated.lean index e0e02f62dded..454f0abfe364 100644 --- a/src/Lean/Linter/Deprecated.lean +++ b/src/Lean/Linter/Deprecated.lean @@ -60,6 +60,8 @@ builtin_initialize deprecatedAttr : ParametricAttribute DeprecationEntry ← do match ParametricAttribute.getParamFromExt? ext (preserveOrder := false) env newName with | none => pure () | some entry => + let disableNote : MessageData := .note m!"This warning can be disabled with \ + `set_option {linter.deprecated.deprecatedTarget.name} false`" match entry.newName? with | some next => if next != newName && next != declName then @@ -68,11 +70,11 @@ builtin_initialize deprecatedAttr : ParametricAttribute DeprecationEntry ← do in favor of `{.ofConstName next true}` instead" if let some note ← deprecationTypeMismatchNote? declName next then msg := msg ++ note - logWarning msg + logWarning <| msg ++ disableNote | none => - logWarning m!"`{.ofConstName newName true}` is itself deprecated, but without an \ + logWarning <| m!"`{.ofConstName newName true}` is itself deprecated, but without an \ explicit replacement; `{.ofConstName declName true}` is being deprecated in favor \ - of a deprecated declaration" + of a deprecated declaration" ++ disableNote let text? := text?.map TSyntax.getString let since? := since?.map TSyntax.getString if id?.isNone && text?.isNone then diff --git a/tests/elab/7993.lean b/tests/elab/7993.lean index 467f7fcb53ee..a8ec21cb9109 100644 --- a/tests/elab/7993.lean +++ b/tests/elab/7993.lean @@ -36,7 +36,11 @@ example := foo abbrev Bar := Nat -- `Foo.foo` is itself deprecated in favor of `Foo.bar`, so deprecating `Bar.bar` towards it warns. -/-- warning: `Foo.foo` is itself deprecated in favor of `Foo.bar`; consider deprecating `Bar.bar` in favor of `Foo.bar` instead -/ +/-- +warning: `Foo.foo` is itself deprecated in favor of `Foo.bar`; consider deprecating `Bar.bar` in favor of `Foo.bar` instead + +Note: This warning can be disabled with `set_option linter.deprecated.deprecatedTarget false` +-/ #guard_msgs in @[deprecated Foo.foo (since := "2025-01-01")] def Bar.bar : Bar → Bar := id diff --git a/tests/elab/deprecatedTransitive.lean b/tests/elab/deprecatedTransitive.lean index e1fdfd404d15..5a33e2aae5f1 100644 --- a/tests/elab/deprecatedTransitive.lean +++ b/tests/elab/deprecatedTransitive.lean @@ -14,7 +14,11 @@ def c1 : Nat := 0 @[deprecated c1 (since := "2020-01-01")] def b1 : Nat := 0 -/-- warning: `b1` is itself deprecated in favor of `c1`; consider deprecating `a1` in favor of `c1` instead -/ +/-- +warning: `b1` is itself deprecated in favor of `c1`; consider deprecating `a1` in favor of `c1` instead + +Note: This warning can be disabled with `set_option linter.deprecated.deprecatedTarget false` +-/ #guard_msgs in @[deprecated b1 (since := "2020-01-01")] def a1 : Nat := 0 @@ -31,7 +35,11 @@ set_option linter.deprecated false in @[deprecated c2 (since := "2020-01-01")] def b2 : Nat := 0 -/-- warning: `b2` is itself deprecated in favor of `c2`; consider deprecating `a2` in favor of `c2` instead -/ +/-- +warning: `b2` is itself deprecated in favor of `c2`; consider deprecating `a2` in favor of `c2` instead + +Note: This warning can be disabled with `set_option linter.deprecated.deprecatedTarget false` +-/ #guard_msgs in @[deprecated b2 (since := "2020-01-01")] def a2 : Nat := 0 @@ -41,7 +49,11 @@ def a2 : Nat := 0 @[deprecated "no replacement" (since := "2020-01-01")] def b3 : Nat := 0 -/-- warning: `b3` is itself deprecated, but without an explicit replacement; `a3` is being deprecated in favor of a deprecated declaration -/ +/-- +warning: `b3` is itself deprecated, but without an explicit replacement; `a3` is being deprecated in favor of a deprecated declaration + +Note: This warning can be disabled with `set_option linter.deprecated.deprecatedTarget false` +-/ #guard_msgs in @[deprecated b3 (since := "2020-01-01")] def a3 : Nat := 0 @@ -55,7 +67,11 @@ set_option linter.deprecated false in @[deprecated c4 (since := "2020-01-01")] def b4 : Nat := 0 -/-- warning: `b4` is itself deprecated in favor of `c4`; consider deprecating `a4` in favor of `c4` instead -/ +/-- +warning: `b4` is itself deprecated in favor of `c4`; consider deprecating `a4` in favor of `c4` instead + +Note: This warning can be disabled with `set_option linter.deprecated.deprecatedTarget false` +-/ #guard_msgs in @[deprecated b4 (since := "2020-01-01")] def a4 : Nat := 0 @@ -74,6 +90,8 @@ Note: The suggested replacement has a different type: Bool instead of Nat + +Note: This warning can be disabled with `set_option linter.deprecated.deprecatedTarget false` -/ #guard_msgs in @[deprecated b5 (since := "2020-01-01")]