Trouble with standard library and imports

Stream: lean4

[Jesse Slater]

I am just starting with Lean, and I am having trouble understanding what the status of the standard library is, and how I can import whatever exists.
It is my understanding that the standard library is not complete for lean4 yet, but that it is being ported over. However, Theorem Proving in Lean 4 lists a bunch of functions which it says are in the standard library and that I can use. I found this https://leanprover-community.github.io/mathlib4_docs/Std/Logic.html, which seems to be a standard library for Lean 4, but when I try to import any of the packages, like Std.Logic, I get an error. Is this the correct standard library to be looking at? What do I need to do to import it?

[Arthur Paulino]

You need to add Std as a dependency on your lakefile.lean:

require std from git
  "https://github.com/leanprover/std4/" @ "d83e97c7843deb1cf4a6b2a2c72aaf2ece0b4ce8"

[Arthur Paulino]

Replace that hash with one that's compatible for you. You want a hash from a version that uses the same toolchain you're using (check the lean-toolchain file to know which toolchain you're using)

[Arthur Paulino]

This is the Std repo: https://github.com/leanprover/std4/
You can navigate the commit history and search for the appropriate version that you need

[Jesse Slater]

Thank you! That worked

[Jeremy Salwen]

Also I would suggest adding mathlib4 which I might consider colloquially part of the "standard" library, but it is in progress as you noted. The docs for mathlib4 are also accessible from the same docs link you shared.

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"