Waiting for Lean server to start takes forever

Stream: new members

[BluishRed]

Hello, I am new so excuse the lack of knowledge. I have followed the instructions provided here to create a project. I have followed the instructions exactly as they are written, and multiple attempts. Essentially when I have a lean file, is says "Waiting for Lean server to start..." in the infoview and there is a "Starting Lean language client" popup, as in the screenshot. The progress bar always gets to the same point and stops. If I wait for around 30-40 minutes, it eventually works correctly, without any issues. I'm just wondering why it is taking so long? Help would be appreciated, thanks.
Screenshot-2023-11-02-194111.png

[Kyle Miller]

When you followed the instructions, did lake exe cache get succeed?

After waiting the 30-40 minutes, if you close VS Code and restart it, does it start fast? If so, that indicates you're waiting around for it to compile mathlib and the cache isn't working.

[BluishRed]

Yes, every command succeeded without errors. Restarting VSCode has no effect, it takes just as long to load as before unfortunately

[Kevin Buzzard]

Can you send a screenshot with the file manager open? Have you used VS Code's "open folder" functionality to open the root directory of your project? What happens if you build the file on the command line? What OS?

[BluishRed]

Screenshot-2023-11-02-230128.png

I am unsure of what this 'open folder' functionality is, I just opened the folder in vscode following the instructions on the guide I linked above. I have tried to build everything on command line and then open in vscode at the end but the same thing happens :( I am using Windows 11. I really appreciate the help, this does seem to be a rather strange issue indeed.

[Kevin Buzzard]

Can you open the VS Code file manager and send a screenshot so we can see the state of the directory you're working in?

[Kevin Buzzard]

I am not clear about what's happening with build. What happens when you build the relevant file on the command line?

[BluishRed]

Sorry I'm not too sure what you mean here, The vscode file manager is open on the right side of the window in both the screen shots, is this the one you're referring too? I'm also not quite sure about build, I followed the directions given here which doesn't mention building files? Sorry for my lack of experience, this is my first time trying to use lean

[Leo Shine]

I had this recently and it seemed like when I did this on my C drive rather than my D drive it was far far quicker, if you've got multiple drive might be worth trying a different one.

[Kevin Buzzard]

Re file manager: sorry! I was expecting it on the left! I'm an idiot. Yeah that looks correct. What is the output of `lake build <path.to.file> on the command line?

[BluishRed]

Leo Shine said:

I had this recently and it seemed like when I did this on my C drive rather than my D drive it was far far quicker, if you've got multiple drive might be worth trying a different one.

Just moved it over to another drive and it takes considerably less time! I think this was it. Thank you so much everyone for the help.

[BluishRed]

Kevin Buzzard said:

Re file manager: sorry! I was expecting it on the left! I'm an idiot. Yeah that looks correct. What is the output of `lake build <path.to.file> on the command line?

No worries! I do have a rather unconventional vscode layout...

[Sebastian Ullrich]

@BluishRed @Leo Shine Any guesses on what the difference between your two drives is, is it HDD vs SSD? Certainly any kind of network drive would be the worst case for Lean, bad enough that we may want to warn about it.

[Leo Shine]

All on local laptop so must be ssd vs Hdd my operating system is on C so must be that way round

[BluishRed]

Sebastian Ullrich said:

BluishRed Leo Shine Any guesses on what the difference between your two drives is, is it HDD vs SSD? Certainly any kind of network drive would be the worst case for Lean, bad enough that we may want to warn about it.

Yes, it was a network drive. It might be a good idea to pop a warning somewhere as there is no indication that this was the case, with no error messages or anything.