Errors installing Lean4 / starting new project

Stream: lean4

[Daniel Donnelly]

image.png

What do I do to start from scratch?

[Daniel Donnelly]

I tried uninstalling / then installing Lean4 extension, and same issue happening.

[Daniel Donnelly]

My goal is to learn some of the Lean4 syntax, specifically in regards to HomAlg

[Kevin Buzzard]

It looks to me like you've opened Lean 4 itself. By HomAlg do you mean homological algebra? In which case (a) this question needs to be moved to #mathlib4 as it's not about Lean itself and (b) you need to create a new project with mathlib as a dependency following the instructions here for example.

Apologies if I've misunderstood and you actually want to hack Lean 4 itself rather than doing mathematics.

[Daniel Donnelly]

@Kevin Buzzard I just named the folder Lean4

[Marc Huisinga]

Daniel Donnelly said:

image.png

What do I do to start from scratch?

What other VS Code extensions do you have installed?

[Daniel Donnelly]

Okay, this fixed itself. I went to "Forall" in the menu bar, then to Document Guide > ... Create a Standalone Lean4 project, selected folder, then waited this time, and everything works now:

image.png

[Marc Huisinga]

I don't think that this issue will simply permanently fix itself. What other VS Code extensions do you have installed?

[Daniel Donnelly]

@Marc Huisinga None, the problem fixed itself. Perhaps because I didn't wait before closing VSCode last time

[Marc Huisinga]

I'm asking because this issue occurs when you have multiple extensions installed that contribute the same command (in this case the 'Restart File' one), e.g. the Lean 4 extension and some fork of the Lean 4 extension.

[Marc Huisinga]

If this isn't what happened here, then it would be really good to know so that we can fix it.

[Marc Huisinga]

(It's also worth noting that your screenshot shows that you do have other extensions installed, e.g. a Nim extension)