Zulip Chat Archive

Stream: general

Topic: Issue with Lean 3 in VScode


Oliver Hayman (Sep 28 2022 at 22:06):

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 (Sep 28 2022 at 22:48):

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

Oliver Hayman (Sep 28 2022 at 23:05):

Yes. Currently Lean 4 is not enabled.

Gabriel Ebner (Sep 28 2022 at 23:28):

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

Gabriel Ebner (Sep 28 2022 at 23:28):

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

Oliver Hayman (Sep 29 2022 at 02:43):

4.0.0. How do I change this?

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

Kevin Buzzard (Sep 29 2022 at 06:31):

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

Oliver Hayman (Sep 29 2022 at 09:13):

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 (Sep 29 2022 at 09:13):

Thanks!


Last updated: Dec 20 2023 at 11:08 UTC