VS Code/Zulip/Github supr symbol size

Stream: general

[Kevin Buzzard]

In this code

def theorem_1_2 :
    ∃ L > 0, ∀ (p : I) (hp₀ : 0 < p) (hp₁ : p < 1) (X : Type*) (_ : Fintype X) (Λ : Set (X → ℝ≥0)),
      small p {s : Set X | L * 𝔼⁻[⨆ f ∈ Λ, ∑ x ∈ Xp, f x; Xp ∼ binomial_set_distribution X p]
        ≤ ⨆ f ∈ Λ, ∑ x ∈ s, f x} := by
  sorry

there's two suprema (\supr) (both ⨆ f ∈ Λ) and they display completely differently for me -- one (on the third line) is large and the other (on the 4th line) is small. But they seem to be the same character? This phenomenon persists on Zulip, Github and in VS Code. Am I just making a mistake and they're not the same character? I cut and pasted one onto the other and there was no change. Is it some kind of optical illusion??

[Yaël Dillies]

They look exactly the same to me here

[Kevin Buzzard]

Oh so it's a "my computer" (and someone else in the same room as me's computer) thing? Here's a screenshot:

Screenshot 2025-12-04 at 14.29.08.png

[Etienne Marion]

I get two different symbols too. This sometimes happens to me with the inner product symbol too ⟪.

[Kevin Buzzard]

Survey of the three people in the room I'm in: two see different sized suprs, one sees them the same. Is it like the blue/gold dress thing maybe? ;-)

[Etienne Marion]

I hope they are not looking at the same screen :laughing:

[Kevin Buzzard]

Oh ha ha yes this is three screens as well :-)

[Bhavik Mehta]

I remember seeing this quite a while ago in vscode; my recollection is that it's a unicode weirdness, to do with whichever other codepoints are in the same line (or maybe just the characters in the same line earlier than the symbol in question). But I'm not certain. It used to happen all the time with \hom; and there'd be two different length arrows for morphisms, one of which looked very much like \r

[Etienne Marion]

If I remove the 𝔼 in Kevin's code the big ⨆ goes back to normal.

[Eric Wieser]

Are they all using the same browser?

[Kevin Buzzard]

I'm using VS Code and the Zulip app and looking at github.com in Chrome (as was the other person who had different sizes) and I'm using a mac. I don't know what browser the same-size person was using as I'm no longer in the same room as them.

[Jireh Loreaux]

For me, they are all the same everywhere I look, and I have never experienced what Bhavik mentions either. I'm on Arch Linux and I checked VS Code, the Zulip App, Zulip in Opera and Falkon, and in the live web editor.

[Etienne Marion]

I see different symbols in VSCode and on Zulip, but not in the web editor (either safari or chrome). I'm on macOS.

[Kevin Buzzard]

See also this #mathlib4 > Calligraphic alphabet weirdness @ 💬 which is presumably the same issue. Whose "fault" is this?

[David Loeffler]

This does indeed seem to be the same issue. Maybe it is a Mac thing? Has anyone seen this on non-Mac systems?

[Snir Broshi]

Here's a few more:

𝔼 ⨆ ⋃ ⨄ ⨃ ⋁ ⨅ ⋂ ⋀ ⨂ ⨁ ⨀ ⨊ ⨝
  ⨆ ⋃ ⨄ ⨃ ⋁ ⨅ ⋂ ⋀ ⨂ ⨁ ⨀ ⨊ ⨝

macOS:
image.png

[Kevin Buzzard]

and David's

𝔼 ℋ
ℋ

in the other thread is displaying on for me as
Screenshot 2025-12-15 at 10.49.58.png

[Julian Berman]

What fonts are you all using, have you changed (or not changed) the default in VSCode perhaps?

[Julian Berman]

I have no issues here, but I use Monaspace. If I remove that (and then go back to the default Menlo, Monaco etc.), then I see two sizes.

[Kevin Buzzard]

I've definitely not knowingly changed any defaults at all on this machine

[Snir Broshi]

I'm also on the defaults. On Zed (which uses ZedMono) the sizes are the same

[Julian Berman]

(I'm just trying to explain Kevin's poll results.) I suspect -- and so far am 2 for 2? that the people seeing different sizes in VSCode are on the default font settings.

[Snir Broshi]

Oh on Zed even switching to Menlo or Monaco keeps the same sizes, so maybe this is a Chrome problem as Eric conjectured (Zed is written in Rust, not an Electron app)

[Julian Berman]

Neither Menlo nor Monaco seem to have ℋ in them, so in all cases I think there's a fallback font being used (and judging by Font Book I think it's Apple Symbols probably but I forget how to be sure in a way better than visual comparison...) Which still probably means it's a question of fallback font behavior in each of these.

[Julian Berman]

I think it's going to be something like that the fallback font is changing based on whether there's an 𝔼 there because that character is taller than the usual character height or something but I don't really know what I'm talking about, every time I try to keep font rendering knowledge in my head it disappears quickly.

[Snir Broshi]

From Chrome devtools:

First line (big): image.png

Second line (small): image.png

[Snir Broshi]

So the E causes the other 13 symbols to switch from Apple Symbols to STIX Two Math

[Snir Broshi]

(the 14 Menlo glyphs are the spaces I put between the math symbols)

[Julian Berman]

There we go thanks, I don't have Chrome installed here but was trying to check the same in FF before (but everything -- fortunately -- just works :)

[Snir Broshi]

by Chrome I meant I checked in VSCode's devtools (Help > Toggle Developer Tools)

[Snir Broshi]

No one can avoid having Chrome installed :sweat_smile:

[Julian Berman]

Oh fun I had no idea VSCode embedded even the dev tools (hopefully it's Chromium at least, but hey I only have VSCode installed to be able to participate in threads like these :P).

Anyways, that suggests one "fix" if someone wants -- namely, if you like the bigger symbol, you can add 'STIX Two Math' to the end (rather than front to not change all of your characters) of your font family setting in VSCode, search for font in settings and it should be the first result. (And if you like the smaller one you can add 'Apple Symbols')

[Snir Broshi]

I believe this is the culprit: CTFontCreateForString
"Returns a font reference that most accurately maps the string range based on the current font."
Not sure what's this "cascade list of the current font" that it references and how we can see it.
Chrome calls this function here
Still not sure why the E affects this function

[Ruben Van de Velde]

Is it possible that the first font doesn't have the E?

[Kevin Buzzard]

Screenshot 2025-12-15 at 12.09.57.png

This screenshot doesn't make much sense to me but it's what's happening on my mac. The A triggers the big H but not after another H, A triggers big B, H and B don't trigger each other etc.

This does affect my Lean usage (e.g. I was assuming that one of the sups in the original message was a different thing to the other one) even though it kind of feels off-topic for this forum. It would be nice if someone just said "this should be reported here" but are we still figuring out where to report it?

[Kevin Buzzard]

Snir Broshi said:

Chrome calls this function here

Chromium, right?

[Michael Stoll]

I don't see this on Linux.

[Julian Berman]

Kevin Buzzard said:

This does affect my Lean usage (e.g. I was assuming that one of the sups in the original message was a different thing to the other one) even though it kind of feels off-topic for this forum. It would be nice if someone just said "this should be reported here" but are we still figuring out where to report it?

I don't know what I think the fix is yet, but I think I'm swaying towards @Eric Wieser being right (suprise?). I've probably run out of energy to chase links, but https://issues.chromium.org/issues/329776392 and https://issues.chromium.org/issues/40887910 are close-but-not-exactly this kind of issue, and https://issues.chromium.org/issues/40459298 has a small bit of information on Blink's fallback behavior (and a linked presentation with some overview slides).

I.e. this would need to be fixed in Chromium. A workaround if possible would perhaps be to explicitly set the font fallback within the Lean extension in the way I mentioned on macOS, but I'm not sure how good of an idea that is, feels wrong.

[David Ledvinka]

As another data point I am not seeing a difference on my linux computer (and saw the difference on my Mac)

[Snir Broshi]

Kevin Buzzard said:

Snir Broshi said:

Chrome calls this function here

Chromium, right?

They differ by epsilon, but yeah

[Snir Broshi]

Kevin Buzzard said:

This screenshot doesn't make much sense to me but it's what's happening on my mac. The A triggers the big H but not after another H, A triggers big B, H and B don't trigger each other etc.

I think the difference is iff A is the first character in the line, right? This makes sense to me based on the code I linked, which seems to give macOS the entire line and ask for a font choice. Edit: Actually it asks macOS character-by-character, so I think the source of this first-character rule is still a mystery.

I also noticed that the rule isn't the first character, but rather the first non-ASCII character. That's why in your original example the characters before 𝔼 didn't matter.