Zulip Chat Archive

Stream: new members

Topic: lake: command not found

Sjaak Smetsers (Jul 05 2022 at 17:03):

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 (Jul 05 2022 at 17:06):

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 (Jul 05 2022 at 17:10):

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 (Jul 05 2022 at 17:13):

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 (Jul 05 2022 at 17:19):

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 (Jul 05 2022 at 17:21):

Try closing your terminal and opening it again

Sjaak Smetsers (Jul 05 2022 at 17:24):

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

Kevin Buzzard (Jul 05 2022 at 17:38):

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

Last updated: Dec 20 2023 at 11:08 UTC