Lean download

Stream: lean4

[Mohamamd Awheeo]

Hello I am trying to download lean to access it from the command line however all the methods are not working including downloading the vs code extension can someone share a clear method to download LEAN4 and access it from the command line

[Adam Topaz]

you can find detailed instructions here: https://leanprover-community.github.io/get_started.html#regular-install

TLDR: Install elan and you should be essentially all set to call lean from the command line.

[Mohamamd Awheeo]

thank you I downloaded elan using the following command : " curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh" now how can I start using it in the documentary it says open vs code and create a lean file but how to run it ?
TIA!

[Adam Topaz]

This should be helpful to get started: https://leanprover-community.github.io/install/project.html

[Mohamamd Awheeo]

I followed the steps and download the vs code extension as well but its stuck at "Waiting for Lean server to start..." message is there away to fix it?

[Mohamamd Awheeo]

image.png

[Kevin Buzzard]

You need to open the root directory of your project folder with VS Code's "open folder" functionality. In your screenshot you have opened the directory which is one above the root directory.

[Mohamamd Awheeo]

I opened the root directory and lean started crashing again:
image.png

[Mohamamd Awheeo]

image.png

[Mohamamd Awheeo]

is there away to run LEAN locally without VS code because I am not able to make it work

[Kyle Miller]

You want to open the folder my_project, not MyProject or installlean

[Mohamamd Awheeo]

still crashing :
image.png

[Mohamamd Awheeo]

the error is: Lean 4 client: couldn't create connection to server.
Message: Pending response rejected since connection got disposed
Code: -32097 @Adam Topaz

[Mac Malone]

@Mohamamd Awheeo What OS are you on?

[Mac Malone]

The error that occurred when starting the server has code 193, which generally means a Linux program was attempted to be run on Windows, there is an architecture mismatch, or there are some missing systems libraries

[Mac Malone]

One way I could see this happen is if you e.g., on Windows, installed elan through WSL/Cygwin and then tried to run lean through a native Windows VS Code installation.

[Galen Selligman]

Mac said:

One way I could see this happen is if you e.g., on Windows, installed elan through WSL/Cygwin and then tried to run lean through a native Windows VS Code installation.

I am having the same problem with (error code: 193) and
Message: Pending response rejected since connection got disposed
Code: -32097

I downloaded lean from the zip file from this link and installed like that
Adam Topaz said:

you can find detailed instructions here: https://leanprover-community.github.io/get_started.html#regular-install

TLDR: Install elan and you should be essentially all set to call lean from the command line.

I also saw that sometimes the project isnt configured properly, so used "lake new Sample" to get it going in VS Code, which was the recommended method in another thread.

image.png

[Sebastian Ullrich]

As Mac wrote, this error code should only be possible if you somehow have platforms mixed on your machine. For example, if Lake tried to call a Linux git.

[Sebastian Ullrich]

What is the zip file you mentioned?

[Galen Selligman]

From https://github.com/leanprover/elan/releases/tag/v2.0.1, which is linked from the README.md at https://github.com/leanprover/elan

Alternatively, on any supported platform: Grab the latest release for your platform, unpack it, and run the contained installation program.

The .zip file elan-x86_64-pc-windows-msvc.zip, because my pc runs windows 10.
Using the lean4 extension (leanprover.lean4) in vs code, as specified from here https://leanprover-community.github.io/install/windows.html. You can see I tried to follow the instructions specified for windows.

[Sebastian Ullrich]

I see, @Adam Topaz's tl;dr was confusing then because elan is usually installed for you as mentioned in the community instructions. But the way you did it should be fine.