invalid import in tutorials

Stream: new members

[Madjosz]

Hi, I just installed VS code like described in https://leanprover-community.github.io/install/windows.html but when I try to run the tutorials project in VS code I get:

invalid import: data.real.basic
could not resolve import: data.real.basic

Can anybody help me to resolve this? When I run lean 00_first_proofs.lean from the command line, everything seems to work.

[Kevin Buzzard]

Isn't there some link which is now advertised when this error pops up, which lists possible solutions?

[Johan Commelin]

@Madjosz In VScode, there is a difference between "Open Folder" and "Open File". You need to use "Open Folder".

[Johan Commelin]

Did you do that?

[Madjosz]

@Kevin Buzzard "No quick fixes available".
@Johan Commelin I did use it but you got me onto the right path: I created a base folder for testing which I opened with "Open Folder". Then I cloned the tutorials into a sub folder which messes up the paths. I have to choose the tutorials folder when doing "Open Folder", this fixes it. Thanks!

[Johan Commelin]

Great!

[Kevin Buzzard]

If you're working on a project, you have to open the project folder in VS Code