Zulip Chat Archive

Stream: general

Topic: Orange bars in vscode jumping to the start of the file


view this post on Zulip Eric Wieser (Feb 06 2021 at 11:27):

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

view this post on Zulip Eric Wieser (Feb 06 2021 at 11:27):

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

view this post on Zulip Eric Wieser (Feb 06 2021 at 11:27):

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

view this post on Zulip Eric Wieser (Feb 06 2021 at 11:30):

This behavior persists even after restarting vscode

view this post on Zulip Kevin Buzzard (Feb 06 2021 at 11:57):

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

view this post on Zulip Eric Wieser (Feb 06 2021 at 12:48):

It was the only one I was editing

view this post on Zulip Eric Wieser (Feb 06 2021 at 12:49):

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

view this post on Zulip Patrick Massot (Feb 06 2021 at 12:51):

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:

view this post on Zulip Marc Huisinga (Feb 06 2021 at 12:52):

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.

view this post on Zulip Eric Wieser (Feb 06 2021 at 12:53):

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

view this post on Zulip Patrick Massot (Feb 06 2021 at 12:53):

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

view this post on Zulip Eric Wieser (Feb 06 2021 at 12:53):

multiple instances is I think what I'm describing

view this post on Zulip Eric Wieser (Feb 06 2021 at 12:54):

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


Last updated: May 14 2021 at 13:24 UTC