lake: command not found

Stream: new members

[Sjaak Smetsers]

What should I do if I type 'lake intit foo' in vscode and then get the message 'lake: command not found'? A very specific hint please, because I don't understand the rest anyway.

[Julian Berman]

What have you run / followed to install Lean? That would sound like you don't have Lean 4 installed, or if you do, that it's not on your PATH.

[Sjaak Smetsers]

Lean 4 seems to be installed. The first examples from 'Theorem proving in Lean' just work. Just making a project is not possible.

[Alex J. Best]

Perhaps lake isn't on the PATH picked up by vscode, what if you open up a separate terminal window and try there? Also try elan -v to be sure

[Sjaak Smetsers]

elan -v returns the same error (elan: command not found). There is a .elan folder in my home directory. What do I need to do to get it working? Any idea what went wrong with the installation?

[Kevin Buzzard]

Try closing your terminal and opening it again

[Sjaak Smetsers]

Jesus. Closing and then opening again works. Apparently it was too obvious. Thank you for your time.

[Kevin Buzzard]

The installation process adds things to your PATH but the current terminal doesn't update.