Fresh install could not resolve import

Stream: new members

[Lachlan Robinson]

Hi,
I have just installed lean on Ubuntu 18.04 and created a directory for the tutorials. I then ran the leanproject get tutorials command however when I open any of the files in the src file I am greeted with errors.

image.png
image.png

I would really appreciate it if someone could help me. It is probably a really simple solution.

[Alex J. Best]

You have to open the directory tutorials in vscode using vscode's open folder button, rather than the higher one Lean. Also you need to change into that directory to run leanproject get-mathlib-cache. Hopefully that should resolve everything!

[Lachlan Robinson]

Alex J. Best said:

You have to open the directory tutorials in vscode using vscode's open folder button, rather than the higher one Lean. Also you need to change into that directory to run leanproject get-mathlib-cache. Hopefully that should resolve everything!

Thanks so much, it worked!