New to Lean

Stream: lean4

[Mahdi Sh]

Hi, I'm new and have issues with installation.
I wanted to use ELAN on Visual Studio Code. In one of the installation steps, it is mentioned to use the command "elan toolchain install leanprover/lean4:stable", which starts downloading the file "lean-4.20.0-windows.tar.zst". However, due to my very poor internet connection, this download fails every time. I have directly downloaded the "lean-4.20.0-windows.tar.zst" file myself. Now, how can I use toolchain to install it from the file on my computer's hard drive (the downloaded file) instead of downloading it from the internet?

[Ruben Van de Velde]

Please don't double post

[Serhii Khoma (srghma)]

ELAN is rustup, so maybe in rust comunity people can help too

[Edward van de Meent]

i seem to recall from multiple conversations that this is a common misconception?

[Edward van de Meent]

or actually, that might be lake being related to cargo

[Mac Malone]

Elan is derived from the rustup codebase. Lake takes some inspiration from Cargo (and other package mangers / build systems), but has no code overlap.

[Notification Bot]

3 messages were moved from this topic to #lean4 > mu eq pi by Mario Carneiro.