Installing lean

Stream: new members

[Roman Fedorov]

Dear Colleagues, I am really sorry for asking such a stupid question... So I installed lean using elan and it basically works. But some features do not. For example it does not recognize the words "obtain" "take" and "premise". Surprisingly, if I type "obtain" in VCS, it gets blue while "take" and "premise" do not. Again, I am really sorry for such stupid a question but I was trying to resolve it for two days and to no avail.

[Jalex Stark]

what is take supposed to do?

[Rob Lewis]

These keywords are from Lean 2. They've been gone for 3+ years. What documentation are you following that taught you those?

[Jalex Stark]

(also, questions like this are completely appropriate, don't wring your hands too much about it)

[Rob Lewis]

I really wish there were a way to scrub old docs off the internet :/

[Jalex Stark]

https://leanprover-community.github.io/

[Rob Lewis]

I'll make a wild guess that you're following Lean 2 TPIL, and you really want #tpil

[Kevin Buzzard]

That's the modern place to start

[Roman Fedorov]

I was using this tutorial, which I found pretty good https://leanprover.github.io/tutorial/ Is there another one?

[Gabriel Ebner]

I think the correct way to get rid of old documentation is to update it instead of producing new tutorials every year.

[Kevin Buzzard]

Please read the warning right at the beginning of what you linked to @Roman Fedorov

[Kevin Buzzard]

actually, don't even read that, look at the link which Jalex posted :D

[Kevin Buzzard]

and the link which Rob posted

[Kevin Buzzard]

In short, the active community here uses a fork of Lean 3, which is actively maintained and updated; the links coming from Microsoft and the official Lean pages are all frozen and out of date because they are working on Lean 4, which still doesn't have a release.

[Roman Fedorov]

Ok, thanks! I was sure something was wrong with my installation, but obviously you are all right
.

[Yury G. Kudryashov]

The "upstream" Lean 3.x is unmaintained (together with its documentation). There is a community fork with community docs but upstream website doesn't redirect users to the community website.

[Michael]

Hello! I'm required to following this tutorial on lean https://leanprover.github.io/logic_and_proof/propositional_logic_in_lean.html#expressions-for-propositions-and-proofs and I'm trying to install lean on vscode but it shows an error "expected command" no matter what I type. I followed the installation instructions on leans github and installed the lean and lean4 extensions on vscode. Anyone know why this is happening? Am I installing the wrong version?

[Matt Diamond]

I could be wrong but I believe that tutorial is for Lean 3, not Lean 4... which version of Lean did you install?

[Alex J. Best]

Its probably best to disable the extension that isn't corresponding to the lean version you are trying to use, too.

[Michael]

hi, thanks for the reply! I installed both the lean and lean4 vscode extensions as well as all the requirements from the installation guide and when I tried disabling the lean4 extension like Alex has suggested, the lean server was not able to start for some reason. It's giving me this error:

----- user triggered restart -----
Watchdog error: Cannot read LSP request: A Lean 3 request was received. Please ensure that your editor has a Lean 4 compatible extension installed. For VSCode, this is

    https://github.com/leanprover/vscode-lean4

Any ideas on why this could be happening?

[Matt Diamond]

it's likely that you installed Lean 3 along with the Lean4 VSCode extension, which is why the VSCode extension is complaining about getting a Lean 3 request

[Matt Diamond]

if you want to go with Lean 3, you'll need to uninstall the Lean 4 extension and install the Lean 3 one

alternatively, you could uninstall Lean 3 and install Lean 4

[Kevin Buzzard]

I'm not so sure about this. The Lean 3 and Lean 4 extensions used to not play well with each other but I seem to have them both installed on this computer and things are fine. Michael, do you have Lean 3 installed on your computer following the instructions here https://leanprover-community.github.io/get_started.html ? And have you got a Lean 3 project open in VS Code?

[Michael]

Yeah I have them both installed as well but I figured out that the problem wasn't the wrong version but it's because I did not create a lean3 project correctly and I managed to get it working after following the instructions to create a project. Thank you so much to everyone that helped!