vscode-lean4
vscode-lean4 copied to clipboard
leanprover
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 :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.
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.
@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.
