search

tlaplus / tlapm

The TLA Proof Manager
https://proofs.tlapl.us/
BSD 2-Clause "Simplified" License
65 stars 20 forks source link

LSP support #90

Closed kape1395 closed 1 month ago

kape1395 commented 1 year ago

This is related to https://github.com/tlaplus/vscode-tlaplus/issues/153.

The current TLAPS/Toolbox integration involves document parsing on the Toolbox side (it uses Sany for that, as I understand). While moving to the VSCode, I would like to push as much logic out of the editor to the backend (TLAPS). The parsing is one aspect. The TLAPS has a parser implementation anyway, and the parser is used by the editor in the scope of the proofs, at least for locating the obligations (or a sub-tree of obligations), folding, and probably proof decomposition functionality.

Instead of implementing a specific protocol for the TLAPS integration in the VSCode, it may be worth trying to implement LSP (Language Server Protocol) internally in the TLAPS. E.g., if started with the --lsp option instead of the --toolbox, it would behave as an LSP server. It could then receive a document to process, handle commands (e.g., check a step, propose a decomposition, etc.), and output the relevant information.

It looks like there are some LSP building blocks that would be reused, e.g., https://github.com/ocaml/ocaml-lsp. I hope it should not interfere with the existing functionality as VSCode supports multiple LSP servers for a single document.

What do you think about such a direction?

lemmy commented 1 year ago

No worries about interference as the current vscode-tlaplus extension is not built with LSP.

muenchnerkindl commented 1 year ago

Your suggestion sounds good to me, but it may require substantial changes to tlapm, which AFAIK is currently not expecting to interact reactively with the IDE.

kape1395 commented 1 year ago

I will experiment a bit and then return with the results.

kape1395 commented 1 year ago

Some LSP commands are working already, document synchronization and some fake diagnostics are shown. The code is in OCaml; the initial draft is here: https://github.com/kape1395/tlapm/tree/lsp/lsp. It is on top of PR #83 and #91.

Moving further depends on how to present the proof states and accept the user's actions. The proof obligations could be shown as test cases like in the Dafny IDE.

image

Maybe you have other approaches to try? I checked: