Zulip Chat Archive

Stream: general

Topic: leanprover-community.github.io/lean3/get_started.htm

Alistair Tucker (Jun 03 2021 at 07:42):

I would like to be able to write down installation instructions for my Lean 3 project that will continue to work beyond the time when mathlib transitions to Lean 4. But I don't know whether installation of leanproject will still be the recommended route on leanprover-community.github.io/get_started.html. If there is any danger it will not, might it be an idea to make a page now called something like leanprover-community.github.io/lean3/get_started.html that won't change?

Alistair Tucker (Jun 03 2021 at 07:43):

So I could link to that instead

Scott Morrison (Jun 03 2021 at 07:48):

Oof, I think this is looking a bit far into the future. :-) I guess a PR making a lightweight redirect would be welcome.

Last updated: Dec 20 2023 at 11:08 UTC