Difference between `Std` and `Batteries` HashMap?

Stream: new members

[Philogy]

I was curious to know what the different / overlap between the Std and Batteries library is and how I import Std? I'm trying to use the HashMap struct, thanks!

[Damiano Testa]

Std was renamed to Batteries at some point, though not all Std namespaces have disappeared.

[Henrik Böving]

That's wrong, there does exist a built in Std and you can import it, its also actively being pushed by the FRO. Std's HashMap is also superior to what is currently present in batteries in terms of what you can program and prove with it.

To import use import Std.Data.HashMap or HashSet or DHashMap depending on your needs

[Henrik Böving]

Note that you need to be on a sufficiently recent lean version in order to use it though!

[Philogy]

Henrik Böving said:

That's wrong, there does exist a built in Std and you can import it, its also actively being pushed by the FRO. Std's HashMap is also superior to what is currently present in batteries in terms of what you can program and prove with it.

To import use import Std.Data.HashMap or HashSet or DHashMap depending on your needs

Thanks I was just a bit confused because I'd import it but directly using HashMap after the import didn't work, realized I needed to use it via Std.HashMap or do open Std to access HashMap. Tbh I don't fully understand how the import and namespacing convention works, I thought in an import statement the last leg is the namespace you import and have access to? So import Std.Data.HashMap would give me access to the HashMap namespace, but it gives me access to the Std.HashMap namespace?

[Kevin Buzzard]

Namespaces and imports are unrelated concepts in lean.

[mars0i]

Henrik Böving said:

That's wrong, there does exist a built in Std and you can import it, its also actively being pushed by the FRO. Std's HashMap is also superior to what is currently present in batteries in terms of what you can program and prove with it.

At present, does it look like the future will lead to Batteries taking over relevant parts of Std, or does it seem that where there are obvious approximate overlaps, the two libraries will continue to develop along parallel lines?

I know that this sort of thing can change over time as contributors and their goals change, but sometimes there's a plan that clarifies what intended to happen.

(I'm looking at the Batteries github page, but have not yet found a main page for the Std project. I'm probably just overlooking some link somewhere.)

[Henrik Böving]

The Std project is built into Lean 4 and mainly maintained by the FRO right now, the batteries project is a community one. Std is going to stay integrated with Lean 4. People do occasionally stream things from batteries into Std but its rather rare that code flows back from Std into batteries. The vision for Std is to be a comprehensive programming language standard library that also has verification mechanisms built in where applicable. The vision for batteries I do not know

[mars0i]

I see there's relevant discussion about Batteries in this thread.