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

Stream: general

[Alistair Tucker]

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]

So I could link to that instead

[Scott Morrison]

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