leanproject: command not found

Stream: new members

[Merel Steenbergen]

I have tried to install Lean by following this tutorial:
https://leanprover-community.github.io/install/windows.html, I've also checked the youtube video to make sure everything was correct. Leanprover in VS Code works so far (haven't been able to run a project obviously, but #eval 1+1 does give me the expected output). However, when I try to get the leanproject I need to run, my bash returns bash: leanproject: command not found

I am using: Windows10, Git version 2.37.0.windows.1, Python 3.8.5.

I have already tried:

• Reïnstalling (also when opening Git Bash as administrator, I saw that in an old chat)
• source ~/.profile
• Rebooting my PC
• I've checked whether the elan/lib is in my PATH variable (it is)

Can anyone help me?

[Eric Wieser]

Note that leanproject is unrelated to elan, and is described in this section

[Eric Wieser]

The TL;DR is pip install mathlibtools

[Merel Steenbergen]

Eric Wieser zei:

The TL;DR is pip install mathlibtools

I did that and it installed, that's why I don't know why it's not working

[Eric Wieser]

What does pip -V give?

[Merel Steenbergen]

pip 22.3.1 from C:\Users\merel\AppData\Local\Packages\PythonSoftwareFoundation.Python.3.8_qbz5n2kfra8p0\LocalCache\local-packages\Python38\site-packages\pip (python 3.8)

[Eric Wieser]

That's a pretty unusual path; how did you install python?

[Eric Wieser]

Does python -m mathlibtools.leanproject work for you?

[Merel Steenbergen]

I think it might be using a version I have installed through my university. I'll try to reinstall Python.

[Eric Wieser]

I wouldn't do that yet

[Merel Steenbergen]

Eric Wieser zei:

Does python -m mathlibtools.leanproject work for you?

Yes

[Eric Wieser]

Great, then that just means that python's Scripts/ directory is not on your PATH

[Eric Wieser]

Does C:\Users\merel\AppData\Local\Packages\PythonSoftwareFoundation.Python.3.8_qbz5n2kfra8p0\LocalCache\local-packages\Python38\Scripts exist for you?

[Merel Steenbergen]

Eric Wieser zei:

Great, then that just means that python's Scripts/ directory is not on your PATH

I'll check and fix it! Thanks!

[Merel Steenbergen]

Eric Wieser zei:

Does C:\Users\merel\AppData\Local\Packages\PythonSoftwareFoundation.Python.3.8_qbz5n2kfra8p0\LocalCache\local-packages\Python38\Scripts exist for you?

Yes

[Eric Wieser]

Great, add that to your path and you should be done (assuming leanproject is in there)

[Merel Steenbergen]

Eric Wieser zei:

Great, add that to your path and you should be done (assuming leanproject is in there)

It works! Thanks so much :)

[gaming with yoty]

I followed the same steps, pip -V gives: "pip 23.1.2 from C:\Users\yotam\AppData\Roaming\Python\Python310\site-packages\pip (python 3.10)"
yet there is no leanproject file in C:\Users\yotam\AppData\Roaming\Python\Python310\Scripts, what do I do (I'm using windows 11 if that matters)

[Eric Wieser]

What does where leanproject give? nevermind

[Eric Wieser]

As a workaround you can use python -m mathlibtools.leanproject instead of leanproject

[gaming with yoty]

I have indeed been doing that, I just thought there might be a way to still use leanproject

[Julian Berman]

What does python -m pip -V say?

[Julian Berman]

You seem to have at least 2 Python installs from the above, a 3.8 and a 3.10 (which is fine, but your python and your pip might not be from the same one).

[Eric Wieser]

Julian, as far as I can tell the 3.8 version was a different user

[Julian Berman]

Oh, indeed, well done me.

[gaming with yoty]

Julian Berman said:

What does python -m pip -V say?

well, for the record, python -m pip -V says:
pip 23.1.2 from C:\Users\yotam\AppData\Roaming\Python\Python310\site-packages\pip (python 3.10)

[Julian Berman]

OK, and you see no leanproject in the scripts directory? You can try pip install --force-reinstall mathlibtools and see if that helps.

[gaming with yoty]

That worked! Thank you so much!