Use of leanpkg

Stream: new members

[Aaryan Prakash]

Hello, I have just started learning about Lean and I was a little confused about the installation steps. According to https://leanprover-community.github.io/toolchain.html#handling-dependencies, is it correct that we are not supposed to use leanpkg at all, i.e. we should only use leanproject? Or are there certain cases when we would have to use leanpkg?

[Kevin Buzzard]

If you want to use Lean 3 (e.g. if you want to use the maths library) then you don't need to worry about leanpkg, it will all be taken care of by leanproject (follow the installation instructions and you'll end up with leanpkg installed anyway but you won't ever execute it yourself)