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.
This commit is contained in:
Kim Morrison
GitHub
parent
9a17919ef1
commit
f70b7e5722
19 changed files with 77 additions and 56 deletions
|
|
@ -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)
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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)) :
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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]
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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 => ""
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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'. -/
|
||||
|
|
|
|||
|
|
@ -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]
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
/--
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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]
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -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 := "...")`
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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`
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue