install mathlib

Stream: new members

[Victor Porton]

How install mathlib without waiting till it completely compiles?

[Victor Porton]

I mean how to add it to my project.

[Arthur Paulino]

Is it already added as a dependency in the leanpkg.toml file? If you already have it as a dependency, leanproject get-mathlib-cache should do the trick

[Victor Porton]

@Arthur Paulino It isn't.

[Arthur Paulino]

Then try leanproject add-mathlib first

[Arthur Paulino]

leanproject --help will list a lot of helpful information about what it's capable of doing

[John Honaker]

Install matlib using leanproject, not leanpkg. If you have already installed it using leanpkg, delete _targets and the line in the leanpkg.toml.

[John Honaker]

I ran into this the other day, when I didn’t realize the difference