Difficulty Installing mathlib

Stream: general

[Chu-Wee Lim]

I followed the instructions here: https://github.com/leanprover-community/mathlib

Everything seemed fine: no error messages but the directory $HOME/.mathlib only contained the following files and nothing more.

.
./bin
./bin/auth_github.py
./bin/cache-olean
./bin/delayed_interrupt.py
./bin/setup-lean-git-hooks
./bin/update-mathlib
./hooks
./hooks/post-checkout
./hooks/post-commit

I already have lean working in Visual Studio Code, but only having difficulty adding mathlib to it.

Thanks in advance for any help.

[ Update: In desperation, I got it to work by using leanpkg add, then manually copying all the directories to the appropriate subfolder in .elan. ]

[Alex J. Best]

Have you seen, https://github.com/leanprover-community/mathlib/blob/master/docs/install/project.md I think this is the recommended way to work with mathlib now, what you have installed is the mathlib-tools scripts, which include update-mathlib, which when used in a project should save some time, but adding mathlib as a project dependency and running leanpkg add as in the link will download and install mathlib for you for a project.

[Chu-Wee Lim]

Thanks. I decided to do it the proper way by reinstalling everything by following the instructions at the above link step-by-step. I managed to install elan, lean again, but VScode again can't find mathlib.

For example, "import topology.basic" gives the error message "file 'topology\basic' not found in the LEAN_PATH" whereas "import init.data.nat" works fine.

The weird thing is that in the "my_project" directory, I could find all the lean and olean files, but somehow VScode can't read them.

[Alex J. Best]

To be clear in your my_project do you have a folder _target/deps/mathlib/src/ with the mathlib files in? Thats how leanpkg add should leave it set up

[Chu-Wee Lim]

Yes, all the lean files are there in the directory, even the olean files.

[ Update: I re-installed the mathlib extension in a separate directory and for some reason it's now working. Thanks for helping me out. ]