Issue with Lean 3 in VScode

Stream: general

[Oliver Hayman]

I recently set up Lean 3 with VScode, but whenever I create a new file I get the following error:

image.png

I had previously added Lean 4 to VScode, and this error appears only if the Lean 4 extension is disabled. Otherwise I can make Lean 3 files, but they end up being in Lean 4 and not Lean 3, even if I specify that the language I want to use is Lean 3.

Does anyone know what is going on? Haven't found answers to this anywhere.

[Gabriel Ebner]

Have you installed both the Lean 3 & Lean 4 extensions?

[Oliver Hayman]

Yes. Currently Lean 4 is not enabled.

[Gabriel Ebner]

All right. Looking at the screenshot, the Lean 3 extension is activated but Lean 4 is running.

[Gabriel Ebner]

What do you get when you run lean --version in that directory on the command-line?

[Oliver Hayman]

4.0.0. How do I change this?

I've installed lean 3 as well as lean 4.

[Kevin Buzzard]

Is the directory you're running that code in a correctly formatted lean 3 project? Lean only works within a project.

[Oliver Hayman]

Yes, this was this issue. I was able to work with individual files for lean 4 so I assumed I could do the same for lean 3.

[Oliver Hayman]

Thanks!