Goal not showing

Stream: new members

[One An]

Hello everyone, it seems like regardless of what I put on vscode, the goal in tactic mode doesn't show up. Can anyone help with this? Thanks!
image.png

[Damiano Testa]

I think the file should exist and be called something.lean

[Damiano Testa]

Does this help?

[One An]

Sorry, what do you mean? Could you clarify?

[Yaël Dillies]

Lean only runs on .lean files. Your file is currently untitled.

[One An]

image.png
i named it .lean but it still doesn't show up

[Yaël Dillies]

Try Lean: Restart server from the command palette

[One An]

image.png

[One An]

it gives an error code, is this normal?

[Yaël Dillies]

Hmm, no that's unusual.

[Damiano Testa]

It is not normal, I do not know why you get the error, but Lean will also not like the /r, once you fix the rest.

[Kyle Miller]

Yeah, you need to set up a lean project: https://leanprover-community.github.io/install/project.html

[One An]

Go to a folder where you want to create a project in a subfolder my_project, and type leanproject new my_project. If you get an error message saying leanproject is an unknown command and you have not logged in since you installed Lean and mathlib, then you may need to first type source ~/.profile or source ~/.bash_profile.

[One An]

Could you explain what this part means?

[One An]

What command do i have to exactly run on git bash?

[Kyle Miller]

If you do leanproject new my_project in bash it should create a new folder my_project containing all the files you need for VS Code to recognize the folder as being a Lean project

[One An]

image.png
is this an error, this is what git bash returns

[Kyle Miller]

Hm, I'm not sure what happened to new, but could you try mkdir my_project then cd my_project and then leanproject init my_project?

[One An]

image.png
this is what it returns

[Kevin Buzzard]

What does leanproject --version return?

[One An]

1.3.2

[One An]

is that the wrong version?

[One An]

should i be using lean 3 or 4?

[Kevin Buzzard]

Leanproject is for lean 3

[One An]

The lean 3 extension doesn't work for me while lean 4 does work. Is that because I don't have lean project?

[Kevin Buzzard]

Nothing will work unless you have a Lean project set up, and the first step in doing that is deciding whether you are using Lean 3 or Lean 4. Once you have decided that, then follow the instructions for installing the language, and then follow the instructions for making a Lean project in that language, and finally then open the root directory of the project using VS Code's "open folder" functionality, and then ask again if it isn't working.

[Kyle Miller]

Based on the screenshots, it seems like there's something wrong with your leanpkg command. It might be worth uninstalling Lean and starting from scratch, following the instructions on the website carefully. https://leanprover-community.github.io/install/windows.html