lake serve fails when lakefile.lean doesn't compile

[gebner]

1. echo does not compile > lakefile.lean
2. lake serve
3. error: package configuration `./lakefile.lean` has errors

I would expect lake serve to start nevertheless so that you get diagnostics while editing lakefile.lean.

We'd like to replace lean --server by lake serve in the editors if possible, and I'd like to avoid yet another corner case.

Falling back to lean --server when lake serve fails is not ideal either. In the future lakefiles might e.g. require dependencies. Then it would become important that lake serve works (and fetches those dependencies) so that you get diagnostics for the top-level lakefile.

[lovettchris]

reminder: remove the lean --server fallback in leanprover/vscode-lean4#97 when this issue is resolved, and perhaps if the lake version matches some number 3.0.1 or something...

[tydeu]

The problem here is that without a valid configuration file it is not clear what the behavior of lake serve should even be. Thus, I think Lake failing in such a scenario makes sense. The user of lake serve (e.g., the editor extension) is much better at determining what a reasonable failback is in this case than Lake (as Lake is devoid of any helpful information without a config file).

[gebner]

it is not clear what the behavior of lake serve should even be

lean --server seems like a reasonable default behavior.

The user of lake serve (e.g., the editor extension) is much better at determining what a reasonable failback is in this case than Lake

The editor has exactly as much (or as little) information as lake. Implementing the fallback in the editors is much more brittle as you need to distinguish different failure modes (wrong lean-toolchain file, crashing server, lean not installed, lakefile wrong), and falling back to lean --server is only appropriate in one of them.

I also don't want to implement the same fallback logic in three+ editor extensions.