Support for multi-toolchain workspaces

Stream: lean4

[Marc Huisinga]

The support for multi-toolchain workspaces PR was recently merged into vscode-lean4. It resolves several long-standing usability issues with the VS Code extension that disproportionally affect new users:

• It is now possible to open Lean 4 files in VS Code without first having to open the respective project as a folder.
• When opening a parent or a sub folder of a Lean 4 project and then opening files within it, Lean will work as expected.
• When opening a folder that contains multiple Lean 4 projects and then opening files within it, Lean will work as expected and use the correct language server for each given file.

This PR is a significant refactor of the VS Code extension. It is likely that it still contains some bugs. I would greatly appreciate if people from the Lean community could help me test this version before it is released to everyone by installing the current vscode-lean4 pre-release (version 0.0.142) that contains this PR:
image.png

Please let me know about any new issues you encounter while using the pre-release version.

One caveat is that due to a limitation in the language client library used by the extension, vscode-lean4 unfortunately does not correctly support nested Lean projects yet. Similarly, when opening Lean files that are not contained in any Lean 4 project, the VS Code extension will use the parent folder of that file for the project scope of the language client. This means that if a non-project Lean file above a Lean 4 project is opened, it effectively acts like a nested project and will not work correctly, either. I hope to resolve these problems at some point in the future as well.

[Richard Copley]

It is now possible to open Lean 4 files in VS Code without first having to open the respective project as a folder.

How does one do that? Here's what I tried:

• Prepare a project

git clone https://github.com/leanprover-community/mathematics_in_lean.git mil
cd mil
lake exe cache get

• Launch VS Code without opening last workspace

code -n

• Open 'Extensions' on the navigation bar and make sure the pre-release Lean 4 extension is selected
• Select 'Open File…' from the 'File' submenu on the main menu bar
• Select 'MIL/C08_Groups_and_Rings/S02_Rings.lean' inside the project directory created above

And here's what happened:
The language server starts as lean.exe (not the expected lake.exe), the lean.exe process has working directory "c:\projects\lean" (not the expected "c:\projects\lean\mil") and the Infoview shows a message

unknown package 'Mathlib'
You might need to open 's:\projects\lean' as a workspace in your editor

[Marc Huisinga]

Richard Copley said:

It is now possible to open Lean 4 files in VS Code without first having to open the respective project as a folder.

How does one do that? Here's what I tried:

• Prepare a project

git clone https://github.com/leanprover-community/mathematics_in_lean.git mil
cd mil
lake exe cache get

• Launch VS Code without opening last workspace

code -n

• Open 'Extensions' on the navigation bar and make sure the pre-release Lean 4 extension is selected
• Select 'Open File…' from the 'File' submenu on the main menu bar
• Select 'MIL/C08_Groups_and_Rings/S02_Rings.lean' inside the project directory created above

And here's what happened:
The language server starts as lean.exe (not the expected lake.exe), the lean.exe process has working directory "c:\projects\lean" (not the expected "c:\projects\lean\mil") and the Infoview shows a message

unknown package 'Mathlib'
You might need to open 's:\projects\lean' as a workspace in your editor

Does your lean folder contain a lean-toolchain file?

[Richard Copley]

It did! Having deleted it, things run much more smoothly (the recipe above runs lake.exe in the mil project directory, as desired). Thanks.

[Marc Huisinga]

The problem was that this is precisely the kind of nested project mentioned above which we unfortunately cannot support yet. In nested projects, vscode-lean4 picks the outer-most lean-toolchain it can find (unless you opened a folder that contains a lean-toolchain file, in which case it stops searching at the folder boundary so that it will not see any lean-toolchain files above it). This is the correct behavior for Lean files in .lake and it results in less catastrophic failures in combination with the language-client library than the alternative of using the inner-most lean-toolchain file to define the scope.

Eventually, when we patch the language-client library to support nested clients, we should be able to use the inner-most lean-toolchain file instead and this interaction will work fine as well.

[Richard Copley]

Marc Huisinga said:

catastrophic failures

I can imagine: a little like this in Emacs

[Johan Commelin]

How should I install the experimental version of the VScode extension? Is there a "nightly" version, or something like that? I can't find it via the VScode extension search bar.

[Marc Huisinga]

Johan Commelin said:

How should I install the experimental version of the VScode extension? Is there a "nightly" version, or something like that? I can't find it via the VScode extension search bar.

Does the screenshot in the first post help?

[Johan Commelin]

Oops, I'm really silly. Yes, that screenshot should be more than enough

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

This is beautiful @Marc Huisinga, I have files open from three random repos using different versions of Lean and all work. Thanks!!

[Marc Huisinga]

Since no further issues have come up with the pre-release, this has now been released to everyone.
Most importantly, not opening the Lean 4 project as a folder should not be a major source of errors anymore.