Which HashMap implementation should I use?

Stream: general

[nrs]

According to Loogle, there's Std.HashMap, Lean.HashMap, and Batteries.HashMap. Is there any one of these that is recommended to use, or better suited for particular purposes? Or are they pretty much the same?

[Damiano Testa]

One of the two should be deprecated: if you used one and you did not get a deprecation, you're using the correct one!

[nrs]

I see, thank you!!

[Eric Wieser]

None of them are deprecated in mathlib master as far as I can tell

[nrs]

can confirm that importing these and using #print on their names does not report any deprecation notice

[Damiano Testa]

Ooh then I misremember: I thought that I had some deprecation about them, but maybe it was hashset then?

[Damiano Testa]

#print may not be enough to trigger a deprecation (#check is not enough, print... Maybe!)

[Shreyas Srinivas]

Std.HashMap has all the nice lemmas iirc

[David Renshaw]

https://leanprover-community.github.io/mathlib4_docs/Lean/Data/HashMap.html#Lean.HashMap

[David Renshaw]

^ looks deprecated to me

[Eric Wieser]

import Batteries

def a : Std.HashMap Nat Nat := sorry
def b : Lean.HashMap Nat Nat := sorry
def c : Batteries.HashMap Nat Nat := sorry

[David Renshaw]

https://github.com/leanprover/lean4/blob/7dc1ceb8d4312850b39cef9e751e0a3b651946e3/src/Lean/Data/HashMap.lean#L274

[Eric Wieser]

Indeed, the deprecation shows up if you don't use #check

[nrs]

tyvm for answers!! hm, if Std.HashMap has more lemmas, is there any reason to use Batteries.HashMap?

[Damiano Testa]

Damiano Testa said:

#print may not be enough to trigger a deprecation (#check is not enough, print... Maybe!)

Here is a similar discussion about deprecation and #check.

[Kim Morrison]

Please only use Std.HashMap going forward!

[Kim Morrison]

https://leanprover.zulipchat.com/#narrow/channel/348111-batteries/topic/Unifying.20.60Batteries.2EHashMap.60.20and.20.60Std.2EHashMap.60.2E/near/477103618 is my proposal for a deprecation path for Batteries.HashMap.

[nrs]

Will do, ty for answer!