search

leanprover / vscode-lean4

Visual Studio Code extension for the Lean 4 proof assistant
Apache License 2.0
169 stars 48 forks source link

feat: support for multi-toolchain workspaces #428

Closed mhuisi closed 7 months ago

mhuisi commented 7 months ago

This PR adds support for using multiple lean toolchains in the same workspace folder. It also enables users to use Lean 4 without first having to open a folder.

For nested workspaces, the client uses the outer-most Lean project. This is the correct behavior for projects in .lake, but not the correct behavior for actual nested projects. I unfortunately do not see a way to make the latter work because the language client library only supports globs to specify which files should be picked up by a language server, and hence cannot express something like "all Lean files in this directory, except those contained in inner directories with their own lean-toolchain". We could in principle set up middleware for every single notification and request, but this is likely to be overly fragile.

Closes #138.

david-christiansen commented 7 months ago

It would be extremely convenient for me to have support for nested folders with different toolchain versions.

Would it be a suitable workaround to symlink to the inner directory from somewhere else, then add that to the workspace?

mhuisi commented 7 months ago

It would be extremely convenient for me to have support for nested folders with different toolchain versions.

Do these different Lean projects depend on one another in some way?

mhuisi commented 7 months ago

It looks like the language client library recently added support for general notification and request middleware. I may take another stab at nested toolchains with that in mind.

mhuisi commented 7 months ago

Looks like the general request middleware doesn't allow us to filter requests. Unfortunately it looks like nested language clients are not feasible at this time.

david-christiansen commented 7 months ago

(for anyone following along, we spoke in person today and it'll be enough for the projects to be peer directories in the same Git repo, which will work for my use case)