Language Server Protocol for TLAPM

.github/workflows/main.yml

@@ -44,10 +44,15 @@ jobs:
             #   with:
             #     path: _build_cache
             #     key: ${{ runner.os }}_build_cache
+            - name: Install optional dependencies
+              if: matrix.ocaml-compiler == '2'
+              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
             - name: Run a subset of `tlapm` tests

.github/workflows/ocaml_versions.py

@@ -3,9 +3,9 @@
 
 
 OCAML_VERSIONS = [
-    '4.08.1',
-    '4.13.0',
-    '4.14.0',
+    '4.13.1',
+    '4.14.1',
+    '5.1.0'
     ]
 
 

.github/workflows/pr.yml

@@ -48,10 +48,15 @@ jobs:
             #   with:
             #     path: _build_cache
             #     key: ${{ runner.os }}_build_cache
+            - name: Install optional dependencies
+              if: matrix.ocaml-compiler == '2'
+              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
             - name: Run a subset of `tlapm` tests

.github/workflows/release.yml

@@ -110,10 +110,15 @@ jobs:
             #   with:
             #     path: _build_cache
             #     key: ${{ runner.os }}_build_cache
+            - name: Install optional dependencies
+              if: matrix.ocaml-compiler == '2'
+              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

@@ -13,7 +13,7 @@
 
 /_build/
 /_build_cache/
-/.vscode/
+/.vscode/settings.json
 /tlaps-*.tar.gz
 
 __pycache__/

.ocamlformat

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

.vscode/cspell.json

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

Makefile

@@ -20,8 +20,11 @@ all: build
 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
+	opam install --yes ocamlformat ocaml-lsp-server
 
 build:
 	dune build
@@ -40,6 +43,10 @@ test-fast:
 test-fast-basic:
 	make -C test fast/basic
 
+fmt:
+	# Onlt 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

@@ -10,6 +10,8 @@
 
 (source (github tlaplus/tlapm))
 
+(cram enable)
+
 (package
  (name tlapm)
  (synopsis "TLA+ Proof Manager")
@@ -40,5 +42,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))

lsp/bin/tlapm_lsp.ml

@@ -0,0 +1,111 @@
+(* cSpell:words cmdliner signum Open_wronly Open_creat fprintf kdprintf *)
+
+open Cmdliner
+
+let traceln_mutex = Mutex.create ()
+
+let transport_of_args tr_stdio tr_socket =
+  let open Tlapm_lsp_lib.Server in
+  match (tr_stdio, tr_socket) with
+  | true, None -> Ok Stdio
+  | false, Some port -> Ok (Socket port)
+  | _ -> Error "Exactly one of transports has to be specified."
+
+let run transport log_to log_io =
+  Printexc.record_backtrace true;
+  let main_fun (env : Eio_unix.Stdenv.base) =
+    let main_switch _sw =
+      let stop_promise, stop_resolver = Eio.Std.Promise.create () in
+      let handle_signal (_signum : int) =
+        Eio.Std.Promise.resolve stop_resolver "Stopping on SigINT"
+      in
+      Sys.set_signal Sys.sigint (Signal_handle handle_signal);
+      Tlapm_lsp_lib.Server.run transport log_io env stop_promise
+    in
+    let with_log_stderr () = Eio.Switch.run main_switch in
+    let with_log_file log_file =
+      let with_log_chan log_chan =
+        (* This is mostly a copy of default_traceln from eio/core/debug.ml,
+           just modified to take a specific out channel instead of stderr. *)
+        let traceln_impl ?__POS__:pos fmt =
+          let k go =
+            let b = Buffer.create 512 in
+            let f = Format.formatter_of_buffer b in
+            go f;
+            Option.iter
+              (fun (file, line, _, _) -> Format.fprintf f " [%s:%d]" file line)
+              pos;
+            Format.pp_close_box f ();
+            Format.pp_print_flush f ();
+            let msg = Buffer.contents b in
+            let lines = String.split_on_char '\n' msg in
+            Mutex.lock traceln_mutex;
+            Fun.protect ~finally:(fun () -> Mutex.unlock traceln_mutex)
+            @@ fun () ->
+            List.iter (Printf.fprintf log_chan "+%s\n") lines;
+            flush log_chan
+          in
+          Format.kdprintf k ("@[" ^^ fmt)
+        in
+        let traceln_bnd = { Eio.Debug.traceln = traceln_impl } in
+        let debug = Eio.Stdenv.debug env in
+        Eio.Fiber.with_binding debug#traceln traceln_bnd (fun _ ->
+            Format.pp_set_formatter_out_channel Format.err_formatter log_chan;
+            Eio.Switch.run main_switch)
+      in
+      Out_channel.with_open_gen
+        [ Open_append; Open_wronly; Open_creat ]
+        0o644 log_file with_log_chan
+    in
+    match log_to with
+    | None -> with_log_stderr ()
+    | Some log_file -> with_log_file log_file
+  in
+  Eio_main.run main_fun
+
+module Cli = struct
+  let arg_stdio =
+    let doc = "Run LSP over StdIO." in
+    let info = Arg.info [ "stdio" ] ~docv:"BOOL" ~doc in
+    Arg.value (Arg.flag info)
+
+  let arg_socket =
+    let doc = "Run LSP over TCP, use the specified port." in
+    let info = Arg.info [ "socket"; "port" ] ~docv:"NUM" ~doc in
+    Arg.value (Arg.opt (Arg.some Arg.int) None info)
+
+  let arg_log_to =
+    let doc = "Log all to the specified file instead of StdErr." in
+    let info = Arg.info [ "log-to" ] ~docv:"FILE" ~doc in
+    Arg.value (Arg.opt (Arg.some Arg.string) None info)
+
+  let arg_log_io =
+    let doc = "Log protocol's IO." in
+    let info = Arg.info [ "log-io" ] ~docv:"BOOL" ~doc in
+    Arg.value (Arg.flag info)
+
+  let term () =
+    let combine tr_stdio tr_socket log_to log_io =
+      match transport_of_args tr_stdio tr_socket with
+      | Ok transport -> `Ok (run transport log_to log_io)
+      | Error err -> `Error (false, err)
+    in
+    Term.(const combine $ arg_stdio $ arg_socket $ arg_log_to $ arg_log_io)
+
+  let name = "tlapm_lsp"
+  let doc = "LSP interface for TLAPS."
+
+  let man =
+    [
+      `S Manpage.s_description;
+      `P "tlapm_lsp allows LSP based IDEs to access the prover functions.";
+      `S Manpage.s_see_also;
+      `P "The TLAPM code repository: https://github.com/tlaplus/tlapm";
+    ]
+
+  let main () =
+    let info = Cmd.info ~doc ~man name in
+    Cmd.v info (Term.ret (term ())) |> Cmd.eval |> Stdlib.exit
+end
+
+let () = Cli.main ()

lsp/components.puml

@@ -0,0 +1,35 @@
+@startuml TLAPM-LSP
+
+component LspServer
+LspServer --> Session
+
+note as N_General
+    General layout of the tlapm_lsp_lib.
+end note
+
+component Session as Session {
+    component Handler
+}
+Session --> Prover
+Session --> Docs
+
+component Docs {
+    component Doc
+    component Version
+    component Actual
+    Doc *-- Version
+    Doc *-- Actual
+    Actual --> Parser
+}
+component Parser {
+    component TLAPM
+    component SANY
+}
+component Prover {
+    component Runner
+    component Toolbox
+    component Progress
+    Runner --> Toolbox
+    Runner --> Progress
+}
+@enduml

lsp/lib/const.ml

@@ -0,0 +1 @@
+let diagnostic_source = "TLAPM"

lsp/lib/const.mli

@@ -0,0 +1 @@
+val diagnostic_source : string

lsp/lib/docs/doc.ml

@@ -0,0 +1,53 @@
+open Util
+
+(* Max number of unprocessed/pending versions to keep. *)
+let keep_vsn_count = 50
+
+type t = {
+  uri : LspT.DocumentUri.t;
+  pending : Doc_vsn.t list;
+      (** All the received but not yet processed versions. *)
+  actual : Doc_actual.t;  (** Already processed version. *)
+}
+
+let make uri tv parser =
+  { uri; pending = []; actual = Doc_actual.make uri tv None parser }
+
+let with_parser doc parser =
+  { doc with actual = Doc_actual.with_parser doc.actual parser }
+
+let add doc tv =
+  let drop_till = Doc_vsn.version tv - keep_vsn_count in
+  let drop_unused = List.filter (fun pv -> Doc_vsn.version pv < drop_till) in
+  { doc with pending = tv :: drop_unused doc.pending }
+
+let latest_vsn doc =
+  match doc.pending with
+  | [] -> Doc_actual.vsn doc.actual
+  | latest :: _ -> Doc_vsn.version latest
+
+let set_actual_vsn doc vsn =
+  if Doc_actual.vsn doc.actual = vsn then Some doc
+  else
+    let rec drop_after_vsn = function
+      | [] -> (None, [])
+      | (pv : Doc_vsn.t) :: pvs ->
+          if Doc_vsn.version pv = vsn then (Some pv, [])
+          else
+            let res, pvs = drop_after_vsn pvs in
+            (res, pv :: pvs)
+    in
+    let selected, pending = drop_after_vsn doc.pending in
+    match selected with
+    | None -> None
+    | Some selected ->
+        let actual =
+          Doc_actual.make doc.uri selected (Some doc.actual)
+            (Doc_actual.parser doc.actual)
+        in
+        Some { doc with actual; pending }
+
+let with_actual doc f =
+  let doc, act, res = f doc doc.actual in
+  let doc = { doc with actual = act } in
+  (doc, res)

lsp/lib/docs/doc.mli

@@ -0,0 +1,12 @@
+(** Represents a document identified by its uri. It can contain multiple versions and all the related info. *)
+
+open Util
+
+type t
+
+val make : LspT.DocumentUri.t -> Doc_vsn.t -> Util.parser_fun -> t
+val with_parser : t -> Util.parser_fun -> t
+val add : t -> Doc_vsn.t -> t
+val latest_vsn : t -> int
+val set_actual_vsn : t -> int -> t option
+val with_actual : t -> (t -> Doc_actual.t -> t * Doc_actual.t * 'a) -> t * 'a