Zulip Chat Archive

Stream: Zulip meta

Topic: unicode characters in docs links

Eric Wieser (Nov 27 2020 at 19:12):

This fails: docs#polynomial.eval₂_ring_hom

Eric Wieser (Dec 03 2020 at 18:05):

As does docs#exterior_algebra.ι_multi

Rob Lewis (Dec 03 2020 at 18:07):

I don't know an immediate way to fix this and I'm not gonna think hard about it, if you can suggest an improvement to docs#(?P<decl>[a-zA-Z0-9_.'-]*[a-zA-Z0-9_'-]) I'm all ears.

Eric Wieser (Dec 03 2020 at 18:12):

Depending on the regex engine, using \p{L} to mean "any unicode letter" in the [] might work

Eric Wieser (Dec 03 2020 at 18:16):

If that doesn't work, putting (?u) on the front might help

Eric Wieser (Dec 03 2020 at 18:17):

So (?u)(?P<decl>[a-zA-Z0-9_.'-\p{L}]*[a-zA-Z0-9_'-\p{L}]), maybe

Eric Wieser (Dec 03 2020 at 18:20):

Ah, the docs seem to suggest it's python syntax - in which case
(?u)(?P<decl>[\w_.'-]*[\w_'-])
Since \w is unicode by default.

Rob Lewis (Dec 03 2020 at 18:57):

Eric Wieser said:

Ah, the docs seem to suggest it's python syntax - in which case
(?u)(?P<decl>[\w_.'-]*[\w_'-])
Since \w is unicode by default.

Failed: Invalid filter pattern. Valid characters are [ a-zA-Z_#=/:+!-].

Eric Wieser (Dec 03 2020 at 19:06):

How about if you drop the (?u)? (and add back the missing docs# that I forgot, whoops)

Rob Lewis (Dec 03 2020 at 19:09):

udocs#polynomial.eval₂_ring_hom
udocs#nat.succ

Rob Lewis (Dec 03 2020 at 19:10):

udocs#exterior_algebra.ι_multi

Rob Lewis (Dec 03 2020 at 19:10):

Nice, see if you can break that, if not I'll change docs#

Eric Wieser (Dec 03 2020 at 19:13):

Punctuation: udocs#ι,udocs#ι;udocs#ι|udocs#ι⟨udocs#ι⟩udocs#ι

Eric Wieser (Dec 03 2020 at 19:13):

Or is there just a link limit: udocs#ι,udocs#ι,udocs#ι,udocs#ι,udocs#ι

Eric Wieser (Dec 03 2020 at 19:14):

docs#ι,docs#ι;docs#ι|docs#ι⟨docs#ι⟩docs#ι

Eric Wieser (Dec 03 2020 at 19:14):

docs#a,docs#a;docs#a|docs#a⟨docs#a⟩docs#a

Eric Wieser (Dec 03 2020 at 19:14):

Well, it was broken before anyway

Rob Lewis (Dec 03 2020 at 20:38):

Okay, good enough for me. docs#polynomial.eval₂_ring_hom src#polynomial.eval₂_ring_hom

Kevin Buzzard (Dec 24 2022 at 23:47):

docs4#set.mem_unionᵢ₂

Kevin Buzzard (Dec 24 2022 at 23:49):

Can this be fixed? Looks like we fixed it for docs, from the above discussion? docs#set.mem_unionᵢ₂ ? (that declaration doesn't exist in lean 3) (oh it doesn't work either)

Kevin Buzzard (Dec 24 2022 at 23:54):

(oh sorry, that declaration doesn't seem to be in the mathlib 4 docs yet? It's here )

Last updated: Dec 20 2023 at 11:08 UTC