How to write a lakefile.lean in Oct 2024 to get packages?

Stream: new members

[Britt Anderson]

I am trying to play with Lean and trying to work in a package setting as a learning exercise. I edited some code and realized I wanted some hashmap function that I think is in Lean.Data.HashMap. I believe I need to put a require line into my lakefile.lean, but on reaching this point I realize I don't really know how to add requirements incrementally as I need them to my lakefile. I also find a require from syntax and a require / syntax. Can I be pointed to some source for how this is supposed to go?

[Henrik Böving]

1. You don't need to add any required to import from Lean or Std, they are built in
2. You want to use Std.Data.HashMap nowadays, the Lean.Data.HashMap one is internal to the compiler and will be removed soon
3. If you are using a sufficiently recent version of lean the go to way would be something like this: require "leanprover-community" / "aesop" @ git "master" For requiring the aesop package from reservoir: https://reservoir.lean-lang.org/@leanprover-community/aesop at git tag master

[Britt Anderson]

Thank you very much. Is there a up to date beginners guide for this? The starting a package chapter in Functional Programming in Lean is a bit thin on details.