From 554e7234330cf06efffe0cb52092e783a27561cc Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 2 Jul 2024 14:30:09 +1000 Subject: [PATCH] chore: add 'since' dates to deprecated (#4617) --- src/Init/Data/Option/Basic.lean | 2 +- src/Init/GetElem.lean | 4 ++-- src/Lean/Message.lean | 2 +- src/Lean/Meta/Tactic/Replace.lean | 2 +- src/lake/Lake/Build/Basic.lean | 2 +- src/lake/Lake/Build/Common.lean | 2 +- src/lake/Lake/Build/Fetch.lean | 4 ++-- src/lake/Lake/Build/Job.lean | 2 +- src/lake/Lake/Build/Trace.lean | 4 ++-- src/lake/Lake/Util/Log.lean | 8 ++++---- 10 files changed, 16 insertions(+), 16 deletions(-) diff --git a/src/Init/Data/Option/Basic.lean b/src/Init/Data/Option/Basic.lean index 4ea1f190a2..eeba715f32 100644 --- a/src/Init/Data/Option/Basic.lean +++ b/src/Init/Data/Option/Basic.lean @@ -26,7 +26,7 @@ def toMonad [Monad m] [Alternative m] : Option α → m α := getM | some _ => true | none => false -@[deprecated isSome, inline] def toBool : Option α → Bool := isSome +@[deprecated isSome (since := "2024-04-17"), inline] def toBool : Option α → Bool := isSome /-- Returns `true` on `none` and `false` on `some x`. -/ @[inline] def isNone : Option α → Bool diff --git a/src/Init/GetElem.lean b/src/Init/GetElem.lean index 9c2c1556e0..5cd8140f6b 100644 --- a/src/Init/GetElem.lean +++ b/src/Init/GetElem.lean @@ -194,12 +194,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-6-12")] abbrev cons_getElem_zero := @getElem_cons_zero +@[deprecated (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-6-12")] abbrev cons_getElem_succ := @getElem_cons_succ +@[deprecated (since := "2024-06-12")] abbrev cons_getElem_succ := @getElem_cons_succ theorem get_drop_eq_drop (as : List α) (i : Nat) (h : i < as.length) : as[i] :: as.drop (i+1) = as.drop i := match as, i with diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index 379c6911f9..9cb2aecc34 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -365,7 +365,7 @@ namespace MessageLog def empty : MessageLog := {} @[deprecated "renamed to `unreported`; direct access should in general be avoided in favor of \ -using `MessageLog.toList/toArray`"] +using `MessageLog.toList/toArray`" (since := "2024-05-22")] def msgs : MessageLog → PersistentArray Message := unreported def hasUnreported (log : MessageLog) : Bool := diff --git a/src/Lean/Meta/Tactic/Replace.lean b/src/Lean/Meta/Tactic/Replace.lean index 5599ab2511..be9c73fad4 100644 --- a/src/Lean/Meta/Tactic/Replace.lean +++ b/src/Lean/Meta/Tactic/Replace.lean @@ -190,7 +190,7 @@ def _root_.Lean.MVarId.changeLocalDecl (mvarId : MVarId) (fvarId : FVarId) (type | _ => throwTacticEx `changeLocalDecl mvarId "unexpected auxiliary target" return mvarId -@[deprecated MVarId.changeLocalDecl] +@[deprecated MVarId.changeLocalDecl (since := "2022-07-15")] def changeLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) (checkDefEq := true) : MetaM MVarId := do mvarId.changeLocalDecl fvarId typeNew checkDefEq diff --git a/src/lake/Lake/Build/Basic.lean b/src/lake/Lake/Build/Basic.lean index ec257525d5..183b897a43 100644 --- a/src/lake/Lake/Build/Basic.lean +++ b/src/lake/Lake/Build/Basic.lean @@ -103,5 +103,5 @@ 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, inline] def logStep [Monad m] [MonadLog m] (message : String) : m Unit := do +@[deprecated (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/Common.lean b/src/lake/Lake/Build/Common.lean index a03f4b2f8e..e5d723cf07 100644 --- a/src/lake/Lake/Build/Common.lean +++ b/src/lake/Lake/Build/Common.lean @@ -250,7 +250,7 @@ A build job for file that is expected to already exist. **Deprecated:** Use either `inputTextFile` or `inputBinFile`. `inputTextFile` normalizes line endings to produce platform-independent traces. -/ -@[deprecated] abbrev inputFile := @inputBinFile +@[deprecated (since := "2024-06-08")] abbrev inputFile := @inputBinFile /-- Build an object file from a source file job using `compiler`. The invocation is: diff --git a/src/lake/Lake/Build/Fetch.lean b/src/lake/Lake/Build/Fetch.lean index 8b6ea6d268..8bf894d56c 100644 --- a/src/lake/Lake/Build/Fetch.lean +++ b/src/lake/Lake/Build/Fetch.lean @@ -75,10 +75,10 @@ example : MonadLiftT JobM FetchM := inferInstance example : MonadLiftT SpawnM FetchM := inferInstance /-- The top-level monad for Lake build functions. **Renamed `FetchM`.** -/ -@[deprecated FetchM] abbrev IndexBuildM := FetchM +@[deprecated FetchM (since := "2024-04-30")] abbrev IndexBuildM := FetchM /-- The old build monad. **Uses should generally be replaced by `FetchM`.** -/ -@[deprecated FetchM] abbrev BuildM := BuildT LogIO +@[deprecated FetchM (since := "2024-04-30")] abbrev BuildM := BuildT LogIO /-- Fetch the result associated with the info using the Lake build index. -/ @[inline] def BuildInfo.fetch (self : BuildInfo) [FamilyOut BuildData self.key α] : FetchM α := diff --git a/src/lake/Lake/Build/Job.lean b/src/lake/Lake/Build/Job.lean index dea138ce97..7418c46175 100644 --- a/src/lake/Lake/Build/Job.lean +++ b/src/lake/Lake/Build/Job.lean @@ -98,7 +98,7 @@ instance : MonadLift LogIO JobM := ⟨ELogT.takeAndRun⟩ abbrev SpawnM := BuildT BaseIO /-- The monad used to spawn asynchronous Lake build jobs. **Replaced by `SpawnM`.** -/ -@[deprecated SpawnM] abbrev SchedulerM := SpawnM +@[deprecated SpawnM (since := "2024-05-21")] abbrev SchedulerM := SpawnM /-- A Lake job. -/ structure Job (α : Type u) where diff --git a/src/lake/Lake/Build/Trace.lean b/src/lake/Lake/Build/Trace.lean index 87e2cfe409..a8323e9616 100644 --- a/src/lake/Lake/Build/Trace.lean +++ b/src/lake/Lake/Build/Trace.lean @@ -277,7 +277,7 @@ 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, specialize] def checkAgainstFile +@[deprecated (since := "2024-06-14"), specialize] def checkAgainstFile [CheckExists i] [GetMTime i] (info : i) (traceFile : FilePath) (self : BuildTrace) : BaseIO Bool := do @@ -292,7 +292,7 @@ Write trace to a file. **Deprecated:** Should not be done manually, but as part of `buildUnlessUpToDate`. -/ -@[deprecated] def writeToFile (traceFile : FilePath) (self : BuildTrace) : IO PUnit := do +@[deprecated (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 68602af8a4..b6185e1b45 100644 --- a/src/lake/Lake/Util/Log.lean +++ b/src/lake/Lake/Util/Log.lean @@ -147,7 +147,7 @@ export MonadLog (logEntry) message := mkErrorStringWithPos msg.fileName msg.pos str none } -@[deprecated] def logToIO (e : LogEntry) (minLv : LogLevel) : BaseIO PUnit := do +@[deprecated (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 () @@ -175,7 +175,7 @@ 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] abbrev io [MonadLiftT BaseIO m] (minLv := LogLevel.info) : MonadLog m where +@[deprecated (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] @@ -486,7 +486,7 @@ abbrev run?' [Functor m] (self : ELogT m α) (log : Log := {}) : m (Option α) : @[inline] def catchLog [Monad m] (f : Log → LogT m α) (self : ELogT m α) : LogT m α := do self.catchExceptions fun errPos => do f (← takeLogFrom errPos) -@[deprecated run?] abbrev captureLog := @run? +@[deprecated run? (since := "2024-05-18")] abbrev captureLog := @run? /-- Run `self` with the log taken from the state of the monad `n`, @@ -532,7 +532,7 @@ instance : MonadLift IO LogIO := ⟨MonadError.runIO⟩ namespace LogIO -@[deprecated ELogT.run?] abbrev captureLog := @ELogT.run? +@[deprecated ELogT.run? (since := "2024-05-18")] abbrev captureLog := @ELogT.run? /-- Runs a `LogIO` action in `BaseIO`.