broken lightbulb

Stream: general

[Kevin Buzzard]

I didn't even explain the reason I was running #print submodule! What I meant to say was: is the lightbulb broken for anyone else?

import algebra.module.submodule

example : submodule ℤ ℤ :=
{! !}
/-
«[goal]» : submodule ℤ ℤ
Hole: Lint/Infer/Match Stub/List Constructors/tidy/Show/Use/Equations Stub/Instance Stub/library_search
-/

It appears, and then when I try and click on it, it disappeared. [I then used #print submodule to see the structure fields and was overwhelmed and got distracted :-) ]

[Kevin Buzzard]

So I absolutely have a broken lightbulb, but only on my laptop. On my desktop things are working fine. On my laptop with the same repo, whenever I attempt to move onto the lightbulb, it disappears. Help!

[Bryan Gin-ge Chen]

I'm not able to reproduce this, but does hitting the keyboard shortcut for "Quick fix" when your cursor is next to the light bulb work? (On macOS the combination is cmd+., so I'm guessing it's ctrl+. on Linux.)

[Kevin Buzzard]

wooah that works! :D

[Kevin Buzzard]

Peek-2021-05-04-21-48.gif

If you all want to laugh at me...

[Bryan Gin-ge Chen]

That's really strange. I suspect some kind of VS Code bug.

[Kevin Buzzard]

Version: 1.55.2
Commit: 3c4e3df9e89829dce27b7b5c24508306b151f30d
Date: 2021-04-13T09:37:02.931Z
Electron: 11.3.0
Chrome: 87.0.4280.141
Node.js: 12.18.3
V8: 8.7.220.31-electron.0
OS: Linux x64 4.15.0-140-generic

[Kevin Buzzard]

That's my ubuntu 18.04 laptop (where i have the broken bulb). On my Ubuntu 20.04 desktop I have

Version: 1.55.2
Commit: 3c4e3df9e89829dce27b7b5c24508306b151f30d
Date: 2021-04-13T09:37:02.931Z
Electron: 11.3.0
Chrome: 87.0.4280.141
Node.js: 12.18.3
V8: 8.7.220.31-electron.0
OS: Linux x64 5.4.0-72-generic

and the lightbulb is working fine.

[Yaël Dillies]

It happens to me too, but inconsistently, and most of the time the lightbulb only disappears when my mouse is in some small particular spots.

[Eric Rodriguez]

(deleted)