Zulip Chat Archive

Stream: new members

Topic: Setting up tutorials


view this post on Zulip Avi Craimer (Sep 24 2020 at 15:12):

Hello,
I'm new to lean. I just installed it on MacOS with the command line, then I downloaded the tutorials and copied the exercises folder. However, on the lean projects page, there aren't any instructions for how to run the code. Also, I am getting errors in VS Code saying that the imports cannot be found. Is there another magic command I need to run to get it all working?

Screen-Shot-2020-09-24-at-11.12.25-AM.png

view this post on Zulip Alex Peattie (Sep 24 2020 at 15:16):

How did you download the tutorials? Did you do leanproject get tutorials?

view this post on Zulip Bryan Gin-ge Chen (Sep 24 2020 at 15:17):

One common mistake that leads to this issue is opening a single file in VS Code instead of the entire project directory.

view this post on Zulip Bryan Gin-ge Chen (Sep 24 2020 at 15:19):

Also, when you say you installed Lean with the command line, do you mean you followed all the instructions here and then here?

view this post on Zulip Bryan Gin-ge Chen (Sep 24 2020 at 15:20):

Doing something else (like trying to use homebrew's Lean) will probably not work.

view this post on Zulip Avi Craimer (Sep 24 2020 at 16:01):

Bryan Gin-ge Chen said:

One common mistake that leads to this issue is opening a single file in VS Code instead of the entire project directory.

I realized in VS Code I'd opened up a parent folder that container the project folder. When I opened just the project folder it worked. Thanks everybody for the troubleshooting advice.


Last updated: May 08 2021 at 09:11 UTC