Zulip Chat Archive

Stream: new members

Topic: Use of leanpkg

Aaryan Prakash (Dec 06 2021 at 00:20):

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 (Dec 06 2021 at 00:21):

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)

Last updated: Dec 20 2023 at 11:08 UTC