vscode-lean icon indicating copy to clipboard operation
vscode-lean copied to clipboard

Support multi-root workspaces

Open gebner opened this issue 8 years ago • 0 comments

Multi-root workspaces have not landed in stable vscode yet as of the June 2017 release, but I expect them to be released soon and we'd better be ready for them.

Potential solutions:

  1. Do not do anything. We'd use the leanpkg.path file from the first directory, the other directories may or may not work (probably not). Put a big warning in the readme.
  2. Start one server per directory. Pros: no change on the c++ side. Cons: large changes in the extension code, multiple servers are compiling the same code.
  3. Support multiple leanpkg.path files in the server. This requires (backwards-incompatible?) changes in the c++ code: 1) some way to specify the list of leanpkg.path files (probably command line options), and 2) merging them (can't see any problems there).

I'd prefer option 3, ideally we'd ship the necessary changes with lean 3.3.

gebner avatar Jul 22 '17 19:07 gebner