Lake commands hang indefinitely

Stream: general

[J. Simon Richard]

Right now on my machine, commands like lake env hang indefinitely.

A while ago I fixed an error like this by closing a VS Code instance running a LEAN LSP, which makes me think there's some kind of lock issue. Any tips on how to debug this further?

I killed all of the other lean/lake processes on my machine to see if that would help, but it didn't. Does lean or lake use file-based locks?

For now I'll just restart my computer, but it would be nice to find the root cause of this issue.

[Yury G. Kudryashov]

What OS? What repo? What Lean version?

[J. Simon Richard]

Arch Linux; the repo is private, but all lake commands (in any project) hang indefinitely (or they did until I restarted my machine);

I'm using different lean versions in different projects. The project I was working on when (I think) the bug started is 4.19.0-rc2, and my lake version is 5.0.0-fafd381.

The default lean version (lean --version in $HOME) is 4.26.0

[Julian Berman]

On Linux perhaps try stracing running your lake command, which should at least tell you what it's waiting on or doing.

[J. Simon Richard]

Yeah, I'll do that the next time I run into this issue