installing lean4

Stream: new members

[stewart mandell]

I'm new to everything here, including Tulip. I followed the instructions to install VSCode, lake, and the lean4 extension for VSCode. I make a folder which I see contains the required lake files etc. However when I open Main.lean or MyProject.lean and try to do something as simple as #eval 1 + 1 I get a squiggly line and it doesn't evaluate. I hope someone can get me started, I spent the whole day trying to do this.

[Matt Diamond]

Are you opening the folder in VSCode or just an individual file?

[Matt Diamond]

if it's the latter, try opening the folder instead (use File > Open Folder... instead of File > Open...)

[Notification Bot]

This topic was moved here from #mathlib4 > installing lean4 by Kim Morrison.

[Kim Morrison]

@stewart mandell just pinging you here in case you worry that your message disappeared.

[Kevin Buzzard]

Say which instructions you followed and send a screenshot of VS Code with the file visible and the file explorer open