`lake serve` fails when opening files in core

[JLimperg]

The recent change in c736c0b7370b924b7c2ec381bdb9bc055efa9a8e to use lake serve seems to cause a regression when opening files in core (i.e. .elan/toolchains/...). With the LSP workspace set to ~/.elan/toolchains/leanprover--lean4---nightly-2022-03-18/src/lean, it complains that ./lakefile.lean cannot be parsed (probably because it doesn't exist). I can provide more detailed repro instructions if needed.

[Kha]

@gebner Should the first branch here moved into the second one? https://github.com/leanprover/lake/blob/6b99f326aa49853a0b52aede020bda873d891d6b/Lake/CLI/Main.lean#L211-L214 The idea was to make lake serve work even outside of Lake projects, no?

[gebner]

The idea was to make lake serve work even outside of Lake projects, no?

It was never really a priority, since we needed a fallback for pre-lake serve versions anyhow (although this is becoming less and less relevant every month). I'd certainly be in favor of having only one server executable.

[Kha]

Should be fixed with https://github.com/leanprover/lake/pull/61#event-6275245449

[JLimperg]

Thanks!