Calligraphic alphabet weirdness

Stream: mathlib4

[David Loeffler]

The discussion about latex in docstrings reminded me of a tangentially related issue I'd been meaning to report.

When I type a calligraphic H (\McH) in VS Code, it seems to switch unpredictably between two different alphabets, one slightly smaller and "curlier" than the other:
Screenshot 2025-12-15 at 07.43.38.png
The 𝒜 at the start of the line is there because deleting it causes the H's on that line to flip to the other script! This seems to be harmless (the compiler accepts all these H's as the same letter), but slightly distracting, because it makes the docstrings a little harder to read.

[Kevin Buzzard]

Yeah it's the earlier Unicode messing things up -- I opened a thread about different sized Sups which is presumably the same issue. I don't know whose fault it is though -- I'm pretty sure it's not anything to do with lean as I could see the same phenomenon in web browsers and on zulip (edit: see here #general > VS Code/Zulip/Github supr symbol size @ 💬 )

[Eric Wieser]

This is probably a bug in Blink (chrome's rendering engine) somewhere

[Jireh Loreaux]

That is fixed in Opera? That seems unlikely.

[David Loeffler]

"Fixed in Opera" seems unlikely, but fixed (or not present) on Linux seems much more plausible – this is why I asked in the other thread if anyone had seen this on non-Mac systems.