Trouble with library_search

Stream: new members

[azorlogh]

Hi, I'm new here, I'm following this demo : https://www.youtube.com/watch?v=b59fpAJ8Mfs
And for some reason, the library search at 13:40 fails with only the message "failed"
I'm using Lean v3.4.2 on linux, installed through elan and on VSCode
I installed the mathlib library by doing leanpkg add leanprover/mathlib
Am I doing something wrong?

[Eric Wieser]

Yes, you should be using the community version of lean, 3.28

[Eric Wieser]

Mathlib only works with the latest version

[azorlogh]

Oooh ok I thought this was the latest version, thank you!
Do I need to clone the community repo to install it with elan ?

[azorlogh]

It looks like my package manager has a package for the community version so I think I'll use that

[Alex J. Best]

Hopefully your package manager is just installing elan, that is the recommended way to work with multiple lean versions! Which manager is it?

[Alistair Tucker]

It sounds as if the installation instructions you followed were old ones. Nowadays we are supposed to interface with leanproject rather than with leanpkg. If you can install it using the instructions here, afterwards you'll be able to get the latest versions of everything by calling leanproject up.

[Kevin Buzzard]

Yeah you can't really use a package manager to install Lean right now because you need all the addons too

[Scott Morrison]

We really should try to evict Lean from the various package managers. :-(