Untitled files no longer work

[gebner]

Using untitled files does not (longer?) seem to work with the current release of the extension. I am a bit confused, because we have tests for this and they pass. I have elan installed, the default Lean version is set to today's nightly, and I've opened a Lean 4 project. Concretely:

1. Open mathlib4.
2. Ctrl-Shift-P "Create: New File..."
3. "Text File"
4. "Select a language"
5. "lean4"
6. No diagnostics are shown, and the infoview says "Waiting for Lean server to start..."

[lovettchris]

I cannot reproduce this in lean extension version v0.0.87 with the following your steps, and lean version `"4.0.0-nightly-2022-07-24".

Note: you will get the message "Waiting for lean server to start..." for ever if you have no elan installed and no lean in your path and the extension is waiting on you to press one of these buttons:

[lovettchris]

I wonder if it was busy installing "4.0.0-nightly-2022-07-04" and you just needed to wait a bit longer? This might be a new Lake behavior? Because I'm starting the Lean server requesting version ""

But Lake seems to then go and install the version listed in the mathlib folder somehow, even though I'm passing no cwd to the server process:

it might be getting a workspace cwd default from vscode. So while I start with only one lean toolchain installed, version leanprover/lean4:nightly (default) I end up with another one installed named leanprover/lean4:nightly-2022-07-04 which happens to be the mathlib4 version... and this is not the vscode extension requesting this install, it seems it is being done magically by lake?

Note: if I open vscode with no folder open and do Create: New File.... then I do get leanprover/lean4:nightly (default) instead of the mathlib4 version.

[lovettchris]

I have a potential fix here: #231