Installation on windows using VS Code

Stream: new members

[Quantum_fluctuations]

I am new to LEAN. I was trying to install LEAN on my windows OS. I followed all steps correctly and the everything was going same as in the walkthrough video, but in the end when I restarted VS code and tried to write a code, it's not working. Can someone please help? I don't know what went wrong. I changed the default profile to git bash, but the code #eval 2+2 is not showing anything. It's not coloured either.
Can anyone please help me?

[Newell Jensen]

Make sure that when you are opening the top folder for a lean project that you are working on or VS Code can have issues. Not sure this will help your situation but I would make sure you are doing that at least.

[Newell Jensen]

That is, from within VS Code do File -> Open Folder and then choose which top folder of a lean project that you are working on.

[Quantum_fluctuations]

Thanks for the response. I was making a stupid mistake. I wasn't writing the extension ".lean" while saving the file. Now, that's corrected.
Now, it's showing "Waiting for LEAN server to start"
image.png

[Quantum_fluctuations]

Is there possibly a mistake I have made on my system? Or is the LEAN server's problem?

[Johan Commelin]

Hmm, did you follow https://leanprover-community.github.io/get_started.html#regular-install ?
And after that: https://leanprover-community.github.io/install/project.html ?

[Kevin Buzzard]

From the screenshot it looks like you have not made a lean project.

[Quantum_fluctuations]

Yes, I hadn't. Now, I have.
image.png
Thanks a lot.

[Peter Gumm]

Hi,
i tried installing lean4, following the instructions on https://leanprover-community.github.io/install/windows.html
I got until creating the first lean4 file, and entering "#eval 1 + 2" . The infoview says "Waiting for Lean server to start". But nothing happens.
Then I tried to reinstall elan. It ends with a failure:
"could not create link from 'C:\Users\gumm\.elan\bin\elan.exe' to 'C:\Users\gumm\.elan\bin\leanc.exe'"
The mentioned directories and files are present ...
:-(

[Kevin Buzzard]

Did you make a lean project and then open the root directory of the project in VS Code using the "open folder" functionality? You can't just run lean on a bare file (you get the error which you're reporting)

[Julian Külshammer]

Just to comment on this: I ran into the same problem as Peter. The installation instructions mention that one should just open a text file and then nothing happened. However, at least for me it worked just continuing with the instructions on setting up a project. If this happens to several people maybe the instructions on the Windows installation should be changed?

[Shreyas Srinivas]

We could indeed do with a tutorial style introduction. Perhaps this helps for now: https://lean-lang.org/lean4/doc/quickstart.html

[Shreyas Srinivas]

also, one should open a <some_file_name>.leannot just a text file. The instructions from within vscode ask to select the language. That's important. But it can be accomplished by naming the file with a .lean extension

[Shreyas Srinivas]

@Kevin Buzzard : you can open a random lean file in isolation. The file extension ".lean" suffices to tell vscode (after the lean4 extension is installed) that it is a lean file

[Patrick Massot]

Shreyas Srinivas said:

Kevin Buzzard : you can open a random lean file in isolation. The file extension ".lean" suffices to tell vscode (after the lean4 extension is installed) that it is a lean file

We should really stop pointing this out. This only leads to disaster when people want to actually do anything with their lean files.

[Shreyas Srinivas]

@Patrick Massot apologies. Although in the case of installation issues (i.e. no lake yet), I don't immediately understand how we can ask users to create a lean project