TLAPS support via LSP.

[kape1395]

The TLAPS support is enabled via settings (tlaplus.tlaps.enabled). It is disabled by default.
The integration with the prover works via the LSP server, which is added to the https://github.com/tlaplus/tlapm repository; the corresponding branch (https://github.com/kape1395/tlapm/tree/lsp) still needs to be merged.

The LSP server must be built and installed to use this integration. Here are the steps I have tested for Ubuntu and Debian. It requires at least the OCaml version 5.0.0.

Setup the OCaml:

sudo apt install opam zlib1g-dev gawk time
opam init # Add `--disable-sandboxing` if running on docker or sandboxing is not supported.
opam switch create 5.1.0
eval $(opam env --switch=5.1.0)

Build the tlapm and tlapm_lsp from the source:

git clone -b lsp https://github.com/kape1395/tlapm
cd tlapm
make opam-deps
make opam-deps-opt
make
make install

At this point, the LSP server should be available. You can check that by

opam exec -- tlapm_lsp --help

The default configuration for the TLA+ VSCode extension now assumes the tlapm_lsp is accessible via opam as shown above. When setup is done, you can invoke the prover by ctrl+g+g. For now, the prover output is only shown as diagnostics. This should be improved.

[kape1395]

Relates to #153

[lemmy]

LGTM

[lemmy]

@kape1395, do you plan to continue pushing more commits, or would you prefer to merge this pull request and then open an additional pull request on top of it?

[kape1395]

I think it is good to merge. I will open another PR if needed.

[muenchnerkindl]

@kape1395: Thanks – after running into weird problems with updating my OCaml installation, I switched to a spare machine (MacOS) and managed to build this version of TLAPS. "opam exec -- tlapm_lsp --help" seems to produce the expected output. I also loaded the TLA+ Nightly VSCode extension and enabled TLAPS support. However, I don't seem to be getting the prover to work from VSCode: Ctrl-G brings up a dialog to navigate to a different location in the module, Cmd-G brings up a search dialog, and launching the command palette and searching for TLA+ doesn't show anything related to TLAPS. The expected log file doesn't exist, so I am assuming that the prover wasn't launched. What am I doing wrong?

[kape1395]

Hi. Thanks for looking at it. After trying it out as a nightly build of the vscode extension, I noticed that the key bindings were not set. I was wondering if that was a problem with my environment or something else. Key bindings were working in the development environment. I entered the key binding in the settings manually, and they started to work. That could be a collision with the standard Ctrl+g (go to line).

For now, the TLAPS support is disabled by default. You can enable it via settings:

If the LSP server works, you should see the proof steps highlighted. Please try reopening the vscode, if they don't appear after changing the setting (enable TLAPS), but I hope that's not needed.

Even if the key bindings are not working, you should see code actions for the proof steps and be able to invoke them by clicking. If you put a cursor on the proof step, a "lapm" appears (also ctrl+. shows that menu in my setup, not sure if that's standard). Code actions look like this:

If the proof step succeeds, the step is now highlighted in green.

I hope that helps find, what's wrong.

For the key bindings, maybe we have to find some, that are not interfering with the standard bindings.

[lemmy]

Related: #309

[kape1395]

Oh, that explains, where the key bindings have gone :)

[muenchnerkindl]

Thanks: I had enabled TLAPS support in the settings but hadn't restarted, that did the trick (should have thought of that myself).

Personally, I don't have preferences for the key bindings. I wouldn't mind if they were different from what the Toolbox uses.

Will I be able to build your PR tlaplus/tlapm#95 as described above in order to play with it and figure out how to fix the broken proofs?

[kape1395]

Yes, the same build instructions should work.

On the failing proof. After building the tlapm as described above, you can run a specific test case as

make -C test fast/regression/setEuclid_test.tla

The output of the test case can be found here:

./_build/default/test/fast/regression/setEuclid_test.tla.err
./_build/default/test/fast/regression/setEuclid_test.tla.out

Just a notice regarding the branches and the above test case:

• It is not failing on the PR Branch updated_enabled_cdot on top of dune, ocaml-5 and lsp. tlapm#95. It is not rebased yet on the current main, thus, don't include the changes from Smt fix tlapm#55, thus the test case is not failing.
• Currently, the above test case fails on the main branch and the PR Language Server Protocol for TLAPM tlapm#93.

[lemmy]

@kape1395 It appears as if the current integration depends on opam being installed. Are there plans to eventually remove this dependency?

[lemmy]

The TLAPS commands and the 'current proof step' view in the action bar are visible even when TLAPS/LSP is disabled in the extension settings. This can be confusing for novice users.

[kape1395]

It appears as if the current integration depends on opam being installed. Are there plans to eventually remove this dependency?

Actually, it doesn't depend on opam. opam exec -- tlapm is just a way to invoke tlapm installed via opam (as it is done now when building tlapm from the source) without knowing exact path to the executable. You can replace this part with tlapm if it is in your PATH. However, there is a plan to change the extension so that it would download the appropriate tlapm release for the user. Then, this path would default to the path where the tlapm release is unpacked automatically. We have to do a release in tlapm to proceed on this. But for now, it seems I have at least to fix tlaplus/tlapm#151. @lemmy

[kape1395]

The TLAPS commands and the 'current proof step' view in the action bar are visible even when TLAPS/LSP is disabled in the extension settings. This can be confusing for novice users.

Indeed. My idea was not to hide the panel but to show short instructions and/or a link to settings on how to enable the tlapm. This way, it would be more visible. We can discuss it in a separate issue #334.

I agree that the commands should be hidden if that setting is disabled.

[lemmy]

It appears as if the current integration depends on opam being installed. Are there plans to eventually remove this dependency?

Actually, it doesn't depend on opam. opam exec -- tlapm is just a way to invoke tlapm installed via opam (as it is done now when building tlapm from the source) without knowing exact path to the executable. You can replace this part with tlapm if it is in your PATH.

Good to know, thanks!