Start lean server using lake serve

[gebner]

Related to #61.

[gebner]

See also discussion on zulip: https://leanprover.zulipchat.com/#narrow/stream/147302-lean4-dev/topic/Expose.20--load-dynlib.20to.20Lean.3F/near/264029782

[lovettchris]

From Gabriel: On a high level, the biggest question is how the fallback should work. That is, when do we try lean --server after lake serve fails? Do we just call lake serve if there is a lakefile.lean present?

There's also a lot of tiny annoyances left. The extension has a configuration for the lean executable. Do we add one for lake as well? There is some version selection code by Chris which also makes it a bit harder to change replace lean --server by lake serve.

From Sebastian: Can we replace this with a setting for the toolchain root path (keeping bin/lean as the sanity check)? I'd like to avoid tying this to elan if not necessary.

[lovettchris]

Proposal, replace the following setting:

With:

Then the rules for using lake serve would be:

1. is 'lake' or 'lake.exe' found in the toolchainPath, If not don't use lake
2. is there a lakefile.lean in the current workspace root? If not don't use lake
3. If the above are both good, use lake serve with optional +version if there's a workspace override in effect.
4. If lake env lean --server fails fall back on lean --server.

[gebner]

I don't think it makes sense to fall back to lake env lean --server, just lake serve and lean --server should be good enough. Otherwise the logic looks good.

[lovettchris]

Yep, Mac showed me the "--" command line trick, so I already changed the code to use "lake serve -- filename" and "lake +version serve -- filename". I updated the PR description to match.

[lovettchris]

This PR is now merged