command 'lean.displayGoal' not found?

Stream: new members

[AnduinHS]

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.
1.PNG
Please forgive me for asking such a perhaps naive question.

[Alex J. Best]

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]

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]

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]

Thanks!