Merge pull request #93 from kape1395/lsp

Language Server Protocol for TLAPM

Author: kape1395

.github/workflows/ci.yml

@@ -16,7 +16,7 @@ jobs:
               - macos-13
               - macos-14
             ocaml-compiler:
-              - '4.13.1'
+              - '4.14.1'
               - '5.1.0'
         env:
           EXAMPLES_DIR: "tlaplus-examples"
@@ -39,10 +39,15 @@ jobs:
               with:
                 path: _build_cache
                 key: ${{ runner.os }}_build_cache
+            - name: Install optional dependencies
+              if: startsWith(matrix.ocaml-compiler, '5.')
+              run: |
+                eval $(opam env)
+                make opam-deps-opt
             - name: Build TLAPM
               run: |
                 eval $(opam env)
-                opam install ./ --deps-only --yes
+                make opam-deps
                 make
                 make release
             - name: Run tests

.github/workflows/release.yml

@@ -97,10 +97,15 @@ jobs:
               with:
                 path: _build_cache
                 key: ${{ runner.os }}_build_cache
+            - name: Install optional dependencies
+              if: startsWith(matrix.ocaml-compiler, '5.')
+              run: |
+                eval $(opam env)
+                make opam-deps-opt
             - name: Build installer of TLAPS
               run: |
                 eval $(opam env)
-                opam install ./ --deps-only --yes
+                make opam-deps
                 make
                 make release
                 echo "TLAPM_RELEASE_FILE=$(make release-print-file)" >> "$GITHUB_ENV"

.gitignore

@@ -9,8 +9,9 @@
 
 /_build/
 /_build_cache/
-/.vscode/
+/.vscode/settings.json
 /tlaps-*.tar.gz
+/src/tlapm.bc
 
 __pycache__/
 *.pyc

.ocamlformat

@@ -0,0 +1,2 @@
+version=0.26.2
+profile=default

.vscode/cspell.json

@@ -0,0 +1,14 @@
+{
+    "words": [
+        "tlaplus",
+        "tlaps",
+        "tlapm",
+        "zenon",
+        "opam",
+        "ocaml",
+        "caml",
+        "sandboxing",
+        "sprintf",
+        "printexc"
+    ]
+}

Makefile

@@ -24,8 +24,11 @@ opam-update: # Update the package lists and install updates.
 opam-deps:
 	opam install ./ --deps-only --yes --working-dir
 
+opam-deps-opt:
+	opam install --yes eio_main lsp
+
 opam-deps-dev:
-	opam install ocamlformat ocaml-lsp-server earlybird
+	opam install --yes ocamlformat ocaml-lsp-server earlybird
 
 build:
 	dune build
@@ -44,6 +47,10 @@ test-fast:
 test-fast-basic:
 	make -C test fast/basic
 
+fmt:
+	# Only the LSP part is not formatted automatically.
+	cd lsp && dune fmt
+
 install:
 	dune install --prefix=$(PREFIX)
 	make -C $(PREFIX)/lib/tlapm/ -f Makefile.post-install

dune-project

@@ -12,6 +12,8 @@
 
 (license BSD-2-Clause)
 
+(cram enable)
+
 (package
  (name tlapm)
  (synopsis "TLA+ Proof Manager")
@@ -42,5 +44,11 @@
   dune-site
   dune-build-info
   sexplib
+  cmdliner
+  camlzip
+  re2
   ppx_inline_test
-  ppx_assert))
+  ppx_assert)
+ (depopts
+  lsp         ; https://github.com/ocaml/ocaml-lsp
+  eio_main))  ; https://github.com/ocaml-multicore/eio, only available on OCaml version >= 5.

library/dune

@@ -1,3 +1,6 @@
 (install
- (section (site (tlapm stdlib)))
- (files (glob_files "*.tla")))
+ (section
+  (site
+   (tlapm stdlib)))
+ (files
+  (glob_files "*.tla")))

lsp/README.md

@@ -0,0 +1,23 @@
+# LSP interface to the TLAPS
+
+The `tlapm_lsp` works as an adapter between the `tlapm` and code editors, e.g., VSCode.
+It is responsible for:
+  - Parsing the document structure to locate features related to proofs, e.g.:
+      - proof obligation by cursor position, possibly collecting all the subtree of obligations.
+  - Running the `tlapm` on specific obligations and reporting the results.
+  - Show progress of the tlapm, allow cancel it.
+  - TODO: Proof re-numbering.
+  - TODO: Proof decomposition.
+  - TODO: Easier experimentation on missing facts.
+
+The test folder contains a VSCode extension / LSP client. It is meant only for testing,
+the real integration should be done in the TLA+ VSCode extension.
+
+See:
+  - Dafny plugin. It shows all the obligations as testcases.
+    <https://github.com/dafny-lang/ide-vscode>
+    <https://github.com/dafny-lang/dafny/tree/master/Source/DafnyLanguageServer>
+  - VSCode Decorators: https://github.com/microsoft/vscode-extension-samples/blob/main/decorator-sample/README.md
+    https://vscode.rocks/decorations/
+    Gutter -- the left side of the editor.
+

lsp/bin/dune

@@ -0,0 +1,7 @@
+(executable
+ (name tlapm_lsp)
+ (public_name tlapm_lsp)
+ (optional) ; Only build, if eio is available, which is only the case for ocaml > 5.
+ (enabled_if
+  (>= %{ocaml_version}, "5.0.0"))
+ (libraries tlapm_lsp_lib eio_main cmdliner))