Zulip Chat Archive

Stream: new members

Topic: leanpkg.path does not exist

ZainAK283 (Jan 18 2023 at 21:21):

Hi all,
I've tried to open some Lean file in VS Code but I'm getting a "Lean: leanpkg.path does not exist" error. I think something has gone wrong in the installation but I'm not savvy enough to know what :sweat_smile:
image.png
Thank you

Kevin Buzzard (Jan 18 2023 at 21:46):

I don't know how you got this project into that state (did you use leanproject to download it? That should make leanpkg.path for you) but just clicking "run leanpkg configure" should fix the problem you have.

ZainAK283 (Jan 18 2023 at 21:55):

I used leanproject to download it, yes
I clicked "run leanpkg configure" and get this error
image.png
I changed the home directory though, so I don't think it should be looking in "C:\Users\zaina\"...?

Kevin Buzzard (Jan 18 2023 at 21:56):

If you haven't actually done anything with this repo yet, then I would just delete it and re-install it in the way described in the README and then watch carefully for errors. This shouldn't be happening.

ZainAK283 (Jan 18 2023 at 21:58):

Does "deleting it" just mean literally deleting the folder "mathematics_in_lean"? Or is there something more subtle that I have to do?

Kevin Buzzard (Jan 18 2023 at 21:59):

If I type leanproject get mathematics_in_lean then I get a copy of the repo including a leanpkg.path. Yes, just delete the directory and then recreate it with leanproject get mathematics_in_lean.

Kevin Buzzard (Jan 18 2023 at 21:59):

What does leanproject --version give you, by the way?

ZainAK283 (Jan 18 2023 at 22:05):

Deleting it and reinstalling it worked (though I'm sure I tried that before), thank you :)
leanproject --version gives me leanproject, version 0.0.10

Eric Wieser (Jan 18 2023 at 22:09):

That's ancient

ZainAK283 (Jan 18 2023 at 22:11):

I installed lean on my laptop back in May 2020 (if not earlier), so it might be from back then? I followed all the steps in https://leanprover-community.github.io/install/windows.html though so if it was meant to update lean or leanproject, it seems like it hasn't...?

Patrick Massot (Jan 18 2023 at 22:13):

Typing pip3 install mathlibtools won't update, you need pip3 install -U mathlibtools

Patrick Massot (Jan 18 2023 at 22:14):

Those are installation instructions, not updating instructions.

ZainAK283 (Jan 18 2023 at 22:15):

leanproject --version now gives output leanproject, version 1.3.2

ZainAK283 (Jan 18 2023 at 22:23):

Thank you all :)

Last updated: Dec 20 2023 at 11:08 UTC