have trouble running leanproject

Stream: new members

[Alex Zhang]

I am trying to use Lean on one of my laptops (Win 10) in VS code.
But leanproject new my_project fails with the message bash: leanproject: command not found.
Could anyone please let me know what might be the problem?

[Kevin Buzzard]

You didn't follow the instructions to the letter :-)

[Kevin Buzzard]

Which instruction you failed to do -- who knows!

[Alex Zhang]

I followed the instruction and reinstalled everything actually. It's quite weird this problem is still there

[Kevin Buzzard]

Your situation is impossible to debug because there are many reasons why it might not work

[Kevin Buzzard]

Are you using git bash?

[Kevin Buzzard]

is leanproject on your system but not in your path, or not on your system?

[Kevin Buzzard]

did you try turning it off and on again?

[Alex Zhang]

Yes, git bash.
I will try to restart my laptop..

[Eric Wieser]

How did you install leanproject?

[Alex Zhang]

It seems OK now after I restarted my computer......
(I just tried to restart VS code and the terminal before, which didn't work)

[Yakov Pechersky]

Sounds like a shell restart problem. Something (likely pip) added leanproject to your shell's PATH but since you hadn't restarted the shell, it wasn't being found. Restarting the computer was an intense way of restarting the shell.

[Huỳnh Trần Khanh]

generally source ~/.profile does the trick. you can also log out and log in again, you don't need to restart your computer