help w/ leanproject command

Stream: new members

[Abram Demski]

Hi! I'm just getting started with Lean, and have followed the installation instructions here, on Windows 11:

https://leanprover-community.github.io/install/windows.html

Everything seems fine there.

It looks like the next step is to create a lean project to mess around with, so I'm trying to follow the instructions here:

https://leanprover-community.github.io/install/project.html

When I try to run the leanproject command to create a new project, in git bash, I just get "bash: leanproject: command not found".

(EDIT: Forgot to mention, the solution mentioned in the instructions, "source ~/profile" or "source ~/.bash_profile", do not seem to accomplish anything.)

I searched my filesystem for "leanproject" to see whether it existed anywhere. Indeed it does: it exists at

C:\Users\abram\AppData\Local\Packages\PythonSoftwareFoundation.Python.3.11_qbz5n2kfra8p0\LocalCache\local-packages\Python311\Scripts\leanproject

There's also a leanproject.py, here:

C:\Users\abram\AppData\Local\Packages\PythonSoftwareFoundation.Python.3.11_qbz5n2kfra8p0\LocalCache\local-packages\Python311\site-packages\mathlibtools\leanproject.py

When I run 'which python' or 'which python3' I get the python installed during the installation instructions:

/c/Users/abram/AppData/Local/Programs/Python/Python311/python
/c/Users/abram/AppData/Local/Programs/Python/Python311/python3

(The slashes are the opposite direction because I'm pasting from git bash here, while the earlier file location was pasted from the windows file explorer.)

Whereas which pip and which pip3 give the following:

/c/Users/abram/AppData/Local/Microsoft/WindowsApps/pip
/c/Users/abram/AppData/Local/Microsoft/WindowsApps/pip3

I don't know whether any of this points to what is going wrong, just reporting what I can.

[Abram Demski]

I've apparently solved the problem by running:

export PATH=$PATH:"/c/Users/abram/AppData/Local/Packages/PythonSoftwareFoundation.Python.3.11_qbz5n2kfra8p0/LocalCache/local-packages/Python311/Scripts"

LMK if there are any obvious further problems with my setup that I should fix based on the info I've provided. (Or, I'll complain here when it inevitably breaks if so...)

[Eric Wieser]

Note that when you install python, there would have been an "add to path" checkbox that should have done that for you

[Abram Demski]

OK, I admit, that was probably my mistake... at the time I thought I must have done that, since I was seeing the correct python location with 'which python', but I guess I must have been seeing that for other reasons.