Problem with installing lean

Stream: new members

[Kaixin Wang]

Hi! I am running into this issue:

image.png

I am on windows 10 lenovo laptop computer.

I followed the instructions here: https://leanprover-community.github.io/install/windows.html up to and try to get the extension to install elan and lean.

I never got this dialog: "saying Failed to start 'lean' language server with a button Install Lean using Elan."

[Bernardo Borges]

It installed correctly. It's just that the folder you opened in vscode os not a project created with lake init. You can still create files and use Lean normally

[Bernardo Borges]

Try pressing Ctrl + Shift + P and then type Lean 4: Infoview. It should load and when you put the cursor on the blue squigly it should display 37

[Kaixin Wang]

At this stage in command prompt
image.png

[Kaixin Wang]

How do I install
I keep on getting installation abort

[Kaixin Wang]

image.png

[Bernardo Borges]

What happens with you just proceed with 1 at this stage?

[Kaixin Wang]

(This is on administrator command prompt

[Bernardo Borges]

Do you have vscode open right now? Maybe it's keeping this file locked

[Kaixin Wang]

Now it's like this
image.png

there is still a warning but at least the underline and the output is present

[Kaixin Wang]

Oh sorry I didn't see your messages until now

[Bernardo Borges]

Looks like it's installed all right

[Kaixin Wang]

Hmm I still have the issue of "Opened folder is not a valid Lean 4 project. Please open a valid Lean 4 project containing a 'lean-toolchain' file for full functionality"
I guess I will ignore that for now.

[Kaixin Wang]

https://github.com/leanprover/vscode-lean4/issues/323
I found this which isn't quite helpful

[Kaixin Wang]

"The default toolchain error should be pretty rare because it only occurs if the user both fiddled with elan toolchain uninstall and opened the wrong folder. I'd hope the amount of users that know how to use elan on the command line but do not know what a Lean project folder is to be relatively small." I didn't fiddle with elan toolchain uninstall .....

[Bernardo Borges]

Bernardo Borges said:

It installed correctly. It's just that the folder you opened in vscode os not a project created with lake init. You can still create files and use Lean normally

Did you open a folder in which you ran lake init?

[Kaixin Wang]

How do I run a command on a folder

[Kevin Buzzard]

you run the command in the root directory of the folder

[Kaixin Wang]

image.png

[Kaixin Wang]

Like this?

[Kaixin Wang]

I see no error now

[Kaixin Wang]

I think I fetched the mathematics_in_lean repository and open it up in VS Code.

[Kaixin Wang]

I tried typing in
image.png

[Kaixin Wang]

This is what it looks like on vscode
image.png

[Kaixin Wang]

I also have this issue
image.png

[Kaixin Wang]

Ok this works: I changed N to Nat
image.png