Zulip Chat Archive

Stream: new members

Topic: command 'lean.displayGoal' not found?

AnduinHS (Aug 25 2021 at 15:56):

I am working on VS Code, after I typed my code and click the 'Info View' button, it says that "command 'lean.displayGoal' not found". I don't know if I have deleted sth.
Please forgive me for asking such a perhaps naive question.

Alex J. Best (Aug 25 2021 at 15:57):

It looks like your file is saved on your desktop, for lean and the vscode plugin to work you need to be in a proper lean project in general.

Alex J. Best (Aug 25 2021 at 15:59):

If you have a lean project you are playing around in, move your file there and then open that whole folder in vscode.

Alex J. Best (Aug 25 2021 at 16:01):

Otherwise make sure you have leanproject installed (see https://leanprover-community.github.io/install/windows.html#get-scripts) and then follow https://leanprover-community.github.io/install/project.html to make a new project somewhere

AnduinHS (Aug 26 2021 at 01:14):


Last updated: Dec 20 2023 at 11:08 UTC