running lake causes duplicate download of Lean

Stream: new members

[Cheesehead]

Hi there.
I already installed a lean 4 toolchain with elan. After I created a new project with lake (after I used lake init in a path), however, running lake will printinfo: downloading component 'lean' and will automatically start to download a duplicate Lean. Why this happens and how should I prevent it from happening?
By the way, I would like to know how to install and use mathlib4 in my code. It seems that I should use the command lake exe cache get, but this also works for a single project. Will this lead to duplicate downloads of mathlib for each of the projects?
To be honest, I am still a little confused with the use of lake. It seems to be a Cabal equivalence for Lean, which provides convenience for building projects. But I am just going through some basic tutorials about theorem proving, and I don't even compile the codes. I am not sure whether I have to use lake, but I didn't find other way to install mathlib.

[Henrik Böving]

It is correct in doing this. Just because you have a version of Lean does not mean you have the correct version of Lean for your current project. Since Lean is still a quickly evolving language with new (potentially breaking) things every nightly each project maintains a lean-toolchain file with the precise version of Lean that it expects. Once lake gets run on a project the first thing that happens is that the proper Lean nightly will get downloaded and then that will be used for you. That said if you have two projects that happen to depend on the same nightly it will not redownload it after it got it for the first time

[Henrik Böving]

With respect to installting mathlib4 you have to declare it as a dependency in your lakefile and then it will just work. The lake exe cache get is a custom command provided by mathlib4 such that you do not have to compile mathlib4 from scratch in your depending project.

[Henrik Böving]

ANd finally yes you cannot get around using lake, it is the intended way of using Lean 4.

[Cheesehead]

Henrik Böving said:

It is correct in doing this. Just because you have a version of Lean does not mean you have the correct version of Lean for your current project. Since Lean is still a quickly evolving language with new (potentially breaking) things every nightly each project maintains a lean-toolchain file with the precise version of Lean that it expects. Once lake gets run on a project the first thing that happens is that the proper Lean nightly will get downloaded and then that will be used for you. That said if you have two projects that happen to depend on the same nightly it will not redownload it after it got it for the first time

Ok, that really makes sense. Thanks so much for your explanation!