getting lean to work with visual studio code

Stream: new members

[Bjørn Remseth]

• I'm following instructions on https://leanprover-community.github.io/install/project.html
• I've started visual studio code on 01_equality_rewriting.lean, and opened the "lean Infoview " pane.
• I don't see any helpful interaction with the lean backend.
• What I do see is the error message "file 'data/real/basic' not found in the search path" (also see attached screenshot Screenshot-2021-06-20-at-17.20.04.png
  
• Any help to talk to lean will be appreciated.

[Alex J. Best]

Did you checkout and try the suggestions in https://leanprover-community.github.io/file-not-found.html ?

[Bjørn Remseth]

Yes I did. Looks legit. I looked at the files in leanpkg.path and looked for any file or directory called "basic" in those directories, but couldn't find any by that name.

[Kevin Buzzard]

From the screenshot it looks to me like you did not open a Lean project in VS Code using the "open folder" functionality.

[Bjørn Remseth]

:-) That may well be right. I'm a bit of a VS Code noob. I'll try to do that and see what happens.

[Bjørn Remseth]

That fixed it. Wonderful. Thank you so much :-)