Zulip Chat Archive

Stream: general

Topic: new linkifier


view this post on Zulip Mario Carneiro (Mar 20 2020 at 10:33):

I don't think this is a very big or contentious change, but as a heads-up: seeing as the leanprover/lean issues page has been dead for a long time, disappeared for a while and then came back as a zombie, I think it is appropriate that lean#42 now links to leanprover-community/lean repo, while leanprover/lean#42 links to the original repo. #42 links to mathlib as before.

view this post on Zulip Johan Commelin (Mar 20 2020 at 10:35):

lean#153 :tada: :left: Thank you Mario!

view this post on Zulip Mario Carneiro (Mar 20 2020 at 10:44):

Actually, that's needlessly specific. I just generalized it again, so that while lean#42 still links to leanprover-community/lean, you can also link to any other repo in leanprover-community like mathlib-tools#3, or any other repo on github like highlightjs/highlight.js#1689 .

view this post on Zulip Johan Commelin (Mar 20 2020 at 10:46):

Except that last one didn't work :sad:

view this post on Zulip Mario Carneiro (Mar 20 2020 at 10:46):

highlightjs/highlight.js#1689

view this post on Zulip Mario Carneiro (Mar 20 2020 at 10:46):

there we go

view this post on Zulip Mario Carneiro (Mar 20 2020 at 10:47):

I'm not sure what exactly the grammar of repo names is

view this post on Zulip Kevin Buzzard (Mar 20 2020 at 11:07):

I had no idea that we could link to anything other than mathlib :D

view this post on Zulip Kevin Buzzard (Mar 20 2020 at 11:08):

Johan Commelin said:

lean#153 :tada: :left: Thank you Mario!

153 is the smallest three-digit number which is the sum of the cubes of its digits.

view this post on Zulip Kenny Lau (Mar 20 2020 at 11:19):

I went to visit him while he was lying ill at the hospital. I had come in taxi cab number 14 and remarked that it was a rather dull number. "No" he replied, "it is a very interesting number. It's the smallest number expressible as the product of 7 and 2 in two different ways."

view this post on Zulip Johan Commelin (Mar 20 2020 at 12:12):

Kevin Buzzard said:

I had no idea that we could link to anything other than mathlib :D

I think we couldn't. Mario just now enabled some Zulip magic a couple of posts ago.

view this post on Zulip Mario Carneiro (Mar 20 2020 at 13:09):

actually we could previously link to leanprover/lean using the lean#num format


Last updated: May 13 2021 at 05:21 UTC