VSCode extension hanging?

Stream: lean4

[Joe Hendrix]

It's my first time using Lean 4 in a while (currently on nightly-2021-12-07), and the VSCode extension seems to hang ("busily processing"). Any suggestions for fixing this?

[Chris B]

If you have stuff in a build directory from before Lean4 switched from leanpkg to lake that might be it. I got yellow bar stuff when the switch happened and just removed the old build dirs.

[Joe Hendrix]

@Chris B Thanks! That solved the problem.