Zulip Chat Archive

Stream: new members

Topic: server reloads imports?


view this post on Zulip Jalex Stark (Apr 30 2020 at 14:33):

Sometimes VSCode will decide that I don't get to see anything in the Lean messages anymore, and the yellow bar on the side of the screen goes all the way up to the first line of my file. I think what's happening is that it decided to rerun all of the code in the imported files. But sometimes it hangs there for minutes and I have to restart VSCode. Any ideas about what is going wrong?

view this post on Zulip Jalex Stark (Apr 30 2020 at 14:37):

oh, I am being dumb. I was working on the files in my project while leanproject up was running...

view this post on Zulip Kenny Lau (Apr 30 2020 at 14:39):

no but sometimes this also happens to me whenever I decide to peek the definition of something or print something

view this post on Zulip Mario Carneiro (Apr 30 2020 at 14:39):

Sometimes things like hovers can trigger a recompilation of imported files. I'm not sure exactly what conditions cause it

view this post on Zulip Kenny Lau (Apr 30 2020 at 14:40):

yeah and it isn't immediate after the two conditions above, but it doesn't happen if I don't do the two things above

view this post on Zulip Kevin Buzzard (Apr 30 2020 at 14:41):

Is this a Windows only thing which has been mentioned in the past?

view this post on Zulip Kenny Lau (Apr 30 2020 at 14:42):

the standard workaround is to restart the Lean server (Ctrl+Shift+P)

view this post on Zulip Jalex Stark (Apr 30 2020 at 14:42):

Kevin Buzzard said:

Is this a Windows only thing which has been mentioned in the past?

probably not since I am on macOS

view this post on Zulip Kevin Buzzard (Apr 30 2020 at 14:46):

When I get the orange bar hell it is usually because I didn't quite wait for long enough for leanproject up (I'm on linux). I think that VS Code implicitly compiles stuff somehow, and then if you change olean files it can get very confused and try to start again from scratch. Restarting VS Code should work (this is just something which one occasionally has to do, in my experience -- sometimes the goal window can crash, or sometimes you can get some hideous memory error etc). I used to restart Lean but for some reason I now have it in my head that when you're messing with olean files then it's safer to just restart VS Code.

view this post on Zulip Scott Morrison (May 02 2020 at 03:20):

I've also been finding that merely restarting the server doesn't solve all problems, and restarting VS Code is more effective. Sometimes, especially when my computer is working harder, I will get into a state where clearly old requests are not being cancelled properly, and I'll get error messages appearing which reflect my keystrokes one by one, but spaced much too long apart. Restarting the server doesn't help, but restarting VS Code always solves it. I've never found a reproducible trigger, sadly. :-(


Last updated: May 16 2021 at 05:21 UTC