Lean server not starting in VSCode

Stream: general

[Jeremy Tan]

I just updated my local copy of mathlib to the latest commit (4.21.0-rc1), but now the Lean infoview is forever saying "Waiting for Lean server to start..."

[Jeremy Tan]

i.e. apparently, the Lean server is never starting

[Jeremy Tan]

never mind, reinstalling the toolchain works, apparently

[Notification Bot]

Jeremy Tan has marked this topic as resolved.

[Marc Huisinga]

I managed to reproduce this issue and I think I know what is causing it.

[František Silváši 🦉]

Unfortunately, I can reproduce this as well :). VS Code won't start the Lean server on 4.21.0-rc1 for me.

[Riccardo Brasca]

Same here. What is the workaround?

[Marc Huisinga]

I'm implementing one right now, give me a few more minutes :-)

(This issue only affects 4.21.0-rc1)

[Marc Huisinga]

Details at vscode-lean4#618

[František Silváši 🦉]

Thanks Marc.

[Marc Huisinga]

0.0.206 of the Lean 4 VS Code extension has been released now. The issue should not occur on this version anymore.

[Anne Baanen]

In the meantime, I'm preparing release candidate 2 with exactly the same code but a rerolled commit hash, since not everyone will update their extension immediately.

[Anne Baanen]

Mathlib is now at v4.21.0-rc2, please let me know if there are any issues.

[Bhavik Mehta]

Anne Baanen said:

Mathlib is now at v4.21.0-rc2, please let me know if there are any issues.

It looks to me like there's not a release tag for mathlib rc2, so rev = "v4.21.0-rc2" in a downstream .toml doesn't work; is that intentional?

[Notification Bot]

Michael Rothgang has marked this topic as unresolved.

[Michael Rothgang]

I have this issue, but in the sphere-eversion project https://github.com/leanprover-community/sphere-eversion (never in mathlib). STR: clone the project (current master, i.e. mathlib 4.20 works), open the folder in VS Code, open Indexing.lean and watch the server never start.

[Marc Huisinga]

I can't reproduce, unfortunately.

[Marc Huisinga]

Ah, I can reproduce it if the project folder is called sphere-eversion, but not if it is called something else, like SphereEversion ...

[Marc Huisinga]

OK, I don't think it's the name after all. I'll look into it tomorrow.

[Marc Huisinga]

I think I actually can't reproduce that it never starts. It takes unusually long, but it does start eventually.

[Michael Rothgang]

Retrying again, now it works fast. It seems it was a different issue for sure.

[Michael Rothgang]

One part contributing to it: when the server wouldn't start, running lake exe cache get from a terminal also would "hang", and eventually error with "git exited with exit code 1" (and no further details).

[Michael Rothgang]

Perhaps this is a "error messages could be more helpful" bug report then...

[Marc Huisinga]

Michael Rothgang said:

Retrying again, now it works fast. It seems it was a different issue for sure.

It only happens on initial clone. I think it's because Lake is cloning dependencies when lake serve is called for the first time by the VS Code extension.

[Michael Rothgang]

Can there be a message printed to the terminal, that it's cloning dependencies or so? (Printing and erasing the message is fine with me; the point is to prevent an impression "nothing happens".)

[Marc Huisinga]

It does report the cloning progress information in the output panel at the end (presumably due to lean4#5615), but I can improve the language server startup progress bar in the bottom right to indicate that it may take a while if this is the first launch.

[Marc Huisinga]

vscode-lean4#619 improves the progress bar message

[Anne Baanen]

Bhavik Mehta said:

Anne Baanen said:

Mathlib is now at v4.21.0-rc2, please let me know if there are any issues.

It looks to me like there's not a release tag for mathlib rc2, so rev = "v4.21.0-rc2" in a downstream .toml doesn't work; is that intentional?

Apologies, fixed now!