PhysLean linkifier broken

Stream: Zulip meta

[Joscha Mennicken]

The PhysLean#123 linkifier is linking to https://github.com/leanprover-community/PhysLean/pull/123 (which does not exist) instead of https://github.com/HEPLean/PhysLean/pull/123.

[Yaël Dillies]

In fact blahblahblah#123 links to (https://github.com/leanprover-community/blahblahblah/pull/123 for most values of blahblahblah. It's not so much that the linkifier is broken, rather than it doesn't exist!

[Joscha Mennicken]

I see, that makes sense. I didn't expect a linkifier this general :D (and I didn't check the list of linkifiers before making this post)

In that case, a custom PhysLean linkifier might be useful.

[Joscha Mennicken]

Looking through the list of linkifiers, HEPLean/PhysLean#123 already works, but requires you to type HEPLean/ every time.

[Yaël Dillies]

I too am also slightly annoyed that I need to type YaelDillies/LeanAPAP#8 every time, but unfortunately the linkifier is already taken for the docs instead: LeanAPAP#conv

[Joscha Mennicken]

Could you not have two linkifiers, one that matches on LeanAPAP#<number> for PRs and one that matches on LeanAPAP#<one non-digit character><arbitrary characters> for the docs?

[Yaël Dillies]

That's a good idea!

[Kim Morrison]

I am happy to set up xyz#123 linkifiers on request, or to install more complicated linkifiers if provided with candidate regexes.

[Joscha Mennicken]

These should work (tested with https://regex101.com/ set to "Golang", which uses the same regex engine that zulip does according to the docs, namely Google's re2):

• LeanAPAP#(?P<id>[0-9]+) → https://github.com/YaelDillies/LeanAPAP/pull/{id}
• LeanAPAP#(?P<decl>[a-zA-Z_'-](?:[\w_.'-]*[\w_'-])?) → https://yaeldillies.github.io/LeanAPAP/docs/find/?pattern={decl}#doc
• PhysLean#(?P<id>[0-9]+) → https://github.com/HEPLean/PhysLean/pull/{id}

[Yaël Dillies]

And could we please the same two for YaelDillies/Toric ?

[Joscha Mennicken]

That should be

• Toric#(?P<id>[0-9]+) → https://github.com/YaelDillies/Toric/pull/{id}
• Toric#(?P<decl>[a-zA-Z_'-](?:[\w_.'-]*[\w_'-])?) → https://yaeldillies.github.io/Toric/docs/find/?pattern={decl}#doc

[Bryan Gin-ge Chen]

Test:

• LeanAPAP#8
• LeanAPAP#conv
• PhysLean#123
• Toric#123
• Toric#conv

[Joscha Mennicken]

I suspect the specific linkifiers must come before the general ones in the linkifier list.

[Bryan Gin-ge Chen]

Yeah, it's a bit slow to drag them through the list. Should work now: PhysLean#123

[Violeta Hernández]

Kim Morrison said:

I am happy to set up xyz#123 linkifiers on request, or to install more complicated linkifiers if provided with candidate regexes.

Hi! Think we could get a CGT#123 linkifier for vihdzp/combinatorial-games?

[Bryan Gin-ge Chen]

test: CGT#123

[Kevin Buzzard]

and indeed we discover that they have PRs about surreal birthdays

[Kevin Buzzard]

My 50th was a pretty surreal birthday -- I got Real.pi as a present.

[Aaron Liu]

Kevin Buzzard said:

and indeed we discover that they have PRs about surreal birthdays

that PR was tricky since I couldn't find any reference to it anywhere online

[Aaron Liu]

I had to prove it myself and it took like a week