Zulip Chat Archive

Stream: general

Topic: new VS code freeze button


Patrick Massot (Mar 18 2020 at 21:30):

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

Patrick Massot (Mar 18 2020 at 21:31):

@Bryan Gin-ge Chen @Gabriel Ebner

Bryan Gin-ge Chen (Mar 18 2020 at 21:58):

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

Patrick Massot (Mar 18 2020 at 21:59):

image.png

Bryan Gin-ge Chen (Mar 18 2020 at 22:01):

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

Bryan Gin-ge Chen (Mar 18 2020 at 22:04):

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 (Mar 18 2020 at 22:05):

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 (Mar 18 2020 at 22:06):

Yes, that does look like the problem.

Bryan Gin-ge Chen (Mar 18 2020 at 22:14):

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 (Mar 18 2020 at 22:15):

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

Bryan Gin-ge Chen (Mar 18 2020 at 22:18):

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

Kevin Buzzard (Mar 18 2020 at 22:28):

Mine has looked like Patrick's for days now

Kevin Buzzard (Mar 18 2020 at 22:28):

Ubuntu

Gabriel Ebner (Mar 18 2020 at 22:32):

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

Kevin Buzzard (Mar 18 2020 at 22:44):

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 (Mar 18 2020 at 22:45):

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

Patrick Massot (Mar 18 2020 at 22:45):

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 (Mar 18 2020 at 22:48):

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 (Mar 18 2020 at 22:54):

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

Gabriel Ebner (Mar 19 2020 at 16:43):

Hmm, I can now reproduce this as well.

Bryan Gin-ge Chen (Mar 19 2020 at 16:47):

Does the insiders build help at all?

Gabriel Ebner (Mar 19 2020 at 17:12):

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

Kevin Buzzard (Apr 12 2020 at 13:53):

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 (Apr 12 2020 at 13:54):

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. (Apr 12 2020 at 13:55):

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

Kevin Buzzard (Apr 12 2020 at 13:56):

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

its_back.png

Kevin Buzzard (Apr 12 2020 at 13:56):

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

Kevin Buzzard (Apr 12 2020 at 13:57):

@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 (Apr 12 2020 at 15:10):

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 (Apr 12 2020 at 15:11):

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 (Apr 12 2020 at 15:37):

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.)


Last updated: Dec 20 2023 at 11:08 UTC