mathlib installation

Stream: general

[Harrison Grodin]

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]

What did you do after the installation?

[Johan Commelin]

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

[Johan Commelin]

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

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

[Harrison Grodin]

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

[Rob Lewis]

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

[Rob Lewis]

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

[Harrison Grodin]

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

[Kevin Buzzard]

.