chore: deprecate Lean.HashMap and Lean.HashSet (#4954)

This restores all of the imports of `Lean.Data.HashMap` and
`Lean.Data.HashSet` so that users actually see the deprecation warnings
instead of a "declaration not found" error.

src/Lean/Compiler/IR/EmitLLVM.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Siddharth Bhat
 -/
 prelude
+import Lean.Data.HashMap
 import Lean.Runtime
 import Lean.Compiler.NameMangling
 import Lean.Compiler.ExportAttr

src/Lean/Data/HashMap.lean

@@ -6,6 +6,8 @@ Author: Leonardo de Moura
 prelude
 import Init.Data.Nat.Power2
 import Lean.Data.AssocList
+import Std.Data.HashMap.Basic
+import Std.Data.HashMap.Raw
 namespace Lean
 
 def HashMapBucket (α : Type u) (β : Type v) :=
@@ -269,4 +271,11 @@ def ofListWith (l : List (α × β)) (f : β → β → β) : HashMap α β :=
         | none   => m.insert p.fst p.snd
         | some v => m.insert p.fst $ f v p.snd)
 
+attribute [deprecated Std.HashMap] HashMap
+attribute [deprecated Std.HashMap.Raw] HashMapImp
+attribute [deprecated Std.HashMap.Raw.empty] mkHashMapImp
+attribute [deprecated Std.HashMap.empty] mkHashMap
+attribute [deprecated Std.HashMap.empty] HashMap.empty
+attribute [deprecated Std.HashMap.ofList] HashMap.ofList
+
 end Lean.HashMap

src/Lean/Data/HashSet.lean

@@ -6,6 +6,8 @@ Author: Leonardo de Moura
 prelude
 import Init.Data.Nat.Power2
 import Init.Data.List.Control
+import Std.Data.HashSet.Basic
+import Std.Data.HashSet.Raw
 namespace Lean
 universe u v w
 
@@ -217,3 +219,9 @@ def insertMany [ForIn Id ρ α] (s : HashSet α) (as : ρ) : HashSet α := Id.ru
 def merge {α : Type u} [BEq α] [Hashable α] (s t : HashSet α) : HashSet α :=
   t.fold (init := s) fun s a => s.insert a
   -- We don't use `insertMany` here because it gives weird universes.
+
+attribute [deprecated Std.HashSet] HashSet
+attribute [deprecated Std.HashSet.Raw] HashSetImp
+attribute [deprecated Std.HashSet.Raw.empty] mkHashSetImp
+attribute [deprecated Std.HashSet.empty] mkHashSet
+attribute [deprecated Std.HashSet.empty] HashSet.empty

src/Lean/Data/NameMap.lean

@@ -5,6 +5,7 @@ Author: Leonardo de Moura
 -/
 prelude
 import Std.Data.HashSet.Basic
+import Lean.Data.HashSet
 import Lean.Data.RBMap
 import Lean.Data.RBTree
 import Lean.Data.SSet

src/Lean/Data/SMap.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Std.Data.HashMap.Basic
+import Lean.Data.HashMap
 import Lean.Data.PersistentHashMap
 universe u v w w'
 

src/Lean/Environment.lean

@@ -8,6 +8,7 @@ import Init.Control.StateRef
 import Init.Data.Array.BinSearch
 import Init.Data.Stream
 import Lean.ImportingFlag
+import Lean.Data.HashMap
 import Lean.Data.SMap
 import Lean.Declaration
 import Lean.LocalContext

src/Lean/Level.lean

@@ -5,6 +5,8 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.Array.QSort
+import Lean.Data.HashMap
+import Lean.Data.HashSet
 import Lean.Data.PersistentHashMap
 import Lean.Data.PersistentHashSet
 import Lean.Hygiene

src/Lean/Meta/Canonicalizer.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.Data.HashMap
 import Lean.Util.ShareCommon
 import Lean.Meta.Basic
 import Lean.Meta.FunInfo

src/Lean/Util/Diff.lean

@@ -5,6 +5,7 @@ Authors: David Thrane Christiansen
 -/
 prelude
 import Init.Data
+import Lean.Data.HashMap
 import Std.Data.HashMap.Basic
 import Init.Omega
 

src/Lean/Util/MonadCache.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Control.StateRef
+import Lean.Data.HashMap
 import Std.Data.HashMap.Basic
 
 namespace Lean

src/Lean/Util/PtrSet.lean

@@ -5,6 +5,8 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.Hashable
+import Lean.Data.HashSet
+import Lean.Data.HashMap
 import Std.Data.HashSet.Basic
 import Std.Data.HashMap.Basic
 

src/Lean/Util/SCC.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.List.Control
+import Lean.Data.HashMap
 import Std.Data.HashMap.Basic
 namespace Lean.SCC
 /-!

src/Lean/Util/ShareCommon.lean

@@ -13,6 +13,7 @@ import Lean.Data.PersistentHashSet
 open ShareCommon
 namespace Lean.ShareCommon
 
+set_option linter.deprecated false in
 def objectFactory :=
   StateFactory.mk {
     Map := HashMap, mkMap := (mkHashMap ·), mapFind? := (·.find?), mapInsert := (·.insert)

src/lake/Lake/Util/OrdHashSet.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+import Lean.Data.HashSet
 import Std.Data.HashSet.Basic
 
 open Lean