install lean3 on windows

Stream: new members

[Shufan Xia]

Hello community, new to Lean, want to install and run lean3 on a windows machine. I followed the steps from this link https://leanprover-community.github.io/lean3/install/windows.html , but could not get it work in my VS code. The VS output window says "Watchdog error: Cannot read LSP request: A Lean 3 request was received. Please ensure that your editor has a Lean 4 compatible extension installed." I understand lean3 is obsolete but still need it. Could someone help me with getting lean3 running? Thanks a lot.
image.png

[Ruben Van de Velde]

Do you have a particular reason to install lean 3 rather than 4? 3 is no longer supported

[Matt Diamond]

assuming you actually need Lean 3, it's possible that you installed the wrong extension on VSCode

[Matt Diamond]

or maybe the mismatch is the other way around, where the extension is Lean 3 but for some reason your project is Lean 4... do you have Lean 4 installed as well?

[Matt Diamond]

actually I see this in your screenshot, which suggests it's just the wrong extension:
image.png

[Shufan Xia]

Ruben Van de Velde said:

Do you have a particular reason to install lean 3 rather than 4? 3 is no longer supported

want to try this https://github.com/jesse-michael-han/lean-gptf/tree/master. The author says it only supports lean3

[Shufan Xia]

Matt Diamond said:

actually I see this in your screenshot, which suggests it's just the wrong extension:
image.png

I don't have lean4 installed yet.
image.png
image.png

[Shufan Xia]

Matt Diamond said:

or maybe the mismatch is the other way around, where the extension is Lean 3 but for some reason your project is Lean 4... do you have Lean 4 installed as well?

how do I set which lean version being used for a project?

[Matt Diamond]

I see. Did you try creating a new Lean 3 project and opening the folder for that project in VSCode? I see you've opened a single file in your Documents folder but I believe you need to create a project.

[Patrick Massot]

Shufan Xia said:

want to try this https://github.com/jesse-michael-han/lean-gptf/tree/master. The author says it only supports lean3

I think this experiment is fully dead. Even if you manage to install the corresponding obsolete version of Lean then it will try to talk to a server that has been shut down a long time ago.

[Shufan Xia]

Matt Diamond said:

I see. Did you try creating a new Lean 3 project and opening the folder for that project in VSCode? I see you've opened a single file in your Documents folder but I believe you need to create a project.

that makes sense. Tried to follow the instruction on 'creating a lean project' from here https://leanprover-community.github.io/lean3/install/project.html. Got "bash: leanproject: command not found". I did try this already " type source ~/.profile or source ~/.bash_profile.". How could I make my git bash recognize lean command? Thanks again

[Patrick Massot]

Modern incarnations of this idea can be found at https://github.com/lean-dojo/LeanCopilot and https://github.com/wellecks/llmstep.

[Patrick Massot]

I should also say that it is very unlikely you will benefit from those IA tools if you never used Lean in the regular way.

[Shufan Xia]

Patrick Massot said:

Modern incarnations of this idea can be found at https://github.com/lean-dojo/LeanCopilot and https://github.com/wellecks/llmstep.

Thank you for this helpful recommendation.

[Patrick Massot]

So you should probably install Lean 4 and follow some tutorial to learn the basics and then turn to either LeanCopilot or LLMStep.

[Patrick Massot]

There are instructions on https://leanprover-community.github.io/. Also note there is a Zulip stream devoted to AI and Lean at https://leanprover.zulipchat.com/#narrow/stream/219941-Machine-Learning-for-Theorem-Proving

[Shufan Xia]

I see. Thank you for your advice. Will give it a try.