Zulip Chat Archive

Stream: new members

Topic: Trouble with library_search


azorlogh (Apr 16 2021 at 18:44):

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 (Apr 16 2021 at 18:46):

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

Eric Wieser (Apr 16 2021 at 18:46):

Mathlib only works with the latest version

azorlogh (Apr 16 2021 at 18:50):

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 (Apr 16 2021 at 18:52):

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

Alex J. Best (Apr 16 2021 at 20:06):

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 (Apr 16 2021 at 21:03):

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 (Apr 16 2021 at 21:51):

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

Scott Morrison (Apr 17 2021 at 00:33):

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


Last updated: Dec 20 2023 at 11:08 UTC