incorrect alignment of red error line in VS Code

Stream: general

[Kevin Buzzard]

--TODO -- ask on Zulip

variable {A : Type}

def V (P : A) : A := P

-- (correct) error on underscore (Lean reports 8:26: error)
example (P : A) : V P = V _ := sorry

def 𝕍 (P : A) : A := P

-- the error is at the underscore but (for me) the red underline is under the 𝕍
-- (Lean reports 14:26: error)
example (P : A) : V P = 𝕍 _ := sorry

Using 𝕍 instead of V seems to confuse VS Code into putting the red wiggly error line in the wrong place. Can anything be done about this? Did I just mess up somehow?

[Johan Commelin]

I guess this is some unicode-confusion... :sad:

[Gabriel Ebner]

The reason is that 𝕍 is one Unicode codepoint (how Lean counts) but two UTF-16 characters (how vscode counts).

[Kevin Buzzard]

Can we use this to prove false?

[Johan Commelin]

Uuuh, no?

[Gabriel Ebner]

It only affects the error squiggles (they can be appear in the wrong column).

[Johan Commelin]

Lean is absolutely not confused. Only VScode is.

[Kevin Buzzard]

Can this be "fixed" or is it not broken?

[Gabriel Ebner]

We could theoretically adjust the column of the error messages in the vscode extension. PRs are welcome!

[Kevin Buzzard]

I have a file where I have 100 occurrences of 𝕍. How come VS Code is not putting the red error messages 100 characters from where they should be?

[Kevin Buzzard]

Or maybe it is and I am just so great at avoiding errors that I never noticed?

[Gabriel Ebner]

The line number is unaffected. It only matters if you're right of a 𝕍 on the same line.

[Kevin Buzzard]

gotcha

[Kevin Buzzard]

Doesn't this mean that I can get VS Code to have an error in a place where there isn't a character?

[Kevin Buzzard]

aah no it goes the wrong way

[Johan Commelin]

Well, it could be under some whitespace, I guess

[Stuart Presnell]

I'm getting another example of the wiggly-error-underline appearing in the wrong place. Screenshot-2022-02-10-at-13.43.06.png

The Info View window is correctly reporting that I have a sorry in data.nat.factorization, but the orange underline is on import algebra.char_p.two.

(When I mouse over the underline, the popup also correctly reports that there's a sorry in data.nat.factorization)

[Stuart Presnell]

This is in #11332

[Gabriel Ebner]

(deleted)

[Gabriel Ebner]

(deleted)

[Eric Rodriguez]

I've always noticed this, I thought this was just how imports worked.

[Stuart Presnell]

Oh, is it typically just whatever's the last line of the import block that gets underlined, independent of which file has the problem?

[Stuart Presnell]

Ok, thanks, I'd never noticed that before