From f70b7e5722da6101572869d87832494e2f8534b7 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 26 Nov 2024 19:45:54 +1100 Subject: [PATCH] feat: `@[deprecated]` requires a replacement identifier or message, and a `since` field (#6112) This PR makes stricter requirements for the `@[deprecated]` attribute, requiring either a replacement identifier as `@[deprecated bar]` or suggestion text `@[deprecated "Past its use by date"]`, and also requires a `since := "..."` field. --- src/Init/Data/List/Basic.lean | 4 +-- src/Init/Data/List/Lemmas.lean | 8 +++--- src/Init/Data/List/Sort/Lemmas.lean | 8 +++--- src/Init/Data/List/TakeDrop.lean | 2 +- src/Init/Data/Nat/Basic.lean | 6 ++--- src/Init/Data/UInt/Lemmas.lean | 30 ++++++++++----------- src/Init/GetElem.lean | 7 ++--- src/Lean/Linter/Deprecated.lean | 14 +++++++--- src/lake/Lake/Build/Basic.lean | 3 ++- src/lake/Lake/Build/Facets.lean | 4 +-- src/lake/Lake/Build/Info.lean | 4 +-- src/lake/Lake/Build/Package.lean | 4 +-- src/lake/Lake/Build/Trace.lean | 7 +++-- src/lake/Lake/Util/Log.lean | 6 +++-- tests/lean/4452.lean | 4 +-- tests/lean/4452.lean.expected.out | 4 +-- tests/lean/deprecated.lean.expected.out | 12 ++++++--- tests/lean/warningAsError.lean | 2 +- tests/lean/warningAsError.lean.expected.out | 4 +-- 19 files changed, 77 insertions(+), 56 deletions(-) diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean index e2624e5f90..1626fa78c4 100644 --- a/src/Init/Data/List/Basic.lean +++ b/src/Init/Data/List/Basic.lean @@ -231,7 +231,7 @@ theorem ext_get? : ∀ {l₁ l₂ : List α}, (∀ n, l₁.get? n = l₂.get? n) injection h0 with aa; simp only [aa, ext_get? fun n => h (n+1)] /-- Deprecated alias for `ext_get?`. The preferred extensionality theorem is now `ext_getElem?`. -/ -@[deprecated (since := "2024-06-07")] abbrev ext := @ext_get? +@[deprecated ext_get? (since := "2024-06-07")] abbrev ext := @ext_get? /-! ### getD -/ @@ -682,7 +682,7 @@ theorem elem_cons [BEq α] {a : α} : (b::bs).elem a = match a == b with | true => true | false => bs.elem a := rfl /-- `notElem a l` is `!(elem a l)`. -/ -@[deprecated (since := "2024-06-15")] +@[deprecated "Use `!(elem a l)` instead."(since := "2024-06-15")] def notElem [BEq α] (a : α) (as : List α) : Bool := !(as.elem a) diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index c078efe7de..5a5f9c1099 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -101,7 +101,7 @@ theorem tail_eq_of_cons_eq (H : h₁ :: t₁ = h₂ :: t₂) : t₁ = t₂ := (c theorem cons_inj_right (a : α) {l l' : List α} : a :: l = a :: l' ↔ l = l' := ⟨tail_eq_of_cons_eq, congrArg _⟩ -@[deprecated (since := "2024-06-15")] abbrev cons_inj := @cons_inj_right +@[deprecated cons_inj_right (since := "2024-06-15")] abbrev cons_inj := @cons_inj_right theorem cons_eq_cons {a b : α} {l l' : List α} : a :: l = b :: l' ↔ a = b ∧ l = l' := List.cons.injEq .. ▸ .rfl @@ -171,7 +171,7 @@ theorem get_cons_succ {as : List α} {h : i + 1 < (a :: as).length} : theorem get_cons_succ' {as : List α} {i : Fin as.length} : (a :: as).get i.succ = as.get i := rfl -@[deprecated (since := "2024-07-09")] +@[deprecated "Deprecated without replacement." (since := "2024-07-09")] theorem get_cons_cons_one : (a₁ :: a₂ :: as).get (1 : Fin (as.length + 2)) = a₂ := rfl theorem get_mk_zero : ∀ {l : List α} (h : 0 < l.length), l.get ⟨0, h⟩ = l.head (length_pos.mp h) @@ -1818,7 +1818,7 @@ theorem getElem_append_right' (l₁ : List α) {l₂ : List α} {n : Nat} (hn : l₂[n] = (l₁ ++ l₂)[n + l₁.length]'(by simpa [Nat.add_comm] using Nat.add_lt_add_left hn _) := by rw [getElem_append_right] <;> simp [*, le_add_left] -@[deprecated (since := "2024-06-12")] +@[deprecated "Deprecated without replacement." (since := "2024-06-12")] theorem get_append_right_aux {l₁ l₂ : List α} {n : Nat} (h₁ : l₁.length ≤ n) (h₂ : n < (l₁ ++ l₂).length) : n - l₁.length < l₂.length := by rw [length_append] at h₂ @@ -1835,7 +1835,7 @@ theorem getElem_of_append {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.l rw [← getElem?_eq_getElem, eq, getElem?_append_right (h ▸ Nat.le_refl _), h] simp -@[deprecated (since := "2024-06-12")] +@[deprecated "Deprecated without replacement." (since := "2024-06-12")] theorem get_of_append_proof {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.length = n) : n < length l := eq ▸ h ▸ by simp_arith diff --git a/src/Init/Data/List/Sort/Lemmas.lean b/src/Init/Data/List/Sort/Lemmas.lean index c798f096a2..494b82331f 100644 --- a/src/Init/Data/List/Sort/Lemmas.lean +++ b/src/Init/Data/List/Sort/Lemmas.lean @@ -293,7 +293,7 @@ theorem sorted_mergeSort apply sorted_mergeSort trans total termination_by l => l.length -@[deprecated (since := "2024-09-02")] abbrev mergeSort_sorted := @sorted_mergeSort +@[deprecated sorted_mergeSort (since := "2024-09-02")] abbrev mergeSort_sorted := @sorted_mergeSort /-- If the input list is already sorted, then `mergeSort` does not change the list. @@ -429,7 +429,8 @@ theorem sublist_mergeSort ((fun w => Sublist.of_sublist_append_right w h') fun b m₁ m₃ => (Bool.eq_not_self true).mp ((rel_of_pairwise_cons hc m₁).symm.trans (h₃ b m₃)))) -@[deprecated (since := "2024-09-02")] abbrev mergeSort_stable := @sublist_mergeSort +@[deprecated sublist_mergeSort (since := "2024-09-02")] +abbrev mergeSort_stable := @sublist_mergeSort /-- Another statement of stability of merge sort. @@ -442,7 +443,8 @@ theorem pair_sublist_mergeSort (hab : le a b) (h : [a, b] <+ l) : [a, b] <+ mergeSort l le := sublist_mergeSort trans total (pairwise_pair.mpr hab) h -@[deprecated (since := "2024-09-02")] abbrev mergeSort_stable_pair := @pair_sublist_mergeSort +@[deprecated pair_sublist_mergeSort(since := "2024-09-02")] +abbrev mergeSort_stable_pair := @pair_sublist_mergeSort theorem map_merge {f : α → β} {r : α → α → Bool} {s : β → β → Bool} {l l' : List α} (hl : ∀ a ∈ l, ∀ b ∈ l', r a b = s (f a) (f b)) : diff --git a/src/Init/Data/List/TakeDrop.lean b/src/Init/Data/List/TakeDrop.lean index c3ec7f3413..e6e5f33063 100644 --- a/src/Init/Data/List/TakeDrop.lean +++ b/src/Init/Data/List/TakeDrop.lean @@ -224,7 +224,7 @@ theorem take_succ {l : List α} {n : Nat} : l.take (n + 1) = l.take n ++ l[n]?.t · simp only [take, Option.toList, getElem?_cons_zero, nil_append] · simp only [take, hl, getElem?_cons_succ, cons_append] -@[deprecated (since := "2024-07-25")] +@[deprecated "Deprecated without replacement." (since := "2024-07-25")] theorem drop_sizeOf_le [SizeOf α] (l : List α) (n : Nat) : sizeOf (l.drop n) ≤ sizeOf l := by induction l generalizing n with | nil => rw [drop_nil]; apply Nat.le_refl diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean index 5b7d9d5542..aebae331e1 100644 --- a/src/Init/Data/Nat/Basic.lean +++ b/src/Init/Data/Nat/Basic.lean @@ -789,7 +789,7 @@ theorem pred_lt_of_lt {n m : Nat} (h : m < n) : pred n < n := pred_lt (not_eq_zero_of_lt h) set_option linter.missingDocs false in -@[deprecated (since := "2024-06-01")] abbrev pred_lt' := @pred_lt_of_lt +@[deprecated pred_lt_of_lt (since := "2024-06-01")] abbrev pred_lt' := @pred_lt_of_lt theorem sub_one_lt_of_lt {n m : Nat} (h : m < n) : n - 1 < n := sub_one_lt (not_eq_zero_of_lt h) @@ -1075,7 +1075,7 @@ theorem pred_mul (n m : Nat) : pred n * m = n * m - m := by | succ n => rw [Nat.pred_succ, succ_mul, Nat.add_sub_cancel] set_option linter.missingDocs false in -@[deprecated (since := "2024-06-01")] abbrev mul_pred_left := @pred_mul +@[deprecated pred_mul (since := "2024-06-01")] abbrev mul_pred_left := @pred_mul protected theorem sub_one_mul (n m : Nat) : (n - 1) * m = n * m - m := by cases n with @@ -1087,7 +1087,7 @@ theorem mul_pred (n m : Nat) : n * pred m = n * m - n := by rw [Nat.mul_comm, pred_mul, Nat.mul_comm] set_option linter.missingDocs false in -@[deprecated (since := "2024-06-01")] abbrev mul_pred_right := @mul_pred +@[deprecated mul_pred (since := "2024-06-01")] abbrev mul_pred_right := @mul_pred theorem mul_sub_one (n m : Nat) : n * (m - 1) = n * m - n := by rw [Nat.mul_comm, Nat.sub_one_mul , Nat.mul_comm] diff --git a/src/Init/Data/UInt/Lemmas.lean b/src/Init/Data/UInt/Lemmas.lean index b89a898647..0e4afa8cfd 100644 --- a/src/Init/Data/UInt/Lemmas.lean +++ b/src/Init/Data/UInt/Lemmas.lean @@ -145,22 +145,22 @@ theorem UInt32.toNat_le_of_le {n : UInt32} {m : Nat} (h : m < size) : n ≤ ofNa theorem UInt32.le_toNat_of_le {n : UInt32} {m : Nat} (h : m < size) : ofNat m ≤ n → m ≤ n.toNat := by simp [le_def, BitVec.le_def, UInt32.toNat, toBitVec_eq_of_lt h] -@[deprecated (since := "2024-06-23")] protected abbrev UInt8.zero_toNat := @UInt8.toNat_zero -@[deprecated (since := "2024-06-23")] protected abbrev UInt8.div_toNat := @UInt8.toNat_div -@[deprecated (since := "2024-06-23")] protected abbrev UInt8.mod_toNat := @UInt8.toNat_mod +@[deprecated UInt8.toNat_zero (since := "2024-06-23")] protected abbrev UInt8.zero_toNat := @UInt8.toNat_zero +@[deprecated UInt8.toNat_div (since := "2024-06-23")] protected abbrev UInt8.div_toNat := @UInt8.toNat_div +@[deprecated UInt8.toNat_mod (since := "2024-06-23")] protected abbrev UInt8.mod_toNat := @UInt8.toNat_mod -@[deprecated (since := "2024-06-23")] protected abbrev UInt16.zero_toNat := @UInt16.toNat_zero -@[deprecated (since := "2024-06-23")] protected abbrev UInt16.div_toNat := @UInt16.toNat_div -@[deprecated (since := "2024-06-23")] protected abbrev UInt16.mod_toNat := @UInt16.toNat_mod +@[deprecated UInt16.toNat_zero (since := "2024-06-23")] protected abbrev UInt16.zero_toNat := @UInt16.toNat_zero +@[deprecated UInt16.toNat_div (since := "2024-06-23")] protected abbrev UInt16.div_toNat := @UInt16.toNat_div +@[deprecated UInt16.toNat_mod (since := "2024-06-23")] protected abbrev UInt16.mod_toNat := @UInt16.toNat_mod -@[deprecated (since := "2024-06-23")] protected abbrev UInt32.zero_toNat := @UInt32.toNat_zero -@[deprecated (since := "2024-06-23")] protected abbrev UInt32.div_toNat := @UInt32.toNat_div -@[deprecated (since := "2024-06-23")] protected abbrev UInt32.mod_toNat := @UInt32.toNat_mod +@[deprecated UInt32.toNat_zero (since := "2024-06-23")] protected abbrev UInt32.zero_toNat := @UInt32.toNat_zero +@[deprecated UInt32.toNat_div (since := "2024-06-23")] protected abbrev UInt32.div_toNat := @UInt32.toNat_div +@[deprecated UInt32.toNat_mod (since := "2024-06-23")] protected abbrev UInt32.mod_toNat := @UInt32.toNat_mod -@[deprecated (since := "2024-06-23")] protected abbrev UInt64.zero_toNat := @UInt64.toNat_zero -@[deprecated (since := "2024-06-23")] protected abbrev UInt64.div_toNat := @UInt64.toNat_div -@[deprecated (since := "2024-06-23")] protected abbrev UInt64.mod_toNat := @UInt64.toNat_mod +@[deprecated UInt64.toNat_zero (since := "2024-06-23")] protected abbrev UInt64.zero_toNat := @UInt64.toNat_zero +@[deprecated UInt64.toNat_div (since := "2024-06-23")] protected abbrev UInt64.div_toNat := @UInt64.toNat_div +@[deprecated UInt64.toNat_mod (since := "2024-06-23")] protected abbrev UInt64.mod_toNat := @UInt64.toNat_mod -@[deprecated (since := "2024-06-23")] protected abbrev USize.zero_toNat := @USize.toNat_zero -@[deprecated (since := "2024-06-23")] protected abbrev USize.div_toNat := @USize.toNat_div -@[deprecated (since := "2024-06-23")] protected abbrev USize.mod_toNat := @USize.toNat_mod +@[deprecated USize.toNat_zero (since := "2024-06-23")] protected abbrev USize.zero_toNat := @USize.toNat_zero +@[deprecated USize.toNat_div (since := "2024-06-23")] protected abbrev USize.div_toNat := @USize.toNat_div +@[deprecated USize.toNat_mod (since := "2024-06-23")] protected abbrev USize.mod_toNat := @USize.toNat_mod diff --git a/src/Init/GetElem.lean b/src/Init/GetElem.lean index 8cd9e17d61..3a4b1adfcc 100644 --- a/src/Init/GetElem.lean +++ b/src/Init/GetElem.lean @@ -206,12 +206,12 @@ instance : GetElem (List α) Nat α fun as i => i < as.length where @[simp] theorem getElem_cons_zero (a : α) (as : List α) (h : 0 < (a :: as).length) : getElem (a :: as) 0 h = a := by rfl -@[deprecated (since := "2024-06-12")] abbrev cons_getElem_zero := @getElem_cons_zero +@[deprecated getElem_cons_zero (since := "2024-06-12")] abbrev cons_getElem_zero := @getElem_cons_zero @[simp] theorem getElem_cons_succ (a : α) (as : List α) (i : Nat) (h : i + 1 < (a :: as).length) : getElem (a :: as) (i+1) h = getElem as i (Nat.lt_of_succ_lt_succ h) := by rfl -@[deprecated (since := "2024-06-12")] abbrev cons_getElem_succ := @getElem_cons_succ +@[deprecated getElem_cons_succ (since := "2024-06-12")] abbrev cons_getElem_succ := @getElem_cons_succ @[simp] theorem getElem_mem : ∀ {l : List α} {n} (h : n < l.length), l[n]'h ∈ l | _ :: _, 0, _ => .head .. @@ -223,7 +223,8 @@ theorem getElem_cons_drop_succ_eq_drop {as : List α} {i : Nat} (h : i < as.leng | _::_, 0 => rfl | _::_, i+1 => getElem_cons_drop_succ_eq_drop (i := i) _ -@[deprecated (since := "2024-11-05")] abbrev get_drop_eq_drop := @getElem_cons_drop_succ_eq_drop +@[deprecated getElem_cons_drop_succ_eq_drop (since := "2024-11-05")] +abbrev get_drop_eq_drop := @getElem_cons_drop_succ_eq_drop end List diff --git a/src/Lean/Linter/Deprecated.lean b/src/Lean/Linter/Deprecated.lean index 0e64288885..ff248cc620 100644 --- a/src/Lean/Linter/Deprecated.lean +++ b/src/Lean/Linter/Deprecated.lean @@ -31,6 +31,10 @@ builtin_initialize deprecatedAttr : ParametricAttribute DeprecationEntry ← let newName? ← id?.mapM Elab.realizeGlobalConstNoOverloadWithInfo let text? := text?.map TSyntax.getString let since? := since?.map TSyntax.getString + if id?.isNone && text?.isNone then + logWarning "`[deprecated]` attribute should specify either a new name or a deprecation message" + if since?.isNone then + logWarning "`[deprecated]` attribute should specify the date or library version at which the deprecation was introduced, using `(since := \"...\")`" return { newName?, text?, since? } } @@ -46,7 +50,9 @@ def getDeprecatedNewName (env : Environment) (declName : Name) : Option Name := def checkDeprecated [Monad m] [MonadEnv m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (declName : Name) : m Unit := do if getLinterValue linter.deprecated (← getOptions) then let some attr := deprecatedAttr.getParam? (← getEnv) declName | pure () - logWarning <| .tagged ``deprecatedAttr <| attr.text?.getD <| - match attr.newName? with - | none => s!"`{declName}` has been deprecated" - | some newName => s!"`{declName}` has been deprecated, use `{newName}` instead" + logWarning <| .tagged ``deprecatedAttr <| + s!"`{declName}` has been deprecated" ++ match attr.text? with + | some text => s!": {text}" + | none => match attr.newName? with + | some newName => s!": use `{newName}` instead" + | none => "" diff --git a/src/lake/Lake/Build/Basic.lean b/src/lake/Lake/Build/Basic.lean index cabed7f250..446264f8aa 100644 --- a/src/lake/Lake/Build/Basic.lean +++ b/src/lake/Lake/Build/Basic.lean @@ -120,5 +120,6 @@ Logs a build step with `message`. As a result, this no longer functions the way it used to. It now just logs the `message` via `logVerbose`. -/ -@[deprecated (since := "2024-05-25"), inline] def logStep [Monad m] [MonadLog m] (message : String) : m Unit := do +@[deprecated "See doc-string for deprecation information." (since := "2024-05-25"), inline] +def logStep [Monad m] [MonadLog m] (message : String) : m Unit := do logVerbose message diff --git a/src/lake/Lake/Build/Facets.lean b/src/lake/Lake/Build/Facets.lean index 8818caa0b0..bf9bb43eb8 100644 --- a/src/lake/Lake/Build/Facets.lean +++ b/src/lake/Lake/Build/Facets.lean @@ -152,7 +152,7 @@ Will NOT cause the whole build to fail if the release cannot be fetched. abbrev Package.optGitHubReleaseFacet := `optRelease package_data optRelease : BuildJob Bool -@[deprecated (since := "2024-09-27")] +@[deprecated optGitHubReleaseFacet (since := "2024-09-27")] abbrev Package.optReleaseFacet := optGitHubReleaseFacet /-- @@ -162,7 +162,7 @@ Will cause the whole build to fail if the release cannot be fetched. abbrev Package.gitHubReleaseFacet := `release package_data release : BuildJob Unit -@[deprecated (since := "2024-09-27")] +@[deprecated gitHubReleaseFacet (since := "2024-09-27")] abbrev Package.releaseFacet := gitHubReleaseFacet /-- A package's `extraDepTargets` mixed with its transitive dependencies'. -/ diff --git a/src/lake/Lake/Build/Info.lean b/src/lake/Lake/Build/Info.lean index 86d16e8c1e..405f197632 100644 --- a/src/lake/Lake/Build/Info.lean +++ b/src/lake/Lake/Build/Info.lean @@ -241,10 +241,10 @@ abbrev Package.gitHubRelease (self : Package) : BuildInfo := abbrev Package.optGitHubRelease (self : Package) : BuildInfo := self.facet optGitHubReleaseFacet -@[deprecated (since := "2024-09-27")] +@[deprecated gitHubRelease (since := "2024-09-27")] abbrev Package.release := @gitHubRelease -@[deprecated (since := "2024-09-27")] +@[deprecated optGitHubRelease (since := "2024-09-27")] abbrev Package.optRelease := @optGitHubRelease @[inherit_doc extraDepFacet] diff --git a/src/lake/Lake/Build/Package.lean b/src/lake/Lake/Build/Package.lean index 08e74c1a6d..66cb6ae307 100644 --- a/src/lake/Lake/Build/Package.lean +++ b/src/lake/Lake/Build/Package.lean @@ -185,14 +185,14 @@ def Package.barrelFacetConfig : PackageFacetConfig reservoirBarrelFacet := def Package.optGitHubReleaseFacetConfig : PackageFacetConfig optGitHubReleaseFacet := mkOptBuildArchiveFacetConfig buildArchiveFile getReleaseUrl -@[deprecated (since := "2024-09-27")] +@[deprecated optGitHubReleaseFacetConfig (since := "2024-09-27")] abbrev Package.optReleaseFacetConfig := optGitHubReleaseFacetConfig /-- The `PackageFacetConfig` for the builtin `gitHubReleaseFacet`. -/ def Package.gitHubReleaseFacetConfig : PackageFacetConfig gitHubReleaseFacet := mkBuildArchiveFacetConfig optGitHubReleaseFacet "GitHub release" -@[deprecated (since := "2024-09-27")] +@[deprecated gitHubReleaseFacetConfig (since := "2024-09-27")] abbrev Package.releaseFacetConfig := gitHubReleaseFacetConfig /-- diff --git a/src/lake/Lake/Build/Trace.lean b/src/lake/Lake/Build/Trace.lean index 9a198679a6..2552f6e3e2 100644 --- a/src/lake/Lake/Build/Trace.lean +++ b/src/lake/Lake/Build/Trace.lean @@ -305,7 +305,9 @@ If not, check if the info is newer than this trace's modification time. **Deprecated:** Should not be done manually, but as part of `buildUnlessUpToDate`. -/ -@[deprecated (since := "2024-06-14"), specialize] def checkAgainstFile +@[deprecated "Should not be done manually, but as part of `buildUnlessUpToDate`." + (since := "2024-06-14"), specialize] +def checkAgainstFile [CheckExists i] [GetMTime i] (info : i) (traceFile : FilePath) (self : BuildTrace) : BaseIO Bool := do @@ -320,7 +322,8 @@ Write trace to a file. **Deprecated:** Should not be done manually, but as part of `buildUnlessUpToDate`. -/ -@[deprecated (since := "2024-06-14")] def writeToFile (traceFile : FilePath) (self : BuildTrace) : IO PUnit := do +@[deprecated "Should not be done manually, but as part of `buildUnlessUpToDate`." (since := "2024-06-14")] +def writeToFile (traceFile : FilePath) (self : BuildTrace) : IO PUnit := do createParentDirs traceFile IO.FS.writeFile traceFile self.hash.toString diff --git a/src/lake/Lake/Util/Log.lean b/src/lake/Lake/Util/Log.lean index 2abf76ac54..cc8a5fcd11 100644 --- a/src/lake/Lake/Util/Log.lean +++ b/src/lake/Lake/Util/Log.lean @@ -161,7 +161,8 @@ export MonadLog (logEntry) message := mkErrorStringWithPos msg.fileName msg.pos str none } -@[deprecated (since := "2024-05-18")] def logToIO (e : LogEntry) (minLv : LogLevel) : BaseIO PUnit := do +@[deprecated "No deprecation message available." (since := "2024-05-18")] +def logToIO (e : LogEntry) (minLv : LogLevel) : BaseIO PUnit := do match e.level with | .trace => if minLv ≥ .trace then IO.println e.message.trim |>.catchExceptions fun _ => pure () @@ -189,7 +190,8 @@ abbrev lift [MonadLiftT m n] (self : MonadLog m) : MonadLog n where instance [MonadLift m n] [methods : MonadLog m] : MonadLog n := methods.lift set_option linter.deprecated false in -@[deprecated (since := "2024-05-18")] abbrev io [MonadLiftT BaseIO m] (minLv := LogLevel.info) : MonadLog m where +@[deprecated "Deprecated without replacement." (since := "2024-05-18")] +abbrev io [MonadLiftT BaseIO m] (minLv := LogLevel.info) : MonadLog m where logEntry e := logToIO e minLv abbrev stream [MonadLiftT BaseIO m] diff --git a/tests/lean/4452.lean b/tests/lean/4452.lean index 4e7191a822..b2c4986e4a 100644 --- a/tests/lean/4452.lean +++ b/tests/lean/4452.lean @@ -1,6 +1,6 @@ def a := 1 -@[deprecated] +@[deprecated "Don't use `hi`." (since := "1970-01-01")] theorem hi : a = 1 := rfl attribute [simp] hi @@ -19,7 +19,7 @@ example (h : 1 = b) : a = b := by guard_target =ₛ 1 = b exact h -@[deprecated] +@[deprecated "Don't use `hi'`, either." (since := "1970-01-01")] theorem hi' : True := .intro example : True := by diff --git a/tests/lean/4452.lean.expected.out b/tests/lean/4452.lean.expected.out index b23f7d3f53..8e50ea96d1 100644 --- a/tests/lean/4452.lean.expected.out +++ b/tests/lean/4452.lean.expected.out @@ -1,2 +1,2 @@ -4452.lean:17:4-17:6: warning: `hi` has been deprecated -4452.lean:28:4-28:7: warning: `hi'` has been deprecated +4452.lean:17:4-17:6: warning: `hi` has been deprecated: Don't use `hi`. +4452.lean:28:4-28:7: warning: `hi'` has been deprecated: Don't use `hi'`, either. diff --git a/tests/lean/deprecated.lean.expected.out b/tests/lean/deprecated.lean.expected.out index f778143a2d..277e66a18c 100644 --- a/tests/lean/deprecated.lean.expected.out +++ b/tests/lean/deprecated.lean.expected.out @@ -1,11 +1,17 @@ -deprecated.lean:11:6-11:7: warning: `f` has been deprecated, use `g` instead +deprecated.lean:5:2-5:14: warning: `[deprecated]` attribute should specify the date or library version at which the deprecation was introduced, using `(since := "...")` +deprecated.lean:8:2-8:12: warning: `[deprecated]` attribute should specify either a new name or a deprecation message +deprecated.lean:8:2-8:12: warning: `[deprecated]` attribute should specify the date or library version at which the deprecation was introduced, using `(since := "...")` +deprecated.lean:11:6-11:7: warning: `f` has been deprecated: use `g` instead 2 deprecated.lean:13:6-13:7: warning: `h` has been deprecated 1 deprecated.lean:15:13-15:15: error: unknown constant 'g1' deprecated.lean:23:13-23:15: error: unknown constant 'g1' -deprecated.lean:30:6-30:8: warning: `f2` has been deprecated, use `Foo.g1` instead +deprecated.lean:27:2-27:55: warning: `[deprecated]` attribute should specify the date or library version at which the deprecation was introduced, using `(since := "...")` +deprecated.lean:30:6-30:8: warning: `f2` has been deprecated: use `Foo.g1` instead 2 2 -deprecated.lean:33:6-33:8: warning: use g1 instead, f4 is not a good name +deprecated.lean:33:6-33:8: warning: `f4` has been deprecated: use g1 instead, f4 is not a good name 2 +deprecated.lean:35:2-35:12: warning: `[deprecated]` attribute should specify either a new name or a deprecation message +deprecated.lean:35:2-35:12: warning: `[deprecated]` attribute should specify the date or library version at which the deprecation was introduced, using `(since := "...")` diff --git a/tests/lean/warningAsError.lean b/tests/lean/warningAsError.lean index 7768da79d2..85e54dd92e 100644 --- a/tests/lean/warningAsError.lean +++ b/tests/lean/warningAsError.lean @@ -2,7 +2,7 @@ set_option linter.deprecated true def f (x : Nat) := x + 1 -@[deprecated f] +@[deprecated f (since := "1970-01-01")] def g (x : Nat) := x + 1 #eval g 0 -- warning diff --git a/tests/lean/warningAsError.lean.expected.out b/tests/lean/warningAsError.lean.expected.out index 97388297b4..b0c11f8f11 100644 --- a/tests/lean/warningAsError.lean.expected.out +++ b/tests/lean/warningAsError.lean.expected.out @@ -1,6 +1,6 @@ -warningAsError.lean:8:6-8:7: warning: `g` has been deprecated, use `f` instead +warningAsError.lean:8:6-8:7: warning: `g` has been deprecated: use `f` instead 1 -warningAsError.lean:12:6-12:7: error: `g` has been deprecated, use `f` instead +warningAsError.lean:12:6-12:7: error: `g` has been deprecated: use `f` instead 1 warningAsError.lean:15:7-15:13: error: unused variable `unused` note: this linter can be disabled with `set_option linter.unusedVariables false`