I can't use mathlib

Stream: new members

[Victor Hugo Hernandez]

Hello, after playing a while with lean's online version, I decided to install it in my pc. I am currently running ubuntu 18.04 LTS and when I try to import things such as Mathlib.MeasureTheory.Measure.Lebesgue.Complex, I get an error in VS code: 'unknown package Mathlib', I was wondering if I could get some help in fixing this error

[Kevin Buzzard]

Did you create a lean repository on your computer using lake and then open the root directory of the repository using VS Code's "open folder" functionality?

[Victor Hugo Hernandez]

@Kevin BuzzardNo, where can I find how to do that?

[Niels Voss]

I think the easiest way to set up the lean files is to run

lake new myproject math

from a command line (Make sure to include the word "math" otherwise you will have to manually add Mathlib as a dependency). This will create a new folder with some files in it. If you navigate to that folder and from it run

lake update
lake exe cache get

The first command will download the mathlib source code to the lake-packages folder, and the second command will download precompiled versions of mathlib so that it doesn't take a hour to compile everything the first time you try to import a file.

[Victor Hugo Hernandez]

It worked, thank you two