Lean 3 vs Lean 4 in outward-facing materials

Stream: general

[Johan Commelin]

We need to work on SEO. If you search the internet for "Natural Number Game" then you'll find the Lean 3 version.

[Johan Commelin]

If we think the Lean 4 version is ready for mass consumption (contentwise, and performancewise), then maybe Kevin can use some html-magic to add a pointer to the Lean 4 version.

[Gabor Nyeki]

Johan Commelin said:

If we think the Lean 4 version is ready for mass consumption (contentwise, and performancewise), then maybe Kevin can use some html-magic to add a pointer to the Lean 4 version.

If Lean 3 is officially deprecated in favor of Lean 4, it would be a good idea to indicate that throughout in Lean 3's online documentation, books, GitHub repos, and the natural number game.

[Patrick Massot]

Gabor, we already try to do that. Please don't hesitate to point out resources that do not comply.

[Mauricio Collares]

The Natural Number Game 3 does not point to a Lean 4 version, perhaps because the Lean 4 version is being updated?

[Kevin Buzzard]

I am holding off pointing the lean 3 version to the lean 4 version until the lean 4 version is at feature parity with the lean 3 version. I finished advanced addition world today, am working on inequality world, and then the only thing left is advanced multiplication world which is just 4 levels (but which in NNG4 will be used as preparation for divisibility world, one of the new worlds). I am hoping for feature parity by the time I start using the NNG in my course; my first lecture is 16th Oct.

[Kevin Buzzard]

The other reason I'm holding off is that I don't have a clue how to edit the Lean 3 web pages ;-)

[Gabor Nyeki]

Patrick Massot said:

Gabor, we already try to do that. Please don't hesitate to point out resources that do not comply.

The tutorials repo linked by MithicSpirit on Mathstodon does not mention that Lean 3 is deprecated but I think it would be good if it did and linked to the tutorials4 repo: https://github.com/leanprover-community/tutorials

[Patrick Massot]

Thanks Gabor, I fixed this one.

[Patrick Massot]

Kevin, don't hesitate to ask for help when you'll be ready to officially deprecate NNG3.

[Andrew Yang]

Maybe the mathlib repo itself should contain such a warning as well?

[Patrick Massot]

Good catch.

[Julian Berman]

Patrick are you intentionally not archiving the repo as well, or perhaps should that be considered?

[Patrick Massot]

Could you remind me what is gained from archiving? No more issues/PR?

[Julian Berman]

Yes, and also the message gets placed also in a banner at the top of the page so it can be slightly more obvious

[Patrick Massot]

Ok, I did it.