missing red squigglies

Stream: lean4

[Kevin Buzzard]

In the below code (which contains an error)

structure Equiv (α : Type) (β : Type) where
  protected toFun : α → β
  protected invFun : β → α

infixl:25 " ≃ " => Equiv

protected def Equiv.symm {α : Type} {β : Type} (e : α ≃ β) : β ≃ α := ⟨e.invFun, e.toFun⟩

theorem Equiv.apply_symm_apply {α : Type} {β : Type} (e : α ≃ β) (x : β) :
  e.toFun (e.invFun x) = x := sorry

theorem apply_symm_apply (A B : Type) (e : A ≃ B) (a : A) (b : B) : e.toFun a = b :=
   -- put cursor directly after `a` and there's no red squiggle??
  Equiv.apply_symm_apply e a
  sorry

if I put my cursor on the sorry on the last line and then move it left so that it wraps up to just after the a (the character which the error is on) then the red squiggly under the a disappears! The file hence looks error-free. Is this expected? I can see this happening on VS Code but not on the web editor.

Hmm, actually when the red squiggle disappears, what appears is (in grey) "Ctrl-I to continue with Copilot" (which I have switched off right now).

(I'm sure this can be minimised more but I've got as far as removing mathlib so hopefully this is enough .)

[Martin Dvořák]

I get the red squiggle with the same cursor placement that you describe.

[Marc Huisinga]

I get an unknown identifier 'asorry' diagnostic when trying your reproduction.

[Kevin Buzzard]

Clarification: I'm not deleting the whitespace, I'm just moving the cursor

[Marc Huisinga]

So the squiggly disappears without making a change to the document?

[Kevin Buzzard]

Peek 2025-01-20 14-27.gif

Is this copilot? I don't know how to turn it off!

[Marc Huisinga]

Did you install the GitHub Copilot extension?

[Kevin Buzzard]

I had it disabled but it needed a VS Code restart. Yeah it's copilot. Sorry for the noise. Aren't other people experiencing this?

[Kevin Buzzard]

I had copilot switched off (you can see bottom right it's turned off) and then I went for "disable extension" and it prompted me to click "restart" and the problem was still occurring, which made me think it wasn't the copilot extension and was something else, but killing and restarting VS Code makes it go away.

[Marc Huisinga]

I had it disabled but it needed a VS Code restart

VS Code extensions need to clean up after themselves for the current session when they are deactivated or uninstalled, and I assume the GitHub Copilot extension just isn't doing this correctly.

[Kevin Buzzard]

Should I open an issue on the copilot repo?

[Marc Huisinga]

The extension appears to be proprietary, so there is no repo. This is the closest alternative: https://github.com/community/community/discussions/categories/copilot

If you want them to look at it, it's probably best to figure out if someone else already reported the issue and then if it hasn't been reported, reproduce it with a mainstream programming language like Python or TypeScript that Microsoft cares about.

[Kevin Buzzard]

OK that is beyond my abilities unfortunately because Lean is the only language I know :-(