Zulip Chat Archive

Stream: new members

Topic: invalid import in tutorials


view this post on Zulip Madjosz (Jun 09 2020 at 09:27):

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.

view this post on Zulip Kevin Buzzard (Jun 09 2020 at 09:41):

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

view this post on Zulip Johan Commelin (Jun 09 2020 at 09:41):

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

view this post on Zulip Johan Commelin (Jun 09 2020 at 09:41):

Did you do that?

view this post on Zulip Madjosz (Jun 09 2020 at 09:48):

@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!

view this post on Zulip Johan Commelin (Jun 09 2020 at 09:48):

Great!

view this post on Zulip Kevin Buzzard (Jun 09 2020 at 09:49):

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


Last updated: May 14 2021 at 06:16 UTC