Lean 3 create new project does not work

Stream: general

[Mattia Bottoni]

Hi everybody :)
I would like to teach students some simple mathematical proofs with Lean 3. I decided to use Lean 3 since in my opinion, it is a bit more user-friendly. The problem is that when following the instructions on https://leanprover-community.github.io/lean3/install/windows.html, none of the students were able to create a new project. Is it possible that Lean 3 is not supported anymore? Students always get the same error message: “Server has stopped with error code 1”.

Thank you for your help
Mattia

[Scott Morrison]

Lean 3 works, but it is not supported and we are strongly encouraging users to make the switch to Lean 4.

[Eric Wieser]

Having said that, you shouldn't be experiencing that error; but it is probably a better use of time to get setup with Lean 4 than debug a machine with a broken Lean 3 setup

[Utensil Song]

Maybe the banner on the page could be yellow, "deprecated" could be in bold, and "the community is migrating to Lean 4" could be "the majority of the community has migrated to Lean 4" .

[Eric Wieser]

https://github.com/leanprover-community/leanprover-community.github.io/pull/377

[Scott Morrison]

LGTM.

[Eric Wieser]

Should we go further to make it red?

[Utensil Song]

@Mattia Bottoni Just curious: can you elaborate on why is Lean 3 a bit more user-friendly in your opinion? Maybe you'll be interested in trying out https://live.lean-lang.org/ which gives you instant access to all of Mathlib4 ( with proper import) in a browser.

[Utensil Song]

Eric Wieser said:

Should we go further to make it red?

Maybe a little too much, blue is too safe and people could skip reading it, but yellow usually catches the eyes.

[Eric Wieser]

Merged as :yellow_large_square: for now, I'll let someone else make a PR if they want even stronger wording/colors

[Mattia Bottoni]

Utensil Song said:

Mattia Bottoni Just curious: can you elaborate on why is Lean 3 a bit more user-friendly in your opinion? Maybe you'll be interested in trying out https://live.lean-lang.org/ which gives you instant access to all of Mathlib4 ( with proper import) in a browser.

E.g. when you try to prove something in Lean 3 you do that between "begin" and "end", which gives that "finish your task" vibe that I like about Lean so much and the tactic import always worked better for me than importing Mathlib (import tactic works faster). Also, I like coming from the NNG to doing your own things with Lean and since NNG uses Lean 3 it is more convenient to stay in Lean 3.

[Mattia Bottoni]

Anyway, thanks to you all for clarifying! :)
I will find a way to change my exercises so that they work with Lean 4.

[Mattia Bottoni]

Scott Morrison said:

Lean 3 works, but it is not supported and we are strongly encouraging users to make the switch to Lean 4.

Could you explain what you mean by "Lean 3 works, but it is not supported"?

Do you mean that it only works when you already had it installed before?

[Michael Rothgang]

By the way, the NNG has been ported to Lean 4: https://adam.math.hhu.de/#/g/hhu-adam/NNG4.

[Eric Wieser]

"not supported" means "you will find very few people willing to provide you support, and even fewer people willing to fix any bugs in it you find"

[Eric Wieser]

"supported" as in "supported by the community", not "supported by the operating system".

[Eric Wieser]

import tactic works faster

Are you aware of import Mathlib.Tactic, which is the Lean 4 analog to import tactic?

[Mattia Bottoni]

Michael Rothgang said:

By the way, the NNG has been ported to Lean 4: https://adam.math.hhu.de/#/g/hhu-adam/NNG4.

Just saw it. Thank you :)

[Mattia Bottoni]

Eric Wieser said:

import tactic works faster

Are you aware of import Mathlib.Tactic, which is the Lean 4 analog to import tactic?

I am, but it still compiles slower somehow.

[Shreyas Srinivas]

That is strange. Have you used the mathlib cache?

[Shreyas Srinivas]

lake exe cache get

[Utensil Song]

when you try to prove something in Lean 3 you do that between "begin" and "end", which gives that "finish your task" vibe that I like about Lean so much

It's now by ... done in teaching practice.

image.png

[Utensil Song]

In case you miss :tada: vibe, here you go

[Mattia Bottoni]

Shreyas Srinivas said:

That is strange. Have you used the mathlib cache?

I have yes :). It runs faster now. Maybe the problem was that I did not use Lean 4 for some time. I am rewriting my exercises for Lean 4 right now.

[Mattia Bottoni]

Utensil Song said:

In case you miss :tada: vibe, here you go

I missed that indeed. Thank you very much!