rewriting old links

Stream: Zulip meta

[Scott Morrison]

@Alya Abbott, could we ping you on a question? For a long time the main github repository that this community has worked with has been https://github.com/leanprover-community/mathlib, and so we set up a linkifier so that e.g. #17568 links there.

[Scott Morrison]

However, we're in the midst of a big transition, and work will switch to a different repository, namely https://github.com/leanprover-community/mathlib4.

[Scott Morrison]

We also have a linkifier for that, e.g. mathlib4#579

[Scott Morrison]

Is there any possibility of rewriting all the old messages, to replace #nnn with something like mathlib3#nnn?

[Junyan Xu]

Firstly, if links were generated when the message is posted and never change afterwards even if the linkifier is modified, then we would just need to edit the linkifier and do nothing else; I think it's unlikely that this is the case, but it would be nice if someone could confirm (couldn't find in the documentation).

Now assume that links are generated from text source when the message is displayed. Then it would be nice if the linkifier could check when the message was posted and generate a link to /mathlib or to /mathlib4 accordingly. If this is possible, there is again no need to mass-rewrite old messages.

[Junyan Xu]

Oh actually @Mario Carneiro suggests that links are generated when the message is posted:
Mario Carneiro said:

I don't think changes to the linkifier affect already posted messages

[Mario Carneiro]

let's test it: #made-just-for-you

[Mario Carneiro]

#made-just-for-you

[Mario Carneiro]

looks like I was right: the first message above uses a linkifier that existed only at the time of the message, and I think if I edit it the link will go away

[Alya Abbott]

Looks like we're all set here. :)