Yellow bar doesn't go away

Stream: new members

[Elena]

I checked out mathlib and got the cache, lake build also works (within seconds). When I start VS Codes and open a random file in the Mathlib folder the yellow bar at the side does not go away, even after waiting for minutes. When I make a new file that does not contain any Mathlib import I can for example get the result of #eval 2 +2 just fine.
Do you have any ideas, what I should do?

I am running Ubuntu 22.4

[Jireh Loreaux]

I've just experienced this once or twice in the last few days. It's ugly but killing lean with

$ kill `pidof lean`

and then restarting the server was successful for me, whereas simply restarting VS Code was insufficient. I haven't been able to reproduce the problem reliably yet, and my setup is a bit weird, so I thought that may have been the cause.

[mars0i]

Please ignore this post. Starting a different thread.

[Jireh Loreaux]

@mars0i wrong thread? If you can point me to the thread you want it in, I can move it.

[Jireh Loreaux]

@Scott Morrison just a heads up that this has been experienced by a least two people. If I can reproduce reliably at any point I'll make an issue.

[mars0i]

@Jireh Loreaux Yes--sorry, I accidentally give it the wrong title. Thanks. I thought I'd given it a new title. Fixed now.

[mars0i]

Ah, now I've subverted the response to @ScottMorrison's post.

[mars0i]

I'm going to try to back this out and start over. Ack! Sorry!

[Elena]

Jireh Loreaux said:

I've just experienced this once or twice in the last few days. It's ugly but killing lean with

$ kill `pidof lean`

and then restarting the server was successful for me, whereas simply restarting VS Code was insufficient. I haven't been able to reproduce the problem reliably yet, and my setup is a bit weird, so I thought that may have been the cause.

That command worked out for me, thank you!

[Mario Carneiro]

@Jireh Loreaux said:

I've just experienced this once or twice in the last few days. It's ugly but killing lean with

$ kill `pidof lean`

and then restarting the server was successful for me, whereas simply restarting VS Code was insufficient. I haven't been able to reproduce the problem reliably yet, and my setup is a bit weird, so I thought that may have been the cause.

I usually use killall lean, is there a reason to use this form instead?

[Jireh Loreaux]

No, I don't think so. They are probably equivalent for this simple use case, right?

[Kevin Buzzard]

There is an imperial student with this problem, but if you wait for two minutes then the orange bars do go away. I can't reproduce on command line. Could this be the same thing?

[Sebastian Ullrich]

If they are on Linux, running this line while the yellow bars are there should provide some valuable information

pidof lean | xargs -n1 gdb --batch -ex "info proc" -ex "thread apply all bt" -p

Try to have only one project and only one Lean file in it opened to minimize the output