Lean hangs when changing imports

Stream: lean4

[Floris van Doorn]

I think this is a Windows-only issue.
When changing the imports of a file, Lean has to re-import the files. However, sometimes the Lean server (in VSCode) will just hang forever showing yellow bars, not making any progress for many mintutes. Reloading the window or restarting the file in VSCode will cause the Lean server to import the files correctly and be ready for use after a matter of seconds.

I have noticed this multiple times myself on Windows, and I have noticed this with various students and other people, I believe always on Windows.

Possibly related: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Server.20out.20of.20sync.20with.20file/near/403969226

[Floris van Doorn]

I created https://github.com/leanprover/vscode-lean4/issues/421

[Shreyas Srinivas]

Also happens on macOS

[Shreyas Srinivas]

Rarely enough that I can't exactly reproduce it these days. But it was more common last summer

[Yaël Dillies]

Doesn't happen to me on gitpod (which runs Ubuntu I believe)

[Christian K]

It also happened to me on Linux, especially when the files need to be built.
But not often enough to be reproducible.

[Sebastian Ullrich]

See also https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Yellow.20bar.20doesn't.20go.20away/near/428287485