Feature request: Support Live Share

Proposal

VS Code Live Share is a feature that allows multiple clients to edit the same file. When using Live Share with Lean, standard LSP functionality (autocomplete, hovers, ..) already works for all clients, but the infoview only works in the primary client (the one running the Lean server). Attempting to open the infoview in the secondary client results in various errors, for instance command 'lean.displayGoal' not found. Note that it is possible to test this locally by opening two windows, sharing from one, and joining from the other.

The Lean server already supports multiple RPC sessions, so in principle it should be possible to add support for a working infoview in both Live Share clients by modifying the extension only.

• User Experience: Better support for collaborating on Lean programs.

• Beneficiaries: Anyone collaborating using Live Share.

• Maintainability: Difficult to say; it may add complexity or lead to a refactoring that simplifies something.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start by reproducing the issue with two VS Code windows using Live Share, as described in the proposal, and compare infoview behavior between the primary and secondary clients. Trace how the extension exposes the infoview and handles the lean.displayGoal command. Done means both clients can open and use the infoview while standard Lean functionality continues to work.