Infoview should indicate when server is not started

[gebner]

Right now it shows "no info found" even if the server did not start.

[lovettchris]

Really? Mine says "Waiting for Lean server to start..." was this fixed recently perhaps?

[gebner]

I think I hit that issue back when we didn't start a Lean server for some directories that didn't contain lakefiles. I still see a similar issue when the server is terminated manually: #155

[Vtec234]

It seems like another instance of this issue occurs when there are errors in lakefile.lean. In this case lake serve enters a mode in which lakefile.lean can be edited, but every other file should immediately fail (see leanprover/lake#52). However the infoview gets stuck displaying "Waiting for server to start...", even when lakefile.lean is the active editor. See also Zulip discussion.

[lovettchris]

Specifically: "part of the problem seems to be that when lakefile.lean contains errors, lake serve prints them e.g. like so

./lakefile.lean:5:18: error: unknown constant 'Lake.PackageFacet.olean'
error: package configuration `./lakefile.lean` has errors

but then continues to execute the LSP server anyway. From the vscode extension's perspective, since it received no error code the server started up okay, and then this somehow leads to showing "Waiting" forever. Perhaps Lake should just exit with 1 at this point. /CC @Mac

Mac: @wojciech Nawrocki this is actually a new feature, not a bug. See Lake #52. :stuck_out_tongue_wink:

Wojciech Nawrocki: I see! Then vscode-lean4 should detect and handle this case.

[marianaalanis93]

Fixed and merged on #159