References to zulip in docstrings

Stream: mathlib4

[Luigi Massacci]

Guten tag,

I often run into docstrings with references to Zulip discussions, but there is almost never a link to the actual thread (eg: docs#Seminorm.instSupSet is what I was looking at right now, but there are other examples too). Is this on purpose? I understand that Zulip links used to be quite brittle, but if I'm not mistaken this has been fixed. Personally I find searching Zulip quite painful as an experience, so I think it would be much easier if threads were linked directly when relevant as opposed to relying on the prodigious memory of some mathlib contributors.

[Eric Wieser]

We should link to messages not threads, but indeed not linking is the worst of both worlds

[Luigi Massacci]

Out of curiosity, why would that be the case?

[Eric Wieser]

I think linking to a thread takes you to the last message in the thread

[Eric Wieser]

And doesn't always survive thread renames

[Eric Wieser]

Message links go to an immutable message id

[Kevin Buzzard]

In particular old links to threads which used to be "look at this short relevant discussion here" then become confusing when someone else revives the thread to talk about something a bit different and the link is now linking to the end of an irrelevant conversation

[Bryan Gin-ge Chen]

Should we add a tech debt item to go over Zulip links?