Error "Waiting for Lean server to start

Stream: new members

[Donna Jo]

Hello, could anyone please help me fix the constant and lasting error "Waiting for Lean server to start..."? Thanks a lot!

[Donna Jo]

Hello, could anyone please help me fix the constant and lasting error "Waiting for Lean server to start..."? Thanks a lot!

[Kevin Buzzard]

Could you please post a screenshot showing the error, with the VS Code file explorer (assuming you're talking about VS Code) open? Note that Lean 4 will only process files which are part of correctly-formatted Lean 4 projects, and the root directory of the project must be opened using VS Code's "open folder" functionality.

[Notification Bot]

This topic was moved here from #lean4 > Error "Waiting for Lean server to start by Eric Wieser.

[Eric Wieser]

(I've moved this: in general, we usually handle installation problems in this stream)

[Notification Bot]

Eric Wieser has marked this topic as unresolved.

[Notification Bot]

A message was moved here from #lean4 > ✔ import tactics causes error by Eric Wieser.

[Nick Dean]

Hi,

One possible reason for the confusion that seems to have occurred with one or more people regarding the 'waiting for lean server to start' issue is that in this GitHub documentation the user is asked to try to evaluate a statement prior to having gone through the process of actually setting up a Lean project (which is explained in the following section).

[Kevin Buzzard]

Reading this documentation, it does read like "if you get 37 then Lean 4 is up and running; if you are interested in mathlib then you now need to do something else", so implicitly "and hence if you are not interested in mathlib then you are finished, and can just open Lean files in VS Code willy-nilly". Because I never use lean without mathlib I am unclear about to what extent this is true, but some testing seems to indicate that I really can just have a file test.lean which I open with VS Code, and Lean is working; import Lean seems to work fine etc.

Perhaps after "...successfully installed Lean 4!" it should say (without even starting a new paragraph) something like "However you will almost certainly want to have access to Lean's standard library, and perhaps also its mathematical library; right now you cannot access either of these, or indeed import any files at all. For a reasonable working experience you should now create a simple project. Projects contain important metadata such as which version of Lean you are using, and even simple experiements should be done within the context of a Lean project."

Is that last sentence true? Whether or not it is, perhaps it's good advice.

I would make the PR myself but can never remember what the relevant repo is.

[Utensil Song]

There are a few places to look for clues of what's going on:

• If you installed Lean 4 using the VSCode extension, and have a Lean 4 project code base opened
  • check Tab "Output" -> Menu "Lean Editor" in the bottom panel, if you see some error there, the installation has failed
  • check Tab "Problems", if you see it's compiling thousands of files from Std and Mathlib, go to Terminal, run source ~/.profile; lake exe cache get
  • try "Ctrl+Shift+P" (or Command+Shift+P under Mac), run "restart Lean server"
  • If it has no effect on the "Problems", try "stop Lean server" (same as above), and run lake build in your terminal to see what's going on
  • re-read anything in the README of the code base (may it be a tutorial or a game etc.) to figure out what's missing

If you still have no clue, you may read my experience shared here (and the links in it): https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Trouble.20installing.20lean4/near/389818546

[Nick Dean]

Hi all,

Just to clarify, I'm not having difficulties myself. What I was trying to point out but mightn't have worded very well is that perhaps the reason some newcomers seemingly continue to encounter this issue is that the documentation on GitHub I linked to might not be worded as clearly as it could be for a complete newcomer.

@Kevin Buzzard That sounds exactly right to me. As you say, I don't know why somebody would use lean without mathlib, but supposing someone interpreted those instructions available on GitHub a certain way without a second thought, it could explain the 'issue' some have reported (the real issue, then, not really being to do with lean, but rather with that documentation on GitHub).

[Utensil Song]

It seems that there are 3 more possibilities that one could encounter this error:

1. Run lake update when adding a dependency, but it updates mathlib to the latest commit, and that commit is still building its cache in CI. This is due to that https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency will create a project depending on Mathlib4 without fixing a commit, thus rely on the manifest to fix it, but it's volatile to instructions from other projects. Running lake update when working on mathlib-related projects (which is, most projects) is advised against on Zulip, but not emphasized in doc, just like issue 6 (Lean toolchain consistency) in my experience, and these are really needed to be emphasized.
2. Sometimes CI could generate invalid cache that lake ignores them silently and start the build from scratch. This happend recently and being diagnosed here, and it seems that lean-cache (in Rust) has to predict what lake (in Lean 4) would do to try to provide a valid cache so there might be a deeper rabbit hole here. But the good news is that lake exe cache get will be run by default with lake build/lake serve which is used by VSCode Lean 4 extension
3. There is a case where lean-cache can't download the cache ( I have one of my environments to reproduce this, and I suspect it's proxy related, but haven't dived into it yet)

[Utensil Song]

My experience is that Lean 4 is stable when you have set it up following some instruction in one doc for a project without thinking about each steps, then keep working on the project, but whenever you change an environment, or jump into a new project, or updated something, or copy-pasted something, or come back a few weeks later, it's easy to fall into some traps and encounter similar errors.

And when this happens, the steps and the separate issues of each step will surface, and troubleshooting them requires some knowledge about how all these tools work (Elan, Lake, lean-cache, VS Code Lean 4 extension etc.) and all these files (lean-toolchain, lakefile.lean, lake-manifest.json, ~/.profile, build/lake.lock, lake-packages etc.), and being aware of all these traps: "toolchain compatibility", "lake is not in PATH without relogin or run a platform-dependent file", "don't run lake update", "must run lake exe cache get and check if it succeeded", "check the commit you depended on when last time it worked" etc. I've managed to work through them and recorded them. It would be helpful to help update the docs, but I haven't fully wrapped my head around all these issues yet.