Very strange VScode font bug

Stream: general

[Peter Nelson]

AFAICT this is nothing to do with lean, but I'm hoping someone here might know about this:

For my project, I picked the unicode symbols ⧸ and ﹡ (different from the normal *) as notation; the ﹡ is now used in mathlib.
They usually display correctly, but when ⧸ appears before ﹡ in the same line, the latter displays as a tiny dot.
It even switches on the fly if I copy/paste the ⧸ in earlier in the line after the fact.

This happens even in a .txt file with no lean present. Changing the font family doesn't help, and this happens on more than one computer (both VSCode on mac).

It is only a display problem (the symbols parse and copy/paste correctly), but is annoying for readability.
Does anyone know what might be going on?

If others are also having this problem, I think I'll just make a PR to change the dual symbol to a different flavour of star.

[Julian Berman]

The keyword you probably are looking for is "ligatures".

[Julian Berman]

Specifically it sounds like you have a ligature enabled in your font for /* (which isn't uncommon as that's a comment character).

[Julian Berman]

What font / OS?

[Peter Nelson]

monospace on macos.
Note that the ⧸ is a weird unicode symbol and not the normal slash.

[Julian Berman]

I observe the same behavior it seems.

[Julian Berman]

(I did not notice what you just mentioned which makes it less likely to be a ligature so yeah strange, but let's see...)

[Julian Berman]

My naive guess is a font rendering bug. Which of course is impossible to search the VSCode issue tracker for (though probably it'd be in the Chromium one).

[Kyle Miller]

I can see this issue too. It seems like ﹡ is actually supposed to be a small asterisk: https://www.compart.com/en/unicode/U+FE61

Weirdly, it's only small if the slash comes before it, and there's no asterisk before that:

image.png

[Peter Nelson]

#12431 changes the notation - imo the easiest solution is to forget about this.