Language Server Protocol for TLAPM

[kape1395]

The changes are over #83 and #91. Closes #90 and #94. The corresponding client part for the VSCode extension is already merged as tlaplus/vscode-tlaplus#307.

• It invokes the parser directly (as a library function) to analyze the document structure and then invokes tlapm as a sub-process.
• The changes to the tlapm are:
  • Accept a file to check from a stdin. This allows the LSP server to check unsaved documents.
  • Accept a file to check as a string when calling the TLAPM parser as a library. Used by the LSP server to locate proof steps.
  • The location tracking for the QED step was broken in the parser. Now that's fixed. Used in the LSP server to show the proof status.
• The LSP server's part requires OCaml-5.1 because I use Eio for concurrency. I made it optional so the TLAPM can still be compiled in older OCaml versions.

From the functionality perspective:

• Proof checking can be invoked by pressing ctrl+g+g or via the code action (yellow lamp along the cursor position).
• Proof status is shown by marking document lines in different colors; the hover explanations are also present.
• Failed proofs are shown as diagnostics.
• Progress of the proof checking is shown (status bar). The operation can be canceled.
• If a new proof-checking command is invoked while the old one is still running, the old invocation is canceled automatically.

[damiendoligez]

Now that #83 and #91 are merged, could you rebase this PR? This will make reviewing easier.

[damiendoligez]

This concludes my review. Good to merge after you look at these last few comments.

[kape1395]

@damiendoligez, it seems I updated the PR according to all the comments. Thanks; they were all helpful.

[lemmy]

Minor regression: #149