VSCode squiggle off

Stream: general

[Patrick Massot]

It seems VSCode has trouble placing the red squiggles when some mathcal font is used, as in:

def 𝓕 : ℕ := 3

def x := 𝓕 + _

resulting in
image.png
compared to
image.png
which rightfully flags the underscore. I'm sure there is much to be done, this is probably a VSCode bug.

[Gabriel Ebner]

I'm surprised it took you so long to stumble upon this bug.

[Patrick Massot]

Maybe I saw it before and had post-traumatic amnesia

[Gabriel Ebner]

Simply put, it happens because vscode and lean count characters differently. In vscode, 𝓕 is two characters. While in Lean, 𝓕 is one character.

[Patrick Massot]

And usually I don't try to type so confusing expression (not the one in the mwe, the real one...)

[Sebastian Ullrich]

(Lean 4 has learned to count like VS Code)

[Gabriel Ebner]

(Technically speaking, vscode (and javascript) count UTF-16 code units by default. While Lean counts Unicode codepoints instead.)

[Oliver Nash]

Or possibly even UCS-2, right?

[Sebastian Ullrich]

(For people with too much time on their hands, there is a hilarious(ly long) thread on this whole issue over at https://github.com/microsoft/language-server-protocol/issues/376)

[Reid Barton]

I was going to say "we can blame Microsoft for this one" but then...

[Reid Barton]

well, let's just say we knew it was a Microsoft issue even before attributing the blame

[Patrick Massot]

I was trying to type

𝓕.φ x + ((L.loop h.1 (t*L.ρ x) x $ (L.N h) * L.π x) - 𝓕.φ x L.v) ⬝ L.π + (t*L.ρ x) • (corrugation.remainder L.p.π (L.N h) (L.loop h.1 1) x),

and I really needed help from Lean and VSCode

[Gabriel Ebner]

You can always insert a line break. The problem only occurs if you're on the same line as the 𝓕.