vscode-lean
vscode-lean copied to clipboard
Support multi-root workspaces
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:
- Do not do anything. We'd use the
leanpkg.pathfile from the first directory, the other directories may or may not work (probably not). Put a big warning in the readme. - 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.
- Support multiple
leanpkg.pathfiles in the server. This requires (backwards-incompatible?) changes in the c++ code: 1) some way to specify the list ofleanpkg.pathfiles (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.