Linkifiers

Stream: Zulip meta

[Adam Topaz]

Can we add zulip linkifiers for the arxiv, nlab and stacks project?
Something approximately like this?
arxiv#(?P<id>[a-z0-9\./]+) https://arxiv.org/abs/%(id)s
nlab#(?P<id>[^\s]+) https://ncatlab.org/nlab/show/%(id)s
stacks#(?P<id>[0-9A-Z]+) https://stacks.math.columbia.edu/tag/%(id)s
I don't really know how to use regex, so the above might require modification...

[Scott Morrison]

arxiv#1510.08836

[Scott Morrison]

nlab#stratified+space

[Scott Morrison]

stacks#01II

[Adam Topaz]

:smile:

[Adam Topaz]

Just testing: arxiv#math/0502016

[Adam Topaz]

Cool! It works with the old-school arxiv links too :)

[Scott Morrison]

I added a - to the regex pattern so you can even link to old gr-qc papers: arxiv#gr-qc/9902017

[Adam Topaz]

Seems like something broke :frown:

arxiv#2011.01620

[Matthew Ballard]

It looks like there is an unescaped / in the regex expression for the arxiv linkifier.

[Mario Carneiro]

I think the issue is actually the escaped .. Testing: arxiv#2011.01620

[James Gallicchio]

Could we get lake#issue special cased to leanprover/lake? :)

[Mario Carneiro]

testing: lake#124

[Mario Carneiro]

sorry, I tried everything I could and the linkifier gods aren't in my favor

[Mario Carneiro]

no defined linkifier order + no negative lookahead makes it really hard to do overlapping patterns effectively :(

[James Gallicchio]

no worries. ooc what is the reason to have the default linkifier?

[Mario Carneiro]

what do you mean? We use leanprover-community as the default org if you don't give a full path like zulip/zulip#123

[James Gallicchio]

... oh wow, there are far more leanprover-community repositories than i thought :face_with_spiral_eyes: I had assumed we could have a bunch of individual special cases and no default organization

[Scott Morrison]

Testing mathlib3 linkifiers before switching over the "unversioned" ones to Lean 4: !3#19208 file3#logic/equiv/array docs3#simple_graph src3#real.pi

[Filippo A. E. Nuccio]

Along this, I was wondering when we plan (if we plan...) to create a lean3 or mathlib3 stream and let the normal ones be automatically intended to be for Lean 4. Because now both lean4 and mathlib4 receive loads of messages that are somewhat unsorted.

[Patrick Massot]

Very soon there will no longer be any discussion at all about Lean 3.

[Filippo A. E. Nuccio]

Well, this might be a bit too much, given that there is material about Lean3 around... leaving some room for those who might have questions would look reasonable to me.

[Eric Wieser]

It could be folded into a room about mathport too; optimistically all the remaining lean3 questions will be "help me port my project"

[Eric Wieser]

And it makes sense to keep those out of the main streams, since if we're lucky the next 100 users we on-board will have never touched lean3 at all

[Scott Morrison]

I think we could just leave the mathlib4 stream in place: it's no longer mostly about porting, but all discussion around contributing to mathlib. Similarly we leave lean4 in place: it's for all discussion about the language but where mathlib isn't relevant.

We'd then add a presumably low-and-decreasing traffic lean3 stream for stragglers, and possible a specific one for mathport, but I'm guessing we can just keep that in lean3.

[Filippo A. E. Nuccio]

Well, but isn't it a pity that the old (and sound, IMHO) streams "general&maths&is_there_a_code_for_X&new_members" are now mostly used for lean3? Why don't reshaping the streams in a way that reflects more the way the community is working? We could have the above-mentioned ones (but dedicated to lean4) plus perhaps a porting one; and then two decreasing streams lean3&mathlib3, whose existence would help newcomers (or oldcomers who are still interested in those things) to understand where to post their questions.

[Scott Morrison]

I'm confused. general, maths, is there code for X, and new members can still exist just as they are, and quite naturally in a month or two there won't be much discussion of lean3?

[Scott Morrison]

mathlib4 and lean4 are intended to be additions to, not replacing, those.

[Filippo A. E. Nuccio]

I see, my only point was that seeing these two streams I felt that the other were "by default" restricted to lean3. At any rate, I do not want to make a fuss, things are most probably fine as they are.

[Floris van Doorn]

I think we can rename mathlib4 to mathlib in 1-3 months (this does not change the topic of discussion)

[Eric Wieser]

Or is it worth renaming it to mathlib-porting, since the majority of it is porting discussions?

[Filippo A. E. Nuccio]

Yes, this seems a very good idea to me.

[Eric Wieser]

Does renaming a stream break existing links to it?

[Eric Wieser]

There are a lot of porting commits that link to Zulip threads, breaking all those links would be rather annoying

[Sebastian Ullrich]

https://leanprover.zulipchat.com/#narrow/stream/236604-the-stream-name-is-meaningless/topic/Linkifiers

[Alex J. Best]

Should we also update the branch#blah linkifier?

[Scott Morrison]

@Alex J. Best I think it's already been updated?

[Mauricio Collares]

Checking if #bors was updated too (I think not?)

[Alex J. Best]

Scott Morrison said:

Alex J. Best I think it's already been updated?

Indeed, I was fooled by https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Geometric.20Group.20Theory.20coordination.20.3F/near/369432763 which is a manual link masquerading as a linkifier..

[Scott Morrison]

Thanks @Mauricio Collares, updated #bors and #bors3.

[Mac Malone]

Mario Carneiro said:

sorry, I tried everything I could and the linkifier gods aren't in my favor

While not ideal, we could just add another special character to distinguish it (e.g., /lake#1) and do the same thing for e.g. /lean4#1.

[Mario Carneiro]

testing: lake#123 !lake#123

[Mario Carneiro]

lean4#123 doesn't seem to need it

[Mario Carneiro]

(the issue here is that while a linkifier for lake#NNN exists, it is shadowed by a more general linkifier and the regex flavor supported by zulip is not powerful enough to prevent the overlap, nor to adjust the relative priority of linkifiers)

[Mac Malone]

@Mario Carneiro is it possible that priority is determined by creation date?

[Mac Malone]

or possibly the privileges/account date of the creator?

[Mac Malone]

@Mario Carneiro From an examination of the Zulip code, this line suggests that custom linkifiers (realm filters) are sorted by their Django database id which afaik is just an auto-increasing integer. Thus, it suggests the linkifiers are essentially ordered by creation date.

[Mario Carneiro]

From what I can tell, the ordering of regex matching is defined by this loop, which gets the regexes from here, which uses the keys of a LinkifierMap. In other words, it's random.

[Mario Carneiro]

the linkifiers themselves are ordered in the database but they aren't walked in that order

[Mac Malone]

@Mario Carneiro If I am not mistaken, a JS Map is ordered by insertion. See keys().

[Mac Malone]

Thus, it should retain the database order.

[Mario Carneiro]

testing: zulip/zulip#123 lake#124

[Mario Carneiro]

lake#124

[Mario Carneiro]

no luck, I tried deleting and re-adding both lake and the general linkifier and it didn't help

[Mario Carneiro]

in any case this is clearly a feature suggestion

[Mario Carneiro]

testing std#123 std4#123

[Mario Carneiro]

I think std#NNN has the same issue as lake#NNN

[Mario Carneiro]

I've added !std#123 but I am not sure that's any better than std4#123

[Mac Malone]

@Mario Carneiro I wonder if the default leanprover-community linkifier is that necessary? Could we just make-do with the specific linkifiers for high-traffic repositories (e.g., std, mathlib, lean-liquid, etc.) and use the full-qualified linker (e.g., leanprover-community/leancrawler#4) for the rare cases. Or, if that is a bit too long to type, use a special character for the lean-community linkifier instead (e.g., !leancrawler#4).

[Mario Carneiro]

I'm still hoping that zulip can get this fixed

[Karl Stolley]

Hi Mario Carneiro and everyone--I'm from the Zulip core team. We're tracking the ordering of linkifiers in this issue; there's also a discussion on chat.zulip.org. Admittedly there hasn't been much movement on this issue since late 2022, but if you'd like to post there, that might help catch some more attention on the matter.

[PIG208]

Thanks for coming over Mario Carneiro to chat.zulip.org! I believe that the direct fix would be removing the default leanprover-community linkifier and re-adding it, and leaving the more specific ones unchanged. However, I agree that it would be more helpful if the linkifiers can be explicitly reordered. Will see if I can open a PR for the fix soon.

[Mario Carneiro]

okay, refreshed the leanprover-community linkifier. Here goes nothing: std#123 lake#123 !lake#123 mathport#123 zulip/zulip#123 std4#123

[Mario Carneiro]

almost: std#123 lake#123 !lake#123 mathport#123 zulip/zulip#123 std4#123

[Mario Carneiro]

yay, everything seems to be working :tada:

[Mac Malone]

Mario Carneiro said:

no luck, I tried deleting and re-adding both lake and the general linkifier and it didn't help

Mario Carneiro said:

okay, refreshed the leanprover-community linkifier [...] yay, everything seems to be working :tada:

Do you know what was difference between this time you refreshed the linkifier and last time? The zulip/zulip#23715 PR which fixed the order seems to have land long before this, so that would not seem to be the cause.

[Mario Carneiro]

I'm going to chalk it up to user error