server reloads imports?

Stream: new members

[Jalex Stark]

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?

[Jalex Stark]

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

[Kenny Lau]

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

[Mario Carneiro]

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

[Kenny Lau]

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

[Kevin Buzzard]

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

[Kenny Lau]

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

[Jalex Stark]

Kevin Buzzard said:

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

probably not since I am on macOS

[Kevin Buzzard]

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.

[Scott Morrison]

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. :-(