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:

[Linski]

Patrick Massot said:

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

Lean 3 is way easier for non-programmer students to pick up imo.

[Mark Fischer]

That's surprising to me. I saw news about Lean 4's release and then got into it so I never used Lean 3. From the examples I've run across though it seems pretty similar.

Especially with how extensible Lean 4 is, there may be ways to make Lean 4 at least close to Lean 3 for non-programmer students. What are some of the sticking points, I wonder?

[Ruben Van de Velde]

I'm not sure that's true, fwiw

[Jordi Navarrette]

Mark Fischer said:

That's surprising to me. I saw news about Lean 4's release and then got into it so I never used Lean 3. From the examples I've run across though it seems pretty similar.

Especially with how extensible Lean 4 is, there may be ways to make Lean 4 at least close to Lean 3 for non-programmer students. What are some of the sticking points, I wonder?

I may make myself persona no grata here, but I'll give this a stab: The sticking points are FIRST IMPRESSIONS. Linski indicates "non-programmers": who among such would have "saw news of Lean 4's release and then got into it"? Just do a side by side of "Theorem Proving in Lean" for the two versions, anyone who's not a dedicated math or cs major/enthusiast is going to be turned off by 4, while at least give 3 a chance because of the initial resemblance to what is seen in philosophy or lower math. As such, what good is extensibility?

I could get on fine with 4, and I'm sure your hardcore lot could care less, but I'm trying to expose and convert those who are not even aware of formal methods as a field - students who are quite bright - to see the power and promise of this area. To that end, the abandonment of Lean 3 support is a great disappointment, as I was really hoping to be able to get my students through Avigad et al's Logic and Proof this September. I guess I'll be changing plans.

[Kevin Buzzard]

I think the correct thing to do is to get the students to port Logic and Proof to Lean 4 :-)

[Ruben Van de Velde]

Is there anything specific about lean 4 that you think is worse than lean 3 for "anyone who's not a dedicated math or cs major/enthusiast"?

[Eric Wieser]

It sounds like the complaint is "the target audience of TPIL changed", not anything about the language itself

[Jeremy Avigad]

@Joseph Hua has been porting Logic and Proof to Lean 4, though I don't know whether it is ready for use. The Lean 3 version can still be run online, in a browser.

Logic and Proof has students writing proof terms instead of tactic proofs, which has the advantage of highlighting the logical structure of a proof. But it is hard to get the syntax right and that causes problems for students. If I were to do it again, I would use tactic proofs exclusively; structuring tactics like have and show serve the same purpose, and they are more robust and give students more feedback. I think Joseph is taking steps in that direction.

There are lots of other good teaching materials based on Lean 4.

[Mark Fischer]

Jordi Navarrette said:

As such, what good is extensibility?

Lean 4's macro system is pretty amazing. Users have access to the same mechanisms and API used to parse and process all of Lean's builtin syntax.

I think it would let you write your own Domain Specific Language with your desired initial resemblance to what is seen in philosophy or lower math. For a first impression, you can probably hide a lot of lean's complexity. I've wondered what it would look like to craft a gentle introduction to formalization in this way. Even if it just makes for improved error messages based on the fact that the author understands exactly what the student is attempting to accomplish. If really polished, I could imagine teaching high-school students some of this stuff in an interactive, iterative feedback environment. Sounds cool.

It seems like there would be at least 2 big downsides:

1. It's also not clear how hard it would be to maintain such a project as Lean isn't that stable yet. It would probably be a lot of work for an uncertain amount of benefit. It's often trial by fire that shows what helps and what doesn't.
2. As students move beyond the DSL, they'd face some confusion about what changes and what stays the same. For example, the Natural Numbers Game changes a few tactics a bit and has a different definition for the ≤ operator. I think they are good choices, but once in a while you'll see a question here that gets asked as a direct result of not realizing this.

[Jordi Navarrette]

To be brief, I would propose that Logic and Proof + Lean 3 were the gentle introduction, but right now the browser version seems broken and doesn't handle the chapters 1 and >10 examples. If the port is not ready, I'll get to work on it myself, and see if it's worth it. To address the other feedback (and, I thank you all for that), I really had plans to work on other things, but I'll get back to you.

[joseph hua]

Jeremy Avigad said:

Joseph Hua has been porting Logic and Proof to Lean 4, though I don't know whether it is ready for use. The Lean 3 version can still be run online, in a browser.

Logic and Proof has students writing proof terms instead of tactic proofs, which has the advantage of highlighting the logical structure of a proof. But it is hard to get the syntax right and that causes problems for students. If I were to do it again, I would use tactic proofs exclusively; structuring tactics like have and show serve the same purpose, and they are more robust and give students more feedback. I think Joseph is taking steps in that direction.

There are lots of other good teaching materials based on Lean 4.

Here is a link to the lean 4 version and the github repo. I tried to use both term mode and tactic mode, but this might have been a little too ambitious.