From e2b30dce0e92d4fd12de8dec3e8194c36b4ed36b Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 14 Nov 2024 10:21:05 +1100 Subject: [PATCH] chore: remove >6 month old deprecations (#1044) --- Batteries.lean | 2 -- Batteries/Data/Array/Merge.lean | 17 --------- Batteries/Data/List/Basic.lean | 4 --- Batteries/Data/List/Lemmas.lean | 3 -- Batteries/Data/RBMap/Basic.lean | 9 ----- Batteries/Lean/Delaborator.lean | 13 ------- Batteries/Lean/HashSet.lean | 3 -- Batteries/Logic.lean | 2 -- Batteries/StdDeprecations.lean | 63 --------------------------------- 9 files changed, 116 deletions(-) delete mode 100644 Batteries/Lean/Delaborator.lean delete mode 100644 Batteries/StdDeprecations.lean diff --git a/Batteries.lean b/Batteries.lean index e6464503cb..b645334bf4 100644 --- a/Batteries.lean +++ b/Batteries.lean @@ -37,7 +37,6 @@ import Batteries.Data.UInt import Batteries.Data.UnionFind import Batteries.Data.Vector import Batteries.Lean.AttributeExtra -import Batteries.Lean.Delaborator import Batteries.Lean.EStateM import Batteries.Lean.Except import Batteries.Lean.Expr @@ -70,7 +69,6 @@ import Batteries.Linter import Batteries.Linter.UnnecessarySeqFocus import Batteries.Linter.UnreachableTactic import Batteries.Logic -import Batteries.StdDeprecations import Batteries.Tactic.Alias import Batteries.Tactic.Basic import Batteries.Tactic.Case diff --git a/Batteries/Data/Array/Merge.lean b/Batteries/Data/Array/Merge.lean index 4b806a35d6..70034111ad 100644 --- a/Batteries/Data/Array/Merge.lean +++ b/Batteries/Data/Array/Merge.lean @@ -26,11 +26,6 @@ where if lt x y then go (acc.push x) (i + 1) j else go (acc.push y) i (j + 1) termination_by xs.size + ys.size - (i + j) -set_option linter.unusedVariables false in -@[deprecated merge (since := "2024-04-24"), inherit_doc merge] -def mergeSortedPreservingDuplicates [ord : Ord α] (xs ys : Array α) : Array α := - merge (compare · · |>.isLT) xs ys - -- We name `ord` so it can be provided as a named argument. set_option linter.unusedVariables.funArgs false in /-- @@ -57,8 +52,6 @@ where | .eq => go (acc.push (merge x y)) (i + 1) (j + 1) termination_by xs.size + ys.size - (i + j) -@[deprecated (since := "2024-04-24")] alias mergeSortedMergingDuplicates := mergeDedupWith - /-- `O(|xs| + |ys|)`. Merge arrays `xs` and `ys`, which must be sorted according to `compare` and must not contain duplicates. If an element appears in both `xs` and `ys`, only one copy is kept. @@ -66,8 +59,6 @@ not contain duplicates. If an element appears in both `xs` and `ys`, only one co @[inline] def mergeDedup [ord : Ord α] (xs ys : Array α) : Array α := mergeDedupWith (ord := ord) xs ys fun x _ => x -@[deprecated (since := "2024-04-24")] alias mergeSortedDeduplicating := mergeDedup - set_option linter.unusedVariables false in /-- `O(|xs| * |ys|)`. Merge `xs` and `ys`, which do not need to be sorted. Elements which occur in @@ -85,8 +76,6 @@ where ys.foldl (init := xs) fun xs y => if xs.any (· == y) (stop := xsSize) then xs else xs.push y -@[deprecated (since := "2024-04-24")] alias mergeUnsortedDeduplicating := mergeUnsortedDedup - -- We name `eq` so it can be provided as a named argument. set_option linter.unusedVariables.funArgs false in /-- @@ -105,8 +94,6 @@ where acc.push hd termination_by xs.size - i -@[deprecated (since := "2024-04-24")] alias mergeAdjacentDuplicates := mergeAdjacentDups - /-- `O(|xs|)`. Deduplicate a sorted array. The array must be sorted with to an order which agrees with `==`, i.e. whenever `x == y` then `compare x y == .eq`. @@ -114,13 +101,9 @@ where def dedupSorted [eq : BEq α] (xs : Array α) : Array α := xs.mergeAdjacentDups (eq := eq) fun x _ => x -@[deprecated (since := "2024-04-24")] alias deduplicateSorted := dedupSorted - /-- `O(|xs| log |xs|)`. Sort and deduplicate an array. -/ def sortDedup [ord : Ord α] (xs : Array α) : Array α := have := ord.toBEq dedupSorted <| xs.qsort (compare · · |>.isLT) -@[deprecated (since := "2024-04-24")] alias sortAndDeduplicate := sortDedup - end Array diff --git a/Batteries/Data/List/Basic.lean b/Batteries/Data/List/Basic.lean index 3e2460f18c..9c0ab14d46 100644 --- a/Batteries/Data/List/Basic.lean +++ b/Batteries/Data/List/Basic.lean @@ -53,10 +53,6 @@ drop_while (· != 1) [0, 1, 2, 3] = [1, 2, 3] | [] => [] | x :: xs => bif p x then xs else after p xs -@[deprecated (since := "2024-05-06")] alias removeNth := eraseIdx -@[deprecated (since := "2024-05-06")] alias removeNthTR := eraseIdxTR -@[deprecated (since := "2024-05-06")] alias removeNth_eq_removeNthTR := eraseIdx_eq_eraseIdxTR - /-- Replaces the first element of the list for which `f` returns `some` with the returned value. -/ @[simp] def replaceF (f : α → Option α) : List α → List α | [] => [] diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean index 89f1de368d..c8fba52299 100644 --- a/Batteries/Data/List/Lemmas.lean +++ b/Batteries/Data/List/Lemmas.lean @@ -524,7 +524,6 @@ theorem get?_inj @[deprecated (since := "2024-10-21")] alias modifyNth_succ_cons := modify_succ_cons @[deprecated (since := "2024-10-21")] alias modifyNthTail_id := modifyTailIdx_id @[deprecated (since := "2024-10-21")] alias eraseIdx_eq_modifyNthTail := eraseIdx_eq_modifyTailIdx -@[deprecated (since := "2024-05-06")] alias removeNth_eq_nth_tail := eraseIdx_eq_modifyTailIdx @[deprecated (since := "2024-10-21")] alias getElem?_modifyNth := getElem?_modify @[deprecated getElem?_modify (since := "2024-06-12")] theorem get?_modifyNth (f : α → α) (n) (l : List α) (m) : @@ -574,5 +573,3 @@ theorem get?_set_ne (a : α) {m n} (l : List α) (h : m ≠ n) : (set l m a).get theorem get?_set (a : α) {m n} (l : List α) : (set l m a).get? n = if m = n then (fun _ => a) <$> l.get? n else l.get? n := by simp [getElem?_set']; rfl -@[deprecated (since := "2024-05-06")] alias length_removeNth := length_eraseIdx -@[deprecated (since := "2024-04-22")] alias sublist.erase := Sublist.erase diff --git a/Batteries/Data/RBMap/Basic.lean b/Batteries/Data/RBMap/Basic.lean index 8eb202591c..e2c9a32c5f 100644 --- a/Batteries/Data/RBMap/Basic.lean +++ b/Batteries/Data/RBMap/Basic.lean @@ -67,9 +67,6 @@ protected def max? : RBNode α → Option α | node _ _ v nil => some v | node _ _ _ r => r.max? -@[deprecated (since := "2024-04-17")] protected alias min := RBNode.min? -@[deprecated (since := "2024-04-17")] protected alias max := RBNode.max? - /-- Fold a function in tree order along the nodes. `v₀` is used at `nil` nodes and `f` is used to combine results at branching nodes. @@ -670,9 +667,6 @@ instance : ToStream (RBSet α cmp) (RBNode.Stream α) := ⟨fun x => x.1.toStrea /-- `O(log n)`. Returns the entry `a` such that `a ≥ k` for all keys in the RBSet. -/ @[inline] protected def max? (t : RBSet α cmp) : Option α := t.1.max? -@[deprecated (since := "2024-04-17")] protected alias min := RBSet.min? -@[deprecated (since := "2024-04-17")] protected alias max := RBSet.max? - instance [Repr α] : Repr (RBSet α cmp) where reprPrec m prec := Repr.addAppParen ("RBSet.ofList " ++ repr m.toList) prec @@ -1055,9 +1049,6 @@ instance : Stream (Values.Stream α β) β := ⟨Values.Stream.next?⟩ /-- `O(log n)`. Returns the key-value pair `(a, b)` such that `a ≥ k` for all keys in the RBMap. -/ @[inline] protected def max? : RBMap α β cmp → Option (α × β) := RBSet.max? -@[deprecated (since := "2024-04-17")] protected alias min := RBMap.min? -@[deprecated (since := "2024-04-17")] protected alias max := RBMap.max? - instance [Repr α] [Repr β] : Repr (RBMap α β cmp) where reprPrec m prec := Repr.addAppParen ("RBMap.ofList " ++ repr m.toList) prec diff --git a/Batteries/Lean/Delaborator.lean b/Batteries/Lean/Delaborator.lean deleted file mode 100644 index e09f2198de..0000000000 --- a/Batteries/Lean/Delaborator.lean +++ /dev/null @@ -1,13 +0,0 @@ -/- -Copyright (c) 2022 Mario Carneiro. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Mario Carneiro, Kyle Miller --/ -import Lean.PrettyPrinter - -open Lean PrettyPrinter Delaborator SubExpr - -/-- Abbreviation for `Lean.MessageData.ofConst`. -/ -@[deprecated Lean.MessageData.ofConst (since := "2024-05-18")] -def Lean.ppConst (e : Expr) : MessageData := - Lean.MessageData.ofConst e diff --git a/Batteries/Lean/HashSet.lean b/Batteries/Lean/HashSet.lean index 2a6ee47909..d0afac657b 100644 --- a/Batteries/Lean/HashSet.lean +++ b/Batteries/Lean/HashSet.lean @@ -10,9 +10,6 @@ namespace Std.HashSet variable [BEq α] [Hashable α] -instance : Singleton α (HashSet α) := ⟨fun x => HashSet.empty.insert x⟩ -instance : Insert α (HashSet α) := ⟨fun a s => s.insert a⟩ - /-- `O(n)`. Returns `true` if `f` returns `true` for any element of the set. -/ diff --git a/Batteries/Logic.lean b/Batteries/Logic.lean index 4bc5f9f102..0be01f3b28 100644 --- a/Batteries/Logic.lean +++ b/Batteries/Logic.lean @@ -8,8 +8,6 @@ import Batteries.Tactic.Alias instance {f : α → β} [DecidablePred p] : DecidablePred (p ∘ f) := inferInstanceAs <| DecidablePred fun x => p (f x) -@[deprecated (since := "2024-03-15")] alias proofIrrel := proof_irrel - /-! ## id -/ theorem Function.id_def : @id α = fun x => x := rfl diff --git a/Batteries/StdDeprecations.lean b/Batteries/StdDeprecations.lean deleted file mode 100644 index 74a00f4f5a..0000000000 --- a/Batteries/StdDeprecations.lean +++ /dev/null @@ -1,63 +0,0 @@ -/- -Copyright (c) 2024 Kim Morrison. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Kim Morrison --/ -import Batteries.Tactic.Alias -import Batteries.Data.DList.Basic -import Batteries.Data.PairingHeap -import Batteries.Data.BinomialHeap.Basic -import Batteries.Data.HashMap.Basic -import Batteries.Data.RBMap.Basic -import Batteries.Data.UnionFind.Basic - -/-! -# We set up deprecations for identifiers formerly in the `Std` namespace. - -Note that we have not moved anything in the `Std.CodeAction` or `Std.Linter` namespace. - -These deprecations do not cover `Std.Tactic`, the contents of which has been moved, -but it would be much harder to generate the deprecations. -Let's hope that people using the tactic implementations can work this out themselves. --/ - -@[deprecated (since := "2024-05-07")] alias Std.AssocList := Batteries.AssocList -@[deprecated (since := "2024-05-07")] alias Std.mkHashMap := Batteries.mkHashMap -@[deprecated (since := "2024-05-07")] alias Std.DList := Batteries.DList -@[deprecated (since := "2024-05-07")] alias Std.PairingHeapImp.Heap := Batteries.PairingHeapImp.Heap -@[deprecated (since := "2024-05-07")] alias Std.TotalBLE := Batteries.TotalBLE -@[deprecated (since := "2024-05-07")] alias Std.OrientedCmp := Batteries.OrientedCmp -@[deprecated (since := "2024-05-07")] alias Std.TransCmp := Batteries.TransCmp -@[deprecated (since := "2024-05-07")] alias Std.BEqCmp := Batteries.BEqCmp -@[deprecated (since := "2024-05-07")] alias Std.LTCmp := Batteries.LTCmp -@[deprecated (since := "2024-05-07")] alias Std.LECmp := Batteries.LECmp -@[deprecated (since := "2024-05-07")] alias Std.LawfulCmp := Batteries.LawfulCmp -@[deprecated (since := "2024-05-07")] alias Std.OrientedOrd := Batteries.OrientedOrd -@[deprecated (since := "2024-05-07")] alias Std.TransOrd := Batteries.TransOrd -@[deprecated (since := "2024-05-07")] alias Std.BEqOrd := Batteries.BEqOrd -@[deprecated (since := "2024-05-07")] alias Std.LTOrd := Batteries.LTOrd -@[deprecated (since := "2024-05-07")] alias Std.LEOrd := Batteries.LEOrd -@[deprecated (since := "2024-05-07")] alias Std.LawfulOrd := Batteries.LawfulOrd -@[deprecated (since := "2024-05-07")] -alias Std.compareOfLessAndEq_eq_lt := Batteries.compareOfLessAndEq_eq_lt -@[deprecated (since := "2024-05-07")] alias Std.RBColor := Batteries.RBColor -@[deprecated (since := "2024-05-07")] alias Std.RBNode := Batteries.RBNode -@[deprecated (since := "2024-05-07")] alias Std.RBSet := Batteries.RBSet -@[deprecated (since := "2024-05-07")] alias Std.mkRBSet := Batteries.mkRBSet -@[deprecated (since := "2024-05-07")] alias Std.RBMap := Batteries.RBMap -@[deprecated (since := "2024-05-07")] alias Std.mkRBMap := Batteries.mkRBMap -@[deprecated (since := "2024-05-07")] alias Std.BinomialHeap := Batteries.BinomialHeap -@[deprecated (since := "2024-05-07")] alias Std.mkBinomialHeap := Batteries.mkBinomialHeap -@[deprecated (since := "2024-05-07")] alias Std.UFNode := Batteries.UFNode -@[deprecated (since := "2024-05-07")] alias Std.UnionFind := Batteries.UnionFind - --- Check that these generate usable deprecated hints --- when referring to names inside these namespaces. -set_option warningAsError true in -/-- -error: `Std.UnionFind` has been deprecated, use `Batteries.UnionFind` instead ---- -error: unknown constant 'Std.UnionFind.find' --/ -#guard_msgs in -#eval Std.UnionFind.find