Zulip Chat Archive

Stream: general

Topic: lean home page still pointing to gitter


view this post on Zulip Kevin Buzzard (Oct 10 2018 at 06:11):

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).

view this post on Zulip Scott Morrison (Oct 10 2018 at 06:13):

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

view this post on Zulip Kevin Buzzard (Oct 10 2018 at 06:15):

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.

view this post on Zulip Mario Carneiro (Oct 10 2018 at 06:17):

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

view this post on Zulip Kevin Buzzard (Oct 10 2018 at 06:17):

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

view this post on Zulip Mario Carneiro (Oct 10 2018 at 06:18):

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

view this post on Zulip Kevin Buzzard (Oct 10 2018 at 06:36):

"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)

view this post on Zulip Kevin Buzzard (Oct 10 2018 at 06:37):

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

view this post on Zulip Kevin Buzzard (Oct 10 2018 at 06:39):

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

view this post on Zulip Jeremy Avigad (Oct 10 2018 at 15:16):

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

view this post on Zulip Sebastian Ullrich (Oct 10 2018 at 15:46):

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

view this post on Zulip Kevin Buzzard (Oct 10 2018 at 20:21):

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

view this post on Zulip Sebastian Ullrich (Oct 10 2018 at 20:27):

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

view this post on Zulip Kevin Buzzard (Oct 10 2018 at 20:37):

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

view this post on Zulip Sebastian Ullrich (Oct 10 2018 at 20:44):

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

view this post on Zulip Patrick Massot (Oct 10 2018 at 20:55):

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."

view this post on Zulip Sebastian Ullrich (Oct 10 2018 at 21:00):

Oh. Yes.

view this post on Zulip Patrick Massot (Oct 10 2018 at 21:07):

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

view this post on Zulip Kevin Buzzard (Oct 10 2018 at 21:14):

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.


Last updated: May 17 2021 at 21:12 UTC