Feature request: Support Live Share

[Vtec234]

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.

[mhuisi]

One issue is that LiveShare may be very unpleasant to use even when the InfoView works because edits by one user at the top of the file will cause a re-elaboration of the file, potentially throwing off people working at the bottom of it. Parallel elaboration should help with this when it lands.

[Vtec234]

@mhuisi that is a valid concern, but I have not found it to be that much of an issue, at least when edits sufficiently low-frequency. This is often the case when working on proofs and spending most of the time thinking rather than writing. Also, even when the infoview is reloading due to an edit higher up, the last known tactic state is still displayed.

[alok]

some incremental elab has been added, maybe good time to revisit this?

[YaelDillies]

This feature would be incredibly useful to me. @eu-robert and I are pair-programming and Eudes currently needs to share their screen via Discord while I suggest edits via vscode.