Setting up tutorials

Stream: new members

[Avi Craimer]

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

[Alex Peattie]

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

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

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

[Avi Craimer]

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.