Zulip Chat Archive

Stream: new members

Topic: Trouble with library_search


view this post on Zulip 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?

view this post on Zulip Eric Wieser (Apr 16 2021 at 18:46):

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

view this post on Zulip Eric Wieser (Apr 16 2021 at 18:46):

Mathlib only works with the latest version

view this post on Zulip 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 ?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Scott Morrison (Apr 17 2021 at 00:33):

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


Last updated: May 16 2021 at 20:13 UTC