fixing the mathlib#n linkifier

Stream: Zulip meta

[Riccardo Brasca]

Kim Morrison said:

Nearly all the changes required, however, seem positive. I've made 5 PRs so far backporting changes. mathlib#14993 mathlib#15119 mathlib#15120 mathlib#15125 mathlib#15126

You are linking mathlib3 PRs :)

[Floris van Doorn]

We should fix the linkifier (maybe the default linkifier got higher prio than the specialized linkifier).

[Edward van de Meent]

Kim Morrison said:

Nearly all the changes required, however, seem positive. I've made 5 PRs so far backporting changes. mathlib#14993 mathlib#15119 mathlib#15120 mathlib#15125 mathlib#15126

these links link to the wrong things... apparently, links to github.com/leanprover-community/mathlib redirect to github.com/leanprover-community/mathlib3... maybe this should be changed?

[Edward van de Meent]

i see i type slow :upside_down:

[Kim Morrison]

Does this work now: mathlib#15119

[Kim Morrison]

Nope

[Edward van de Meent]

not prepending mathlib should work tho

[Kim Morrison]

mathlib#15119

[Kim Morrison]

@Edward van de Meent yes, I understand: I've already editted my post. I'm trying to fix the linkifer.

[Notification Bot]

9 messages were moved here from #mathlib4 > Running Mathlib under set_option debug.byAsSorry by Kim Morrison.

[Edward van de Meent]

right... but maybe we still should fix the redirect on github

[Floris van Doorn]

We want to have mathlib redirect to mathlib3, at least for a while. mathlib was the name for mathlib3 until yesterday, and pointing it to mathlib4 now will break a bunch of links (and scripts).
We will probably do this at some point in the future.

[Edward van de Meent]

ahhh, that makes sense

[Daniel Weber]

Notification Bot said:

9 messages were moved here from #mathlib4 > Running Mathlib under set_option debug.byAsSorry by Kim Morrison.

Why does this link to "Running Mathlib under \x02klzzwxh:0000\x03"?