Zulip Chat Archive

Stream: general

Topic: mathlib installation


Harrison Grodin (Dec 05 2019 at 21:03):

I'm having some trouble installing mathlib on Ubuntu. I tried running the recommended script, but in VSCode, I just get "file 'data/list/perm' not found in the LEAN_PATH". Any advice?

Johan Commelin (Dec 05 2019 at 21:07):

What did you do after the installation?

Johan Commelin (Dec 05 2019 at 21:07):

If you type #check 3 in VScode? Do you get some response in the "Lean messages" window?

Johan Commelin (Dec 05 2019 at 21:08):

@Harrison Grodin What do you mean with "installing mathlib"? The recommended method is to add mathlib as dependency to another package. Did you try that?

Harrison Grodin (Dec 05 2019 at 21:18):

I tried running the command given here: https://github.com/leanprover-community/mathlib/blob/master/docs/install/debian.md

Harrison Grodin (Dec 05 2019 at 21:19):

I have everything set up in VSCode (#check 3 works), but I don't totally understand how to gain access to mathlib.

Rob Lewis (Dec 05 2019 at 21:24):

When you followed the instructions here, are you sure you used "open folder" in VSCode?

Rob Lewis (Dec 05 2019 at 21:24):

https://github.com/leanprover-community/mathlib/blob/master/docs/install/project.md

Harrison Grodin (Dec 05 2019 at 21:34):

Oh, I see - I didn't actually install mathlib to my project. It works now - thanks so much!

Kevin Buzzard (Dec 05 2019 at 22:42):

.


Last updated: Dec 20 2023 at 11:08 UTC