new linkifier

Stream: general

[Mario Carneiro]

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.

[Johan Commelin]

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

[Mario Carneiro]

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 .

[Johan Commelin]

Except that last one didn't work :sad:

[Mario Carneiro]

highlightjs/highlight.js#1689

[Mario Carneiro]

there we go

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Kenny Lau]

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

[Johan Commelin]

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.

[Mario Carneiro]

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