new VS code freeze button

Stream: general

[Patrick Massot]

My VS code just updated itself and it looks like the Freeze/Unfreeze tactic state buttons are now broken.

[Patrick Massot]

@Bryan Gin-ge Chen @Gabriel Ebner

[Bryan Gin-ge Chen]

I can't immediately reproduce this in VS Code 1.43.1 on macOS. What kind of brokenness are you seeing exactly?

[Patrick Massot]

image.png

[Bryan Gin-ge Chen]

I still see this: Screenshot-2020-03-18-18.00.29.png

[Bryan Gin-ge Chen]

Can you try Ctrl+Shift+P and enter "Developer: Open Webview Developer Tools" and see if you see anything suspicious in the console when you open / close the info view panel?

[Patrick Massot]

Is

Failed to load resource: net::ERR_UNKNOWN_URL_SCHEME
continue.svg:1 Failed to load resource: net::ERR_UNKNOWN_URL_SCHEME
pause.svg:1 Failed to load resource: net::ERR_UNKNOWN_URL_SCHEME

suspicious enough?

[Bryan Gin-ge Chen]

Yes, that does look like the problem.

[Bryan Gin-ge Chen]

What do you see if you go to the "Elements" tab, then click the button at the top left to "Select an element to inspect it", and then click on either of the broken buttons? Screenshot-2020-03-18-18.13.06.png

[Patrick Massot]

<img title="Freeze display" src="vscode-resource:/home/pmassot/.vscode/extensions/jroesch.lean-0.15.8/media/pause.svg">

[Bryan Gin-ge Chen]

It could be related to this issue. I guess restarting VS Code hasn't helped?

[Kevin Buzzard]

Mine has looked like Patrick's for days now

[Kevin Buzzard]

Ubuntu

[Gabriel Ebner]

I can't reproduce this either. I'm using vscode 1.42.1 on nixos (also no problems with 1.43.0).

[Kevin Buzzard]

If I close and open the goal tab then it just goes back to how it used to be with the pause icon

[Kevin Buzzard]

And then I if I restart Vs code it goes back to the two broken images. Maybe it only happens to mathematicians

[Patrick Massot]

This is not great, but at least I can continue recording screencasts for my locked down students without a weird bug

[Bryan Gin-ge Chen]

This does kind of sound like that issue I linked above. Sadly, it doesn't look like the commit linked there has gotten into a preview release yet.

[Bryan Gin-ge Chen]

I think the commit might be in the VS Code "Insiders" build?

[Gabriel Ebner]

Hmm, I can now reproduce this as well.

[Bryan Gin-ge Chen]

Does the insiders build help at all?

[Gabriel Ebner]

I can't easily try the insiders build, but restarting worked.

[Kevin Buzzard]

Hi. So I still have

broken_pics.png

some broken pics in my Lean goal. I was about to make a short Lean video with a screengrab but now I've realised that it looks a bit unprofessional. Is there any way I can fix this -- even a local hack? My experience in the past with these issues is that if you wait a while then someone fixes them with the next release but I am not sure we ever got to the bottom of this one and it's still there for me on Ubuntu 18.04 with VS Code 1.44.0 and version 0.15.8 of the Lean extension.

[Kevin Buzzard]

In fact I am so used to them now that I hadn't even noticed them for a month -- the only reason I noticed them now was that I thought I could turn on the option for hiding instances to make the goal look less intimidating, and then I realised that I didn't have that any more (there used to be a drop-down menu which let me hide variables called _inst37_ etc)

[Jason KY.]

Normally I just close the goal window and open it again, then it works

[Kevin Buzzard]

oh -- if I close the tab and open it again, I get back to the old system??

its_back.png

[Kevin Buzzard]

(not the VS Code window, just the lean goal tab)

[Kevin Buzzard]

@Jason KY. there is supposed to be a new system which ... wait ... maybe I have the new system? Yeah maybe this is what it's supposed to look like. Serves me right for never leaving Goal mode :-)

[Bryan Gin-ge Chen]

I'm now quite confident that this is due to the issue in VS Code I posted above: microsoft/vscode#89038. Sadly, it doesn't seem like the VS Code devs have been able to figure out a fix yet.

[Kevin Buzzard]

I shouldn't have mentioned it again, I'm sorry. It was just going to stop me making a video -- but once I realised the fix actually gave me the new version it was fine (I thought the fix gave me some old version).

[Bryan Gin-ge Chen]

I actually ran into this a few days ago and I would've posted here myself if I'd been been able to find this thread again. (All I was going to say was that closing and reopening the tab fixed it for me.)