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: Aug 03 2023 at 10:10 UTC