Zulip Chat Archive

Stream: general

Topic: Difficulty Installing mathlib

Chu-Wee Lim (Oct 09 2019 at 06:51):

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.


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 (Oct 09 2019 at 07:08):

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 (Oct 09 2019 at 08:36):

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 (Oct 09 2019 at 08:39):

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 (Oct 09 2019 at 08:44):

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. ]

Last updated: Dec 20 2023 at 11:08 UTC