lean home page still pointing to gitter

Stream: general

[Kevin Buzzard]

I occasionally notice that Lean's web pages still point to gitter, and we occasionally get questions there; perhaps the signage isn't good enough for everyone. How could we go about changing this? I could make a PR but someone will have to point me to the location of the git source for those pages (not least so I can check the PR is not already made).

[Scott Morrison]

I think we just run into the general problem that PRs here risk annoying Leo.

[Kevin Buzzard]

I know, but on this particular occasion I am personally prepared to take the risk. I have been extremely good at not annoying Leo recently -- a few months ago I was desperate to email him to tell him 100 things and Tom Hales just basically went "No. No. No. No. No. Leave him alone." This is a one-line PR to fix something which is broken and the review process is trivial.

[Mario Carneiro]

are you saying you need us to say "no no no"?

[Kevin Buzzard]

If you're not going to tell me how to do it I'm going to go rogue and figure it out myself.

[Mario Carneiro]

I guess I don't know if the website is also defunct or just the tool

[Kevin Buzzard]

"Small bug fixes (few lines of code) are always welcome.". From the docs (which I'm currently reading -- I'm trying to put together an "installation options overview" page)

[Kevin Buzzard]

"Bug reports are always welcome, but nitpicking issues are not". Hmm.

[Kevin Buzzard]

But I've now found two links to Zulip in the Lean docs / GH pages, and one link to gitter.

[Jeremy Avigad]

I think @Sebastian Ullrich has permissions to the relevant repo.

[Sebastian Ullrich]

Unfortunately I don't. If someone could open a PR with some new wording (is it still a "public" "chat room"?), I'll talk to Leo

[Kevin Buzzard]

I would do this but I don't know the URL of the repo.

[Sebastian Ullrich]

@Kevin Buzzard https://github.com/leanprover/leanprover.github.io/blob/master/documentation/index.md. You should be able to edit it right on Github.

[Kevin Buzzard]

https://github.com/leanprover/leanprover.github.io/pull/75

[Sebastian Ullrich]

(Okay, now I have write access. Thanks for the PR.)

[Patrick Massot]

Sebastian, are you willing to get other PR to that repo? Like one about the sentence "The current version of Lean is Lean 3, and is under active development."

[Sebastian Ullrich]

Oh. Yes.

[Patrick Massot]

https://github.com/leanprover/leanprover.github.io/pull/76

[Kevin Buzzard]

Good catch Patrick. As you all know I've been pushing for more users in the maths community recently, and it's good to get the docs right. I don't care that Lean 4 is coming and there might be some chaos -- mathematicians need a lot of training in general and the sooner they start the better. In fact in some sense now we have a stable Lean it's quite a good time for new users to appear.