Orange bars in vscode jumping to the start of the file

Stream: general

[Eric Wieser]

I'm finding when editing leaf files in mathlib, that sometimes the orange bar jumps right back to the start of the file, and I have to restart lean for it to progress again

[Eric Wieser]

After I restart, everything behaves for about 5 minutes, and then it jumps right back to the top of the file again. Given the file takes about 2 minutes to build, this makes working on it extremely frustrating

[Eric Wieser]

Is there any way to work out what the server is doing here?

[Eric Wieser]

This behavior persists even after restarting vscode

[Kevin Buzzard]

Close all files other than the one you're editing?

[Eric Wieser]

It was the only one I was editing

[Eric Wieser]

Although I'm now wondering whether the vscode-lean extension actually supports having multiple vscode workspaces (with different mathlib installs) open at the same time

[Patrick Massot]

Eric Wieser said:

Although I'm now wondering whether the vscode-lean extension actually supports having multiple vscode workspaces (with different mathlib installs) open at the same time

And you're asking why you're in trouble? :lol:

[Marc Huisinga]

Eric Wieser said:

Although I'm now wondering whether the vscode-lean extension actually supports having multiple vscode workspaces (with different mathlib installs) open at the same time

A quick search shows that multiple features in vscode-lean were implemented with workspace.rootPath, i.e. before you could even open multiple workspaces.

[Eric Wieser]

To be clear, this is separate Vscode windows with a different workspace in each.

[Patrick Massot]

Note that you can open several instances of VScode, and everything will work smoothly.

[Eric Wieser]

multiple instances is I think what I'm describing

[Eric Wieser]

So it sounds like that shouldn't have been the cause