Installing lean 3 issues

Stream: new members

[Nagwa]

Screenshot-2023-10-09-at-18.17.42.png
Hey, I know that it says that I need to install lean 4 but I do not want it I want lean 3, how can I delete elan for lean 4?

[Kevin Buzzard]

That question doesn't make sense: elan is an all-purpose "I install whichever version of Lean is necessary" tool, it is not specific to lean 3 or lean 4. And you are asking your question in an incorrect thread: can you please start a new thread in e.g. #new members ?

[Nagwa]

oh sorry

[Patrick Massot]

We really need to find who is asking students to install Lean 3 in October 2023. This makes no sense at all.

[Nagwa]

I KNOW!!!!

[Nagwa]

I have got this professor and he insists on install lean 3

[Kevin Buzzard]

please name and shame them here

[Patrick Massot]

Kevin means we would be happy to help that person migrate to Lean 4.

[Nagwa]

Screenshot-2023-10-09-at-18.17.42.png
I want to install lean 3 but I think I have installed lean 4 not in vs code but in my terminal how can I get rid of it?

[Kevin Buzzard]

I think that what is happening here is that you have just got a random Lean file in a random directory and not in a Lean project, so Lean has absolutely no idea which version of Lean to use, so it uses the "active toolchain" version, which you can see with elan default

[Kevin Buzzard]

The easiest way to continue would just be to make a correctly-formatted Lean project rather than just a standalone file, and then elan will know which version of lean to use by looking at the relevant config file in the project.

[Nagwa]

all I'm saying here is that he's a German professor and likes to make students suffer

[Kevin Buzzard]

If your professor is insisting on using Lean 3 then I assume they have made a Lean 3 course repository, which you can just clone. Then put your test files in there and things should work fine.

[Kevin Buzzard]

If they have not even made a Lean 3 course repository then you should tell your professor that you can't do that yourself because you don't know how and all the instructions have changed to this new-fangled lean 4 thing, so could you use Lean 4 instead?

[Nagwa]

Screenshot-2023-10-09-at-18.38.08.png

[Nagwa]

I think I might ask him that, but let me just try

[Kevin Buzzard]

Re the Lean 3 choice: surprisingly, Lean 4 can also do proofs in logic.

[Kevin Buzzard]

What is the link he gave you for Lean 3 (in your screenshot in the incorrect thread)? We could break that before you ask.

[Nagwa]

Screenshot-2023-10-09-at-18.41.33.png
help :sob:

[Ruben Van de Velde]

(did we not just land new code into mathlib 3 in the last hour?)

[Nagwa]

Kevin Buzzard said:

What is the link he gave you for Lean 3 (in your screenshot in the incorrect thread)? We could break that before you ask.

okay wait

[Nagwa]

Screenshot-2023-10-09-at-18.45.54.png

[Kevin Buzzard]

I don't really remember -- perhaps Lean 4 supports people using single .lean files not in a correctly set-up package, but Lean 3 did not? It's been a year since I last touched Lean 3. If I'm right you'll have to make a correctly-formatted Lean 3 project if you want to use Lean 3. The leanpkg.toml file is the config file which says precisely which version of Lean 3 you will be using

[Nagwa]

https://lean-lang.org/download/

[Nagwa]

Screenshot-2023-10-09-at-18.47.42.png
Then I git clone it

[Kevin Buzzard]

The question I meant to ask was: what is the URL of the link that you screenshotted in the bad thread: "All the information about Lean 3 you find <here>"?

[Kevin Buzzard]

You don't clone Lean. elan does that job for you.

[Kevin Buzzard]

I mean you clone a Lean 3 project such as https://github.com/leanprover-community/lean-liquid . And then you just delete all the files in src and put your own files in there.

[Nagwa]

Oh makes sense, but do I have to copy the http or ssh?

[Kevin Buzzard]

But probably even that won't work because you'll need all the lean 3 community tooling. Just tell your professor that you spent 3 hours trying to get Lean 3 to work and you couldn't and all the instructions on how to make it work have been removed and nobody on the Zulip would help because they have all forgotten how to make Lean 3 work because it's end of life, and so you're going to submit answers in Lean 4

[Nagwa]

Sorry if I'm making stupid questions but it really is confusing

[Patrick Massot]

Nagwa said:

all I'm saying here is that he's a German professor and likes to make students suffer

You'd be surprised by how few professors actually like to make student suffer. It is much more probable that this person does not use Lean everyday but wanted students to benefit from it anyway so he invested a lot of time learning Lean 3, maybe only half a year ago, and simply doesn't have time to learn a new version. That's why we could help.

[Kevin Buzzard]

If the URL points to something on the community website then we could just update it to Lean 4 because this is a job which needs to be done anyway. If it's a local link then just follow the instructions there.

[Yaël Dillies]

I think I know who the lecturer is :grinning: