Zulip Chat Archive

Stream: general

Topic: incorrect alignment of red error line in VS Code


Kevin Buzzard (Feb 03 2020 at 09:32):

--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 (Feb 03 2020 at 09:36):

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

Gabriel Ebner (Feb 03 2020 at 09:37):

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

Kevin Buzzard (Feb 03 2020 at 09:38):

Can we use this to prove false?

Johan Commelin (Feb 03 2020 at 09:38):

Uuuh, no?

Gabriel Ebner (Feb 03 2020 at 09:38):

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

Johan Commelin (Feb 03 2020 at 09:38):

Lean is absolutely not confused. Only VScode is.

Kevin Buzzard (Feb 03 2020 at 09:39):

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

Gabriel Ebner (Feb 03 2020 at 09:39):

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

Kevin Buzzard (Feb 03 2020 at 09:39):

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 (Feb 03 2020 at 09:40):

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

Gabriel Ebner (Feb 03 2020 at 09:40):

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

Kevin Buzzard (Feb 03 2020 at 09:40):

gotcha

Kevin Buzzard (Feb 03 2020 at 09:41):

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 (Feb 03 2020 at 09:41):

aah no it goes the wrong way

Johan Commelin (Feb 03 2020 at 09:57):

Well, it could be under some whitespace, I guess

Stuart Presnell (Feb 10 2022 at 13:55):

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 (Feb 10 2022 at 13:56):

This is in #11332

Gabriel Ebner (Feb 10 2022 at 13:58):

(deleted)

Gabriel Ebner (Feb 10 2022 at 13:58):

(deleted)

Eric Rodriguez (Feb 10 2022 at 14:00):

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

Stuart Presnell (Feb 10 2022 at 14:01):

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 (Feb 10 2022 at 14:28):

Ok, thanks, I'd never noticed that before


Last updated: Dec 20 2023 at 11:08 UTC