diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 2d10f3c6..2eb98d76 100644 --- a/.github/workflows/ci.yml +++ b/.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 diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 51e19fe4..d1c6fcbb 100644 --- a/.github/workflows/release.yml +++ b/.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" diff --git a/.gitignore b/.gitignore index ab6fe08c..f2763769 100644 --- a/.gitignore +++ b/.gitignore @@ -9,8 +9,9 @@ /_build/ /_build_cache/ -/.vscode/ +/.vscode/settings.json /tlaps-*.tar.gz +/src/tlapm.bc __pycache__/ *.pyc diff --git a/.ocamlformat b/.ocamlformat new file mode 100644 index 00000000..8adea03e --- /dev/null +++ b/.ocamlformat @@ -0,0 +1,2 @@ +version=0.26.2 +profile=default diff --git a/.vscode/cspell.json b/.vscode/cspell.json new file mode 100644 index 00000000..4bf3f7c3 --- /dev/null +++ b/.vscode/cspell.json @@ -0,0 +1,14 @@ +{ + "words": [ + "tlaplus", + "tlaps", + "tlapm", + "zenon", + "opam", + "ocaml", + "caml", + "sandboxing", + "sprintf", + "printexc" + ] +} diff --git a/Makefile b/Makefile index bdcf442b..c23f1454 100644 --- a/Makefile +++ b/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 diff --git a/dune-project b/dune-project index e93212d9..5f370468 100644 --- a/dune-project +++ b/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. diff --git a/library/dune b/library/dune index 9b2e33cd..e803c05b 100644 --- a/library/dune +++ b/library/dune @@ -1,3 +1,6 @@ (install - (section (site (tlapm stdlib))) - (files (glob_files "*.tla"))) + (section + (site + (tlapm stdlib))) + (files + (glob_files "*.tla"))) diff --git a/lsp/README.md b/lsp/README.md new file mode 100644 index 00000000..f05290d9 --- /dev/null +++ b/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. + + + - 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. + diff --git a/lsp/bin/dune b/lsp/bin/dune new file mode 100644 index 00000000..f49f1aba --- /dev/null +++ b/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)) diff --git a/lsp/bin/tlapm_lsp.ml b/lsp/bin/tlapm_lsp.ml new file mode 100644 index 00000000..3d654d3e --- /dev/null +++ b/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 () diff --git a/lsp/bin/tlapm_lsp.mli b/lsp/bin/tlapm_lsp.mli new file mode 100644 index 00000000..e69de29b diff --git a/lsp/components.puml b/lsp/components.puml new file mode 100644 index 00000000..63ac3226 --- /dev/null +++ b/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 \ No newline at end of file diff --git a/lsp/lib/const.ml b/lsp/lib/const.ml new file mode 100644 index 00000000..c7a4b480 --- /dev/null +++ b/lsp/lib/const.ml @@ -0,0 +1 @@ +let diagnostic_source = "TLAPM" diff --git a/lsp/lib/const.mli b/lsp/lib/const.mli new file mode 100644 index 00000000..6fe15c8b --- /dev/null +++ b/lsp/lib/const.mli @@ -0,0 +1 @@ +val diagnostic_source : string diff --git a/lsp/lib/docs/doc.ml b/lsp/lib/docs/doc.ml new file mode 100644 index 00000000..9c7f8f66 --- /dev/null +++ b/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) diff --git a/lsp/lib/docs/doc.mli b/lsp/lib/docs/doc.mli new file mode 100644 index 00000000..5b5e0dce --- /dev/null +++ b/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 diff --git a/lsp/lib/docs/doc_actual.ml b/lsp/lib/docs/doc_actual.ml new file mode 100644 index 00000000..dcdf0f8e --- /dev/null +++ b/lsp/lib/docs/doc_actual.ml @@ -0,0 +1,126 @@ +open Util +open Prover + +let prover_mutex = Eio.Mutex.create () + +(* Separated form the type [t] to have the value lazily evaluated. *) +module Parsed = struct + type t = { + nts : Toolbox.tlapm_notif list; + ps : Proof_step.t option; + (** Parsed document structure, a tree of proof steps. + It is obtained by parsing the document and then updated + when obligation proof states are received from the prover. *) + } + + let make ~uri ~(doc_vsn : Doc_vsn.t) ~(ps_prev : Proof_step.t option) ~parser + = + match + Eio.Mutex.use_rw ~protect:true prover_mutex @@ fun () -> + parser ~content:(Doc_vsn.text doc_vsn) + ~filename:(LspT.DocumentUri.to_path uri) + with + | Ok mule -> + let ps = Proof_step.of_module mule ps_prev in + { nts = []; ps } + | Error (loc_opt, msg) -> + let nts = [ Toolbox.notif_of_loc_msg loc_opt msg ] in + { nts; ps = None } + + let ps_if_ready (p : t Lazy.t) = + match Lazy.is_val p with false -> None | true -> (Lazy.force p).ps +end + +type t = { + uri : LspT.DocumentUri.t; + doc_vsn : Doc_vsn.t; + p_ref : int; + ps_prev : Proof_step.t option; + (** Proof steps from the previous version, if there was any.*) + parser : Util.parser_fun; (** Parser to use to parse the modules. *) + parsed : Parsed.t Lazy.t; + (** Parsed document and information derived from it. *) +} + +(** Create new actual document based on the document version [doc_vsn] + and port the current state from the previous actual document + [prev_act], if provided. *) +let make uri doc_vsn prev_act parser = + match prev_act with + | None -> + (* There is no previous active document, we will not try + to move the proof state from there. *) + let parsed = lazy (Parsed.make ~uri ~doc_vsn ~ps_prev:None ~parser) in + { uri; doc_vsn; p_ref = 0; ps_prev = None; parser; parsed } + | Some prev_act -> + (* We have the previous actual document, thus either use its + parsed data, or the data it got from its previous. *) + let ps_prev = + match Parsed.ps_if_ready prev_act.parsed with + | None -> prev_act.ps_prev + | some -> some + in + let parsed = lazy (Parsed.make ~uri ~doc_vsn ~ps_prev ~parser) in + { uri; doc_vsn; p_ref = prev_act.p_ref; ps_prev; parser; parsed } + +let with_parser act parser = make act.uri act.doc_vsn (Some act) parser +let parser act = act.parser +let vsn act = Doc_vsn.version act.doc_vsn +let text act = Doc_vsn.text act.doc_vsn + +let proof_res (act : t) : Doc_proof_res.t = + let parsed = Lazy.force act.parsed in + Doc_proof_res.make parsed.nts parsed.ps + +let locate_proof_range (act : t) range = + let parsed = Lazy.force act.parsed in + Proof_step.locate_proof_range parsed.ps range + +let get_proof_step_details act range = + let parsed = Lazy.force act.parsed in + Proof_step.locate_proof_step parsed.ps range + +let prover_prepare (act : t) next_p_ref = + (* Force it to be parsed, then prepare for the next proof session. *) + match (Lazy.force act.parsed).ps with + | None -> None + | Some _ -> Some { act with p_ref = next_p_ref } + +let prover_add_obl_provers (act : t) (p_ref : int) (obl_id : int) + (provers : string list) = + if act.p_ref = p_ref then + let parsed = Lazy.force act.parsed in + let ps = Proof_step.with_provers parsed.ps p_ref obl_id provers in + let parsed = Lazy.from_val { parsed with ps } in + Some { act with parsed } + else None + +let prover_add_obl (act : t) (p_ref : int) (obl : Toolbox.Obligation.t) = + if act.p_ref = p_ref then + let parsed = Lazy.force act.parsed in + let ps = Proof_step.with_prover_result parsed.ps p_ref obl in + let parsed = Lazy.from_val { parsed with ps } in + Some { act with parsed } + else None + +let prover_add_notif (act : t) p_ref notif = + if act.p_ref = p_ref then + let parsed = Lazy.force act.parsed in + let nts = notif :: parsed.nts in + let parsed = Lazy.from_val { parsed with nts } in + Some { act with parsed } + else None + +let prover_terminated (act : t) p_ref = + if act.p_ref = p_ref then + let parsed = Lazy.force act.parsed in + let ps = Proof_step.with_prover_terminated parsed.ps p_ref in + let parsed = Lazy.from_val { parsed with ps } in + Some { act with parsed } + else None + +let is_obl_final (act : t) p_ref obl_id = + if act.p_ref = p_ref then + let parsed = Lazy.force act.parsed in + Proof_step.is_obl_final parsed.ps p_ref obl_id + else None diff --git a/lsp/lib/docs/doc_actual.mli b/lsp/lib/docs/doc_actual.mli new file mode 100644 index 00000000..4c987f1d --- /dev/null +++ b/lsp/lib/docs/doc_actual.mli @@ -0,0 +1,21 @@ +(** Actual state of the document. *) + +open Util +open Prover + +type t + +val make : LspT.DocumentUri.t -> Doc_vsn.t -> t option -> Util.parser_fun -> t +val with_parser : t -> Util.parser_fun -> t +val parser : t -> Util.parser_fun +val vsn : t -> int +val text : t -> string +val proof_res : t -> Doc_proof_res.t +val locate_proof_range : t -> Range.t -> Range.t +val get_proof_step_details : t -> Range.Position.t -> Proof_step.t option +val prover_prepare : t -> int -> t option +val prover_add_obl_provers : t -> int -> int -> string list -> t option +val prover_add_obl : t -> int -> Toolbox.Obligation.t -> t option +val prover_add_notif : t -> int -> Toolbox.tlapm_notif -> t option +val prover_terminated : t -> int -> t option +val is_obl_final : t -> int -> int -> bool option diff --git a/lsp/lib/docs/doc_proof_res.ml b/lsp/lib/docs/doc_proof_res.ml new file mode 100644 index 00000000..cc51122b --- /dev/null +++ b/lsp/lib/docs/doc_proof_res.ml @@ -0,0 +1,39 @@ +open Prover +open Util + +type t = { nts : Toolbox.tlapm_notif list; ps : Proof_step.t option } + +let make nts ps = { nts; ps } +let empty = { nts = []; ps = None } + +(* Return decorator markers and diagnostics. *) +let as_lsp pr = + (* Collect the diagnostics and decorator markers from the proof steps. *) + let diags, marks = + Proof_step.fold + (fun (diags, marks) ps -> + let mark = Proof_step.as_lsp_tlaps_proof_state_marker ps in + let marks = mark :: marks in + Proof_step.fold_obs + (fun (diags, marks) obl -> + match Obl.as_lsp_diagnostic obl with + | None -> (diags, marks) + | Some diag -> (diag :: diags, marks)) + (diags, marks) ps) + ([], []) pr.ps + in + (* Also add the diagnostics from the notifications. *) + let notif_diags = + List.map + (fun (ntf : Toolbox.tlapm_notif) -> + let severity = + match ntf.sev with + | TlapmNotifError -> LspT.DiagnosticSeverity.Error + | TlapmNotifWarning -> LspT.DiagnosticSeverity.Warning + in + LspT.Diagnostic.create ~message:(`String ntf.msg) + ~range:(Range.as_lsp_range ntf.loc) + ~severity ~source:Const.diagnostic_source ()) + pr.nts + in + (List.concat [ diags; notif_diags ], marks) diff --git a/lsp/lib/docs/doc_proof_res.mli b/lsp/lib/docs/doc_proof_res.mli new file mode 100644 index 00000000..bc807f21 --- /dev/null +++ b/lsp/lib/docs/doc_proof_res.mli @@ -0,0 +1,12 @@ +(** Proof results of a document. Includes the errors returned from the prover + as well as all the proof steps with their current state. + *) + +open Util +open Prover + +type t + +val make : Toolbox.tlapm_notif list -> Proof_step.t option -> t +val empty : t +val as_lsp : t -> LspT.Diagnostic.t list * Structs.TlapsProofStepMarker.t list diff --git a/lsp/lib/docs/doc_vsn.ml b/lsp/lib/docs/doc_vsn.ml new file mode 100644 index 00000000..fa2a6463 --- /dev/null +++ b/lsp/lib/docs/doc_vsn.ml @@ -0,0 +1,9 @@ +type t = { + text : string; (* Contents of the file at the specific version. *) + version : int; +} + +let make txt vsn = { text = txt; version = vsn } +let text tv = tv.text +let version tv = tv.version +let diff_pos a b = Range.first_diff_pos a.text b.text diff --git a/lsp/lib/docs/doc_vsn.mli b/lsp/lib/docs/doc_vsn.mli new file mode 100644 index 00000000..5fa0e4bd --- /dev/null +++ b/lsp/lib/docs/doc_vsn.mli @@ -0,0 +1,11 @@ +(** Versions that are collected after the last prover launch or client + asks for diagnostics. We store some limited number of versions here, + just to cope with async events from the client. + *) + +type t + +val make : string -> int -> t +val text : t -> string +val version : t -> int +val diff_pos : t -> t -> Range.Position.t diff --git a/lsp/lib/docs/docs.ml b/lsp/lib/docs/docs.ml new file mode 100644 index 00000000..e7607a4e --- /dev/null +++ b/lsp/lib/docs/docs.ml @@ -0,0 +1,116 @@ +open Util +open Prover +module Proof_step = Proof_step +module Proof_status = Proof_status +module Doc_proof_res = Doc_proof_res + +type parser_fun = Util.parser_fun +type tk = LspT.DocumentUri.t +type t = { parser : Util.parser_fun; by_uri : Doc.t DocMap.t } + +let empty parser = { parser; by_uri = DocMap.empty } + +let with_parser docs parser = + let by_uri = DocMap.map (fun d -> Doc.with_parser d parser) docs.by_uri in + { parser; by_uri } + +(* Just record the text. It will be processed later, when a prover + command or diagnostics query is issued by the client. *) +let add docs uri vsn txt = + let tv = Doc_vsn.make txt vsn in + let upd = function + | None -> Some (Doc.make uri tv docs.parser) + | Some (doc : Doc.t) -> Some (Doc.add doc tv) + in + { docs with by_uri = DocMap.update uri upd docs.by_uri } + +let rem docs uri = { docs with by_uri = DocMap.remove uri docs.by_uri } + +let latest_vsn docs uri = + match DocMap.find_opt uri docs.by_uri with + | None -> None + | Some doc -> Some (Doc.latest_vsn doc) + +(* Here we merge pending versions with the actual and then run + the supplied function on the prepared doc info. *) +let with_doc_vsn docs uri vsn f = + match DocMap.find_opt uri docs.by_uri with + | None -> (docs, None) + | Some doc -> ( + match Doc.set_actual_vsn doc vsn with + | None -> (docs, None) + | Some doc -> + let doc, res = Doc.with_actual doc f in + let by_uri = DocMap.add uri doc docs.by_uri in + ({ docs with by_uri }, res)) + +(* Calculate proof range by user selection. *) +let suggest_proof_range docs uri range : t * (int * Range.t) option = + match latest_vsn docs uri with + | None -> (docs, None) + | Some vsn -> + with_doc_vsn docs uri vsn @@ fun (doc : Doc.t) (act : Doc_actual.t) -> + let p_range = Doc_actual.locate_proof_range act range in + (doc, act, Some (vsn, p_range)) + +(* Push specific version to the actual, increase the proof_rec and clear the notifications. *) +let prover_prepare docs uri vsn range ~p_ref : + t * (string * Range.t * Doc_proof_res.t) option = + with_doc_vsn docs uri vsn @@ fun (doc : Doc.t) (act : Doc_actual.t) -> + match Doc_actual.prover_prepare act p_ref with + | None -> (doc, act, None) + | Some act -> + let p_range = Doc_actual.locate_proof_range act range in + let res = (Doc_actual.text act, p_range, Doc_actual.proof_res act) in + (doc, act, Some res) + +let prover_add_obl_provers docs uri vsn p_ref obl_id provers = + with_doc_vsn docs uri vsn @@ fun (doc : Doc.t) (act : Doc_actual.t) -> + match Doc_actual.prover_add_obl_provers act p_ref obl_id provers with + | None -> (doc, act, None) + | Some act -> (doc, act, Doc_actual.is_obl_final act p_ref obl_id) + +let prover_add_obl docs uri vsn p_ref (obl : Toolbox.Obligation.t) = + with_doc_vsn docs uri vsn @@ fun (doc : Doc.t) (act : Doc_actual.t) -> + match Doc_actual.prover_add_obl act p_ref obl with + | None -> (doc, act, None) + | Some act -> (doc, act, Doc_actual.is_obl_final act p_ref obl.id) + +let prover_add_notif docs uri vsn p_ref notif = + with_doc_vsn docs uri vsn @@ fun (doc : Doc.t) (act : Doc_actual.t) -> + match Doc_actual.prover_add_notif act p_ref notif with + | None -> (doc, act, None) + | Some act -> (doc, act, Some (Doc_actual.proof_res act)) + +let prover_terminated docs uri vsn p_ref = + with_doc_vsn docs uri vsn @@ fun (doc : Doc.t) (act : Doc_actual.t) -> + match Doc_actual.prover_terminated act p_ref with + | None -> (doc, act, None) + | Some act -> (doc, act, Some (Doc_actual.proof_res act)) + +let get_proof_res docs uri vsn = + with_doc_vsn docs uri vsn @@ fun doc act -> + (doc, act, Some (Doc_actual.proof_res act)) + +let get_proof_res_latest docs uri = + match latest_vsn docs uri with + | None -> (docs, None, None) + | Some latest_vsn -> + let docs, res = get_proof_res docs uri latest_vsn in + (docs, Some latest_vsn, res) + +let get_proof_step_details docs uri vsn range = + with_doc_vsn docs uri vsn @@ fun doc act -> + let res = + match Doc_actual.get_proof_step_details act range with + | None -> None + | Some ps -> Some (Proof_step.as_lsp_tlaps_proof_step_details uri ps) + in + (doc, act, res) + +let get_proof_step_details_latest docs uri range = + match latest_vsn docs uri with + | None -> (docs, None) + | Some latest_vsn -> + let docs, res = get_proof_step_details docs uri latest_vsn range in + (docs, res) diff --git a/lsp/lib/docs/docs.mli b/lsp/lib/docs/docs.mli new file mode 100644 index 00000000..a48b3dab --- /dev/null +++ b/lsp/lib/docs/docs.mli @@ -0,0 +1,89 @@ +(** Here we maintain a list of documents and their revisions. *) + +open Prover +module LspT := Lsp.Types + +module Proof_step : sig + type t +end + +module Proof_status : sig + type t + + val yojson_of_t : t -> Yojson.Safe.t +end + +type t +(** A document store type. *) + +type parser_fun = Util.parser_fun +(** Parser function to use to parse modules. *) + +type tk = LspT.DocumentUri.t +(** Key type to identify documents. *) + +(** Result of an update, returns an actual list of obligations and errors. *) +module Doc_proof_res : sig + type t + + val make : Toolbox.tlapm_notif list -> Proof_step.t option -> t + val empty : t + val as_lsp : t -> LspT.Diagnostic.t list * Structs.TlapsProofStepMarker.t list +end + +val empty : parser_fun -> t +(** Create new empty document store. *) + +val with_parser : t -> parser_fun -> t +(** Set parser function to use. *) + +val add : t -> tk -> int -> string -> t +(** Either add document or its revision. Forgets all previous unused revisions. *) + +val rem : t -> tk -> t +(** Remove a document with all its revisions. *) + +val suggest_proof_range : t -> tk -> Range.t -> t * (int * Range.t) option +(** Suggest proof range based on the user selection. *) + +val prover_prepare : + t -> + tk -> + int -> + Range.t -> + p_ref:int -> + t * (string * Range.t * Doc_proof_res.t) option +(** Increment the prover ref for the specified doc/vsn. *) + +val prover_add_obl_provers : + t -> tk -> int -> int -> int -> string list -> t * bool option +(** Record the provers for an obligation. *) + +val prover_add_obl : + t -> tk -> int -> int -> Toolbox.Obligation.t -> t * bool option +(** Record obligation for the document, clear all the intersecting ones. *) + +val prover_add_notif : + t -> tk -> int -> int -> Toolbox.tlapm_notif -> t * Doc_proof_res.t option +(** Record notification for the document, clear all the intersecting ones. *) + +val prover_terminated : t -> tk -> int -> int -> t * Doc_proof_res.t option +(** Cleanup the incomplete proof states on termination of the prover. *) + +val get_proof_res : t -> tk -> int -> t * Doc_proof_res.t option +(** Get the actual proof results for the specific version. Cleanup them, if needed. *) + +val get_proof_res_latest : t -> tk -> t * int option * Doc_proof_res.t option +(** Get the latest actual proof results. Cleanup them, if needed. *) + +val get_proof_step_details : + t -> + tk -> + int -> + Range.Position.t -> + t * Structs.TlapsProofStepDetails.t option +(** Get the current proof state for the specific obligation. *) + +val get_proof_step_details_latest : + t -> tk -> Range.Position.t -> t * Structs.TlapsProofStepDetails.t option +(** Get the current proof state for the specific obligation at the latest version of the document. *) diff --git a/lsp/lib/docs/obl.ml b/lsp/lib/docs/obl.ml new file mode 100644 index 00000000..d5bdb221 --- /dev/null +++ b/lsp/lib/docs/obl.ml @@ -0,0 +1,264 @@ +open Util +open Prover + +module Role = struct + type t = + | Main (** Main obligation for a proof step. *) + | Aux (** Auxiliary, created by the prover in the BY clause. *) + | Unknown (** Initially all the obligations are of unknown role. *) + | Unexpected + (** Was not received from the parser, but got later from the prover. *) + + let as_string = function + | Main -> "main" + | Aux -> "aux" + | Unknown -> "unknown" + | Unexpected -> "unexpected" +end + +type t = { + role : Role.t; + parsed : Tlapm_lib.Proof.T.obligation option; + (** The obligation as received from the parser. *) + parsed_text_plain : string option Lazy.t; (** Works as a cache. *) + parsed_text_normalized : string option Lazy.t; (** Works as a cache. *) + p_ref : int; + (** We collect proof info in a scope of p_ref only. + For each new p_ref we reset all the prover results. *) + p_obl_id : int option; (** Obligation ID, as assigned by the prover. *) + checking : bool; (** Is obligation checking currently running? *) + by_prover : Toolbox.Obligation.t StrMap.t; + prover_names : string list option; + latest_prover : string option; + status : Proof_status.t; +} + +let obl_to_str obl = + let buf = Buffer.create 100 in + let fmt = Format.formatter_of_buffer buf in + Tlapm_lib.Proof.Fmt.pp_print_obligation fmt obl; + Format.pp_print_flush fmt (); + Buffer.contents buf + +let obl_to_normalized_str obl = + obl_to_str (Tlapm_lib.Backend.Toolbox.normalize true obl) + +let of_parsed_obligation (parsed : Tlapm_lib.Proof.T.obligation) status = + let parsed_text_plain = lazy (Some (obl_to_str parsed)) in + let parsed_text_normalized = lazy (Some (obl_to_normalized_str parsed)) in + { + role = Role.Unknown; + parsed = Some parsed; + parsed_text_plain; + parsed_text_normalized; + p_ref = 0; + p_obl_id = None; + checking = false; + by_prover = StrMap.empty; + prover_names = None; + latest_prover = None; + status; + } + +let reset obl p_ref = + { + obl with + p_ref; + p_obl_id = None; + checking = false; + by_prover = StrMap.empty; + prover_names = None; + latest_prover = None; + status = Proof_status.Pending; + } + +let with_role role obl = { obl with role } +let role obl = obl.role + +(* Should exist in any case. *) +let loc obl = + match obl.parsed with + | None -> + (match obl.latest_prover with + | None -> + assert false (* there should be either parsed info or prover result *) + | Some prover -> StrMap.find prover obl.by_prover) + .loc + | Some parsed -> Range.of_locus_must (Tlapm_lib.Util.get_locus parsed.obl) + +let fingerprint obl = + match obl.parsed with None -> None | Some obl -> obl.fingerprint + +(** Check if this obligation has the specified id. *) +let is_for_obl_id obl p_ref obl_id = + if p_ref = obl.p_ref then + match obl.p_obl_id with None -> false | Some id -> id = obl_id + else false + +(** Either there exist a success result (the latest one), + or we have outputs from all the provers. *) +let is_final obl = + match obl.status with + | Pending | Progress -> false + | Proved | Omitted | Missing -> true + | Failed -> ( + match obl.prover_names with + | None -> false + | Some prover_names -> + let have_prover_result pn = StrMap.mem pn obl.by_prover in + List.for_all have_prover_result prover_names) + +let status obl = if obl.checking then Proof_status.Progress else obl.status +let text_plain obl = Lazy.force obl.parsed_text_plain +let text_normalized obl = Lazy.force obl.parsed_text_normalized + +(** Try to get most detailed status message. + Take it from the prover result, if exist. *) +let latest_status_msg obl = + match obl.latest_prover with + | None -> Proof_status.to_message obl.status + | Some prover -> + Toolbox.tlapm_obl_state_to_string + (StrMap.find prover obl.by_prover).status + +let latest_obl_text obl = + match obl.latest_prover with + | None -> text_normalized obl + | Some prover -> (StrMap.find prover obl.by_prover).obl + +let with_prover_terminated p_ref (obl : t) = + if obl.p_ref <= p_ref then { obl with checking = false } else obl + +let with_prover_obligation p_ref (tlapm_obl : Toolbox.Obligation.t) + (obl : t option) = + (* Create, if we had no such [Obl.t]. *) + let obl = + match obl with + | None -> + { + role = Role.Unexpected; + parsed = None; + parsed_text_plain = lazy None; + parsed_text_normalized = lazy None; + p_ref = 0; + (* To have it reset bellow. *) + p_obl_id = None; + checking = false; + by_prover = StrMap.empty; + prover_names = None; + latest_prover = None; + status = Proof_status.Pending; + } + | Some obl -> obl + in + let obl_add obl = + let obl = + match Toolbox.Obligation.(tlapm_obl.prover) with + | None -> obl + | Some prover -> + { + obl with + by_prover = StrMap.add prover tlapm_obl obl.by_prover; + latest_prover = Some prover; + status = Proof_status.of_tlapm_obl_state tlapm_obl.status; + } + in + { obl with p_obl_id = Some tlapm_obl.id; checking = not (is_final obl) } + in + (* Reset / update / ignore the prover info. *) + if obl.p_ref < p_ref then obl_add (reset obl p_ref) + else if obl.p_ref = p_ref then obl_add obl + else obl + +let with_proof_state_from obl by_fp = + match obl.latest_prover with + | None -> ( + match fingerprint obl with + | None -> obl + | Some fp -> ( + match by_fp fp with + | None -> obl + | Some other -> + { + obl with + p_ref = other.p_ref; + p_obl_id = other.p_obl_id; + checking = other.checking; + by_prover = other.by_prover; + prover_names = other.prover_names; + latest_prover = other.latest_prover; + status = other.status; + })) + | Some _ -> obl + +let with_prover_names p_ref obl_id prover_names obl = + let update obl = + { obl with p_obl_id = Some obl_id; prover_names = Some prover_names } + in + (* Reset / update / ignore the prover info. *) + if obl.p_ref < p_ref then update (reset obl p_ref) + else if obl.p_ref = p_ref then update obl + else obl + +let as_lsp_diagnostic (obl : t) = + match Proof_status.is_diagnostic obl.status with + | true -> + let message = "Obligation: " ^ latest_status_msg obl in + let message = + match latest_obl_text obl with + | None -> message + | Some obl_text -> message ^ "\n" ^ obl_text + in + let message = `String message in + let severity = LspT.DiagnosticSeverity.Error in + let range = Range.as_lsp_range (loc obl) in + let source = Const.diagnostic_source in + Some (LspT.Diagnostic.create ~message ~range ~severity ~source ()) + | false -> None + +let as_lsp_tlaps_proof_obligation_state obl = + let role = Role.as_string obl.role in + let range = Range.as_lsp_range (loc obl) in + let status = Proof_status.to_string obl.status in + let normalized = text_normalized obl in + let results = + let open Toolbox.Obligation in + let some_str s = match s with None -> "?" | Some s -> s in + let make_result o = + let prover = some_str o.prover in + let status = + Proof_status.to_string (Proof_status.of_tlapm_obl_state o.status) + in + let meth = some_str o.meth in + let reason = o.reason in + let obligation = o.obl in + Structs.TlapsProofObligationResult.make ~prover ~meth ~status ~reason + ~obligation + in + let make_pending prover = + Structs.TlapsProofObligationResult.make ~prover ~meth:(some_str None) + ~status:(Proof_status.to_string Pending) + ~reason:None ~obligation:None + in + (* Next, try to retain the order of the provers as it was reported + by the tlaps. Only output pending/planned provers if the + obligation state is not final yet. *) + let final = is_final obl in + match obl.prover_names with + | None -> + List.map (fun (_pn, o) -> make_result o) (StrMap.to_list obl.by_prover) + | Some prover_names -> + let planned pn = + match StrMap.find_opt pn obl.by_prover with + | None -> if final then None else Some (make_pending pn) + | Some o -> Some (make_result o) + in + let unplanned (pn, o) = + if List.mem pn prover_names then None else Some (make_result o) + in + List.append + (List.filter_map planned prover_names) + (List.filter_map unplanned (StrMap.to_list obl.by_prover)) + in + Structs.TlapsProofObligationState.make ~role ~range ~status ~normalized + ~results diff --git a/lsp/lib/docs/obl.mli b/lsp/lib/docs/obl.mli new file mode 100644 index 00000000..90506b9c --- /dev/null +++ b/lsp/lib/docs/obl.mli @@ -0,0 +1,32 @@ +open Util +open Prover + +module Role : sig + type t = Main | Aux | Unknown | Unexpected +end + +type t + +val of_parsed_obligation : Tlapm_lib.Proof.T.obligation -> Proof_status.t -> t +val with_role : Role.t -> t -> t +val with_prover_terminated : int -> t -> t +val with_prover_obligation : int -> Toolbox.Obligation.t -> t option -> t +val with_proof_state_from : t -> (string -> t option) -> t +val with_prover_names : int -> int -> string list -> t -> t +val role : t -> Role.t +val loc : t -> Range.t +val fingerprint : t -> string option +val status : t -> Proof_status.t +val is_for_obl_id : t -> int -> int -> bool +val is_final : t -> bool +val text_plain : t -> string option +val text_normalized : t -> string option +val latest_status_msg : t -> string +val latest_obl_text : t -> string option + +val as_lsp_diagnostic : t -> LspT.Diagnostic.t option +(** Convert to the LSP data structures. *) + +val as_lsp_tlaps_proof_obligation_state : + t -> Structs.TlapsProofObligationState.t +(** Convert to the LSP data structures. *) diff --git a/lsp/lib/docs/proof_status.ml b/lsp/lib/docs/proof_status.ml new file mode 100644 index 00000000..d049057c --- /dev/null +++ b/lsp/lib/docs/proof_status.ml @@ -0,0 +1,58 @@ +open Prover + +type t = Proved | Failed | Omitted | Missing | Pending | Progress + +let of_tlapm_obl_state = function + | Toolbox.ToBeProved -> Progress + | Toolbox.BeingProved -> Progress + | Toolbox.Normalized -> Progress + | Toolbox.Proved -> Proved + | Toolbox.Failed -> Failed + | Toolbox.Interrupted -> Failed + | Toolbox.Trivial -> Proved + | Toolbox.Unknown _ -> Failed + +let to_string = function + | Proved -> "proved" + | Failed -> "failed" + | Omitted -> "omitted" + | Missing -> "missing" + | Pending -> "pending" + | Progress -> "progress" + +let to_message = function + | Failed -> "Proof failed." + | Missing -> "Proof missing." + | Omitted -> "Proof omitted." + | Progress -> "Proving in progress." + | Pending -> "Proof pending." + | Proved -> "Proof checked successfully." + +let to_order = function + | Failed -> 0 + | Missing -> 1 + | Omitted -> 2 + | Progress -> 3 + | Pending -> 4 + | Proved -> 5 + +let of_order = function + | 0 -> Failed + | 1 -> Missing + | 2 -> Omitted + | 3 -> Progress + | 4 -> Pending + | 5 -> Proved + | _ -> failwith "Impossible order" + +let top = Proved +let min a b = of_order (min (to_order a) (to_order b)) +let yojson_of_t t = `String (to_string t) + +let is_diagnostic = function + | Failed -> true + | Missing -> false + | Omitted -> false + | Progress -> false + | Pending -> false + | Proved -> false diff --git a/lsp/lib/docs/proof_status.mli b/lsp/lib/docs/proof_status.mli new file mode 100644 index 00000000..9f45bff4 --- /dev/null +++ b/lsp/lib/docs/proof_status.mli @@ -0,0 +1,15 @@ +open Prover + +type t = Proved | Failed | Omitted | Missing | Pending | Progress + +val of_tlapm_obl_state : Toolbox.tlapm_obl_state -> t +val to_string : t -> string +val to_message : t -> string +val to_order : t -> int +val of_order : int -> t +val top : t +val min : t -> t -> t +val yojson_of_t : t -> Yojson.Safe.t + +val is_diagnostic : t -> bool +(** Returns true, if this state should be shown as a diagnostic. *) diff --git a/lsp/lib/docs/proof_step.ml b/lsp/lib/docs/proof_step.ml new file mode 100644 index 00000000..0e021e01 --- /dev/null +++ b/lsp/lib/docs/proof_step.ml @@ -0,0 +1,555 @@ +open Util +open Prover + +(** We categorize the proof steps just to make the presentation in the UI clearer. *) +module Kind = struct + type t = Module | Struct | Leaf + + let to_string = function + | Module -> "module" + | Struct -> "struct" + | Leaf -> "leaf" +end + +type t = { + kind : Kind.t; + (** Kind/Type of this proof step. + We want to show the proof steps differently based in its type. *) + status_parsed : Proof_status.t option; + (** Status derived at the parse time, if any. + This is for the omitted or error cases. *) + status_derived : Proof_status.t; + (** Derived status. + Here we sum-up the states from all the related obligations and sub-steps. *) + step_loc : Range.t; + (** Location of the entire step. + It starts with a statement/sequent and ends with the BY keyword (inclusive), + not including the listed facts and definitions. In the case of a structured + proof, this ends with the BY keyword of the corresponding QED step. *) + head_loc : Range.t; + (** The location of the proof sequent. + It is always contained within the [step_loc]. + This is shown as a step in the UI. *) + full_loc : Range.t; + (** [step_loc] plus all the BY facts included. + If an obligation is in [full_loc] but not in the [step_loc], + we consider it supplementary (will be shown a bit more hidden). *) + obs : Obl.t RangeMap.t; + (** Obligations associated with this step. + Here we include all the obligations fitting into [full_loc], + but not covered by any of the [sub] steps. *) + sub : t list; (* Sub-steps, if any. *) +} + +(* Derived status is always a minimum of the parsed, the obligations and the sub-steps. *) +let derived_status parsed obs sub = + let parsed = Option.value ~default:Proof_status.top parsed in + let ps_min = Proof_status.min in + let acc = + RangeMap.fold (fun _ obl acc -> ps_min acc (Obl.status obl)) obs parsed + in + List.fold_left (fun acc sub -> ps_min acc sub.status_derived) acc sub + +(* Takes step parameters and a set of remaining unassigned obligations, + constructs the proof step and returns obligations that are left unassigned. *) +let make ~kind ?status_parsed ~step_loc ?head_loc ~full_loc ~sub obs_map = + let intersects_with_full_loc obl_loc _ = Range.intersect obl_loc full_loc in + let intersects_with_step_loc obl_loc = Range.intersect obl_loc step_loc in + let obs, obs_map = RangeMap.partition intersects_with_full_loc obs_map in + let obs = + RangeMap.mapi + (fun obl_range obl -> + match intersects_with_step_loc obl_range with + | true -> Obl.with_role Obl.Role.Main obl + | false -> Obl.with_role Obl.Role.Aux obl) + obs + in + let head_loc = + (* Take the beginning of the first line, if header location is unknown. *) + match head_loc with + | Some head_loc -> head_loc + | None -> Range.(of_points (from step_loc) (from step_loc)) + in + let status_derived = derived_status status_parsed obs sub in + let ps = + { + kind; + status_parsed; + status_derived; + step_loc; + head_loc; + full_loc; + obs; + sub; + } + in + (ps, obs_map) + +let as_lsp_tlaps_proof_state_marker ps = + let status = Proof_status.to_string ps.status_derived in + let range = Range.as_lsp_range ps.head_loc in + let hover = Proof_status.to_message ps.status_derived in + Structs.TlapsProofStepMarker.make ~status ~range ~hover + +let as_lsp_tlaps_proof_step_details uri ps = + let kind = Kind.to_string ps.kind in + let status = Proof_status.to_string ps.status_derived in + let location = + LspT.Location.create ~uri ~range:(Range.as_lsp_range ps.full_loc) + in + let obligations = + List.map + (fun (_, o) -> Obl.as_lsp_tlaps_proof_obligation_state o) + (RangeMap.to_list ps.obs) + in + let sub_count = + let proved, failed, omitted, missing, pending, progress = + List.fold_left + (fun (proved, failed, omitted, missing, pending, progress) sub_ps -> + match sub_ps.status_derived with + | Proved -> (proved + 1, failed, omitted, missing, pending, progress) + | Failed -> (proved, failed + 1, omitted, missing, pending, progress) + | Omitted -> (proved, failed, omitted + 1, missing, pending, progress) + | Missing -> (proved, failed, omitted, missing + 1, pending, progress) + | Pending -> (proved, failed, omitted, missing, pending + 1, progress) + | Progress -> (proved, failed, omitted, missing, pending, progress + 1)) + (0, 0, 0, 0, 0, 0) ps.sub + in + Structs.CountByStepStatus.make ~proved ~failed ~omitted ~missing ~pending + ~progress + in + Structs.TlapsProofStepDetails.make ~kind ~status ~location ~obligations + ~sub_count + +(* Recursively collect all the fingerprinted obligations. + This is used to transfer proof state from the + previous to the new document version. *) +let obl_by_fp ps = + let tbl = Hashtbl.create 1024 in + match ps with + | None -> tbl + | Some ps -> + let rec traverse ps = + let add_by_fp (o : Obl.t) = + match Obl.fingerprint o with + | None -> () + | Some fp -> Hashtbl.add tbl fp o + in + RangeMap.iter (fun _ o -> add_by_fp o) ps.obs; + List.iter traverse ps.sub + in + traverse ps; + tbl + +(** Just make a flat list of all the proof steps. *) +let flatten ps = + let rec traverse ps = ps :: List.flatten (List.map traverse ps.sub) in + match ps with None -> [] | Some ps -> traverse ps + +(** Iterate over the proof steps. *) +let fold f acc ps = + let rec fold_rec acc ps = + let acc = f acc ps in + List.fold_left fold_rec acc ps.sub + in + match ps with None -> acc | Some ps -> fold_rec acc ps + +(** Iterate over obligations of a particular proof step. *) +let fold_obs f acc ps = RangeMap.fold (fun _ obl acc -> f acc obl) ps.obs acc + +module Acc = struct + type t = { file : string; obs_map : Obl.t RangeMap.t } + + let some (x, acc) = (Some x, acc) + let for_file file acc = file = acc.file +end + +let if_in_file wrapped file fn = + match Tlapm_lib.Util.query_locus wrapped with + | Some loc when loc.file = file -> fn (Range.of_locus_must loc) + | Some _ -> None + | None -> None + +let if_in_file_acc wrapped acc fn = + match Tlapm_lib.Util.query_locus wrapped with + | Some loc when Acc.for_file loc.file acc -> fn (Range.of_locus_must loc) acc + | Some _ -> (None, acc) + | None -> (None, acc) + +let rec of_proof step_loc sq_range (proof : Tlapm_lib.Proof.T.proof) acc : + t * Acc.t = + let open Tlapm_lib in + let kind, sub, status_parsed, suppl_loc, acc = + match Property.unwrap proof with + | Proof.T.Obvious -> (Kind.Leaf, [], None, None, acc) + | Proof.T.Omitted omission -> + let status_parsed = + match omission with + | Explicit -> Proof_status.Omitted + | Implicit -> Proof_status.Missing + | Elsewhere _loc -> Proof_status.Omitted + in + (Kind.Leaf, [], Some status_parsed, None, acc) + | Proof.T.By (usable, _only) -> + let wrapped_join_ranges base list = + List.fold_left + (fun acc d -> + match Range.of_wrapped d with + | None -> acc + | Some r -> Range.join acc r) + base list + in + let suppl_range = step_loc in + let suppl_range = wrapped_join_ranges suppl_range usable.defs in + let suppl_range = wrapped_join_ranges suppl_range usable.facts in + (Kind.Leaf, [], None, Some suppl_range, acc) + | Proof.T.Steps (steps, qed_step) -> + let acc, sub = + List.fold_left_map + (fun acc s -> + let s, acc = of_step s acc in + (acc, s)) + acc steps + in + let sub = List.filter_map Fun.id sub in + let qed, acc = of_qed_step qed_step acc in + let sub = sub @ [ qed ] in + let suppl_loc = + List.fold_left + (fun acc sub_ps -> Range.join acc sub_ps.full_loc) + step_loc sub + in + (Kind.Struct, sub, None, Some suppl_loc, acc) + | Proof.T.Error _ -> (Kind.Leaf, [], Some Proof_status.Failed, None, acc) + in + let head_loc = + match sq_range with + | Some sq_range -> Some Range.(of_points (from step_loc) (till sq_range)) + | None -> None + in + let full_loc = + match suppl_loc with + | None -> step_loc + | Some suppl_loc -> Range.join step_loc suppl_loc + in + let st, obs_map = + make ~kind ?status_parsed ~step_loc ?head_loc ~full_loc ~sub acc.obs_map + in + (st, { acc with obs_map }) + +and of_implicit_proof_step step_loc suppl_locs (acc : Acc.t) : t * Acc.t = + let full_loc = List.fold_left Range.join step_loc suppl_locs in + let st, obs_map = + make ~kind:Kind.Leaf ~step_loc ~head_loc:step_loc ~full_loc ~sub:[] + acc.obs_map + in + (st, { acc with obs_map }) + +and of_step (step : Tlapm_lib.Proof.T.step) acc : t option * Acc.t = + let open Tlapm_lib in + match Property.unwrap step with + | Proof.T.Hide _ -> (None, acc) + | Proof.T.Define _ -> (None, acc) + | Proof.T.Assert (sequent, proof) -> + Acc.some + (of_proof + (Range.of_wrapped_must step) + (Range.of_wrapped sequent.active) + proof acc) + | Proof.T.Suffices (sequent, proof) -> + Acc.some + (of_proof + (Range.of_wrapped_must step) + (Range.of_wrapped sequent.active) + proof acc) + | Proof.T.Pcase (expr, proof) -> + Acc.some + (of_proof + (Range.of_wrapped_must step) + (Range.of_wrapped expr) proof acc) + | Proof.T.Pick (_bounds, expr, proof) -> + Acc.some + (of_proof + (Range.of_wrapped_must step) + (Range.of_wrapped expr) proof acc) + | Proof.T.Use (_, _) -> (None, acc) + | Proof.T.Have expr -> + let suppl_locs = List.filter_map Range.of_wrapped [ expr ] in + Acc.some + (of_implicit_proof_step (Range.of_wrapped_must step) suppl_locs acc) + | Proof.T.Take bounds -> + let suppl_locs = + List.filter_map (fun (hint, _, _) -> Range.of_wrapped hint) bounds + in + Acc.some + (of_implicit_proof_step (Range.of_wrapped_must step) suppl_locs acc) + | Proof.T.Witness exprs -> + let suppl_locs = List.filter_map Range.of_wrapped exprs in + Acc.some + (of_implicit_proof_step (Range.of_wrapped_must step) suppl_locs acc) + | Proof.T.Forget _ -> (None, acc) + +and of_qed_step (qed_step : Tlapm_lib.Proof.T.qed_step) acc : t * Acc.t = + match Tlapm_lib.Property.unwrap qed_step with + | Tlapm_lib.Proof.T.Qed proof -> + let open Tlapm_lib in + let qed_loc = Property.query qed_step Proof.Parser.qed_loc_prop in + let qed_range = Range.of_locus_opt qed_loc in + of_proof (Range.of_wrapped_must qed_step) qed_range proof acc + +(* This is internal function for traversing the modules and module units recursively. *) +let rec of_submod (mule : Tlapm_lib.Module.T.mule) (acc : Acc.t) : + t option * Acc.t = + let open Tlapm_lib in + if_in_file_acc mule acc @@ fun step_loc acc -> + let mule = Property.unwrap mule in + let mu_step mu (sub, acc) = + let st, acc = of_mod_unit mu acc in + let sub = match st with None -> sub | Some st -> st :: sub in + (sub, acc) + in + let sub, acc = List.fold_right mu_step mule.body ([], acc) in + match sub with + | [] -> (None, acc) + | _ -> + let st, obs_map = + make ~kind:Kind.Module ~step_loc ~full_loc:step_loc ~sub acc.obs_map + in + (Some st, { acc with obs_map }) + +and of_mod_unit (mod_unit : Tlapm_lib.Module.T.modunit) acc : t option * Acc.t = + let open Tlapm_lib in + let open Tlapm_lib.Module.T in + if_in_file_acc mod_unit acc @@ fun mod_unit_loc acc -> + match Property.unwrap mod_unit with + | Constants _ -> (None, acc) + | Recursives _ -> (None, acc) + | Variables _ -> (None, acc) + | Definition _ -> (None, acc) + | Axiom _ -> (None, acc) + | Theorem (_name, sq, _naxs, _prf, prf_orig, _sum) -> + Acc.some (of_proof mod_unit_loc (Range.of_wrapped sq.active) prf_orig acc) + | Submod sm -> of_submod sm acc + | Mutate _ -> (None, acc) + | Anoninst _ -> (None, acc) + +(* This is the entry point for creating proof steps from a module. + It will return None, if the module has no provable statements. + Otherwise it will return a proof step representing all the module + with all the sub-steps for the theorems, and so on. *) +let of_module (mule : Tlapm_lib.Module.T.mule) prev : t option = + match mule.core.stage with + | Final fin -> + let prev_obs = obl_by_fp prev in + let file = + match Tlapm_lib.Util.query_locus mule with + | None -> failwith "of_module, has no file location" + | Some m_locus -> m_locus.file + in + let mule_obl (o : Tlapm_lib.Proof.T.obligation) = + (* Keep only the obligations from the current file. *) + if_in_file o.obl file @@ fun o_range -> + (* We will use the fingerprints to retain the + proof status between the modifications. *) + let o = + match o.fingerprint with + | None -> Tlapm_lib.Backend.Fingerprints.write_fingerprint o + | Some _ -> o + in + let o = Obl.of_parsed_obligation o Proof_status.Pending in + let o = Obl.with_proof_state_from o (Hashtbl.find_opt prev_obs) in + Some (o_range, o) + in + let obs = fin.final_obs in + let obs = List.filter_map mule_obl (Array.to_list obs) in + let obs_map = RangeMap.of_list obs in + let acc = Acc.{ file; obs_map } in + let step_opt, acc = of_submod mule acc in + assert (RangeMap.is_empty acc.obs_map); + step_opt + | Parsed -> failwith "of_module, parsed" + | _ -> failwith "of_module, non final" + +let with_prover_terminated (ps : t option) p_ref = + let rec traverse ps = + let sub = List.map traverse ps.sub in + let obs = RangeMap.map (Obl.with_prover_terminated p_ref) ps.obs in + let status_derived = derived_status ps.status_parsed obs sub in + { ps with sub; obs; status_derived } + in + match ps with None -> None | Some ps -> Some (traverse ps) + +let with_provers (ps : t option) p_ref obl_id prover_names = + let rec traverse ps = + let found = ref false in + let try_obl obl = + if (not !found) && Obl.is_for_obl_id obl p_ref obl_id then ( + found := true; + Obl.with_prover_names p_ref obl_id prover_names obl) + else obl + in + let try_sub ps = + if not !found then ( + let ps, sub_found = traverse ps in + if sub_found then found := true; + ps) + else ps + in + let obs = RangeMap.map try_obl ps.obs in + let sub = List.map try_sub ps.sub in + let ps = { ps with obs; sub } in + (ps, !found) + in + match ps with + | None -> None + | Some ps -> + let ps, _ = traverse ps in + Some ps + +let with_prover_result (ps : t option) p_ref (pr : Toolbox.Obligation.t) = + let rec traverse (ps : t) (pr : Toolbox.Obligation.t) = + if Range.intersect ps.full_loc pr.loc then + let apply_to_sub acc sub_ps = + match acc with + | true -> (* Already found previously. *) (acc, sub_ps) + | false -> ( + (* Not found yet, try the depth-first search. *) + match traverse sub_ps pr with + | None -> (acc, sub_ps) + | Some sub_ps -> (true, sub_ps)) + in + let found, sub = List.fold_left_map apply_to_sub false ps.sub in + let ps = + match found with + | true -> { ps with sub } + | false -> + let upd o = Some (Obl.with_prover_obligation p_ref pr o) in + let obs = RangeMap.update pr.loc upd ps.obs in + { ps with obs } + in + let status_derived = derived_status ps.status_parsed ps.obs ps.sub in + Some { ps with status_derived } + else None + in + match ps with + | None -> None + | Some ps -> ( + match traverse ps pr with None -> Some ps | Some ps -> Some ps) + +(* Find the deepest proof step that intersects line-wise with the specified position. *) +let locate_proof_step (ps : t option) (position : Range.Position.t) : t option = + let rec traverse ps = + if Range.line_covered ps.full_loc position then + match List.find_map traverse ps.sub with + | None -> Some ps + | Some sub_ps -> Some sub_ps + else None + in + match ps with None -> None | Some ps -> traverse ps + +let locate_proof_range (ps : t option) (range : Range.t) : Range.t = + let ps_from = locate_proof_step ps (Range.from range) in + let ps_till = locate_proof_step ps (Range.till range) in + match (ps_from, ps_till) with + | None, None -> Range.of_all + | Some ps_from, None -> ps_from.full_loc + | None, Some ps_till -> ps_till.full_loc + | Some ps_from, Some ps_till -> Range.join ps_from.full_loc ps_till.full_loc + +let is_obl_final (ps : t option) p_ref obl_id = + let rec traverse ps = + let with_obl_id r = + Obl.is_for_obl_id (RangeMap.find r ps.obs) p_ref obl_id + in + match RangeMap.find_first_opt with_obl_id ps.obs with + | None -> List.find_map traverse ps.sub + | Some (_, o) -> Some (Obl.is_final o) + in + match ps with None -> None | Some ps -> traverse ps + +let%test_unit "determine proof steps" = + let mod_file = "test_obl_expand.tla" in + let mod_text = + String.concat "\n" + [ + "---- MODULE test_obl_expand ----"; + "EXTENDS FiniteSetTheorems"; + "THEOREM FALSE"; + " <1>1. TRUE OBVIOUS"; + " <1>2. TRUE"; + " <1>3. TRUE"; + " <1>q. QED BY <1>1, <1>2, <1>3"; + "THEOREM FALSE"; + " <1>q. QED"; + " <2>1. TRUE"; + " <2>q. QED BY <2>1"; + " ----- MODULE sub ------"; + " VARIABLE X"; + " LEMMA X = X"; + " ======================="; + "===="; + ] + in + let mule = + Result.get_ok + (Parser.module_of_string ~content:mod_text ~filename:mod_file + ~loader_paths:[]) + in + let ps = of_module mule None in + match flatten ps with + | [ + _m_test_obl_expand; + _th1; + _th1_11; + _th1_12; + _th1_13; + _th1_1q; + _th2; + _th2_1q; + _th2_1q_21; + _th2_1q_2q; + _m_sub; + _th3; + ] as all -> ( + List.iteri + (fun i ps -> + Format.printf + "Step[%d]: |obs|=%d, full_loc=%s, step_loc=%s head_loc=%s\n" i + (RangeMap.cardinal ps.obs) + (Range.string_of_range ps.full_loc) + (Range.string_of_range ps.step_loc) + (Range.string_of_range ps.head_loc)) + all; + assert (RangeMap.cardinal _th2_1q_2q.obs = 2); + assert ( + RangeMap.cardinal + (RangeMap.filter + (fun _ o -> Obl.role o = Obl.Role.Main) + _th2_1q_2q.obs) + = 1); + let _, _th2_1q_2q_obl = RangeMap.choose _th2_1q_2q.obs in + match Obl.text_normalized _th2_1q_2q_obl with + | Some "ASSUME TRUE \nPROVE FALSE" -> () + | Some s -> failwith (Format.sprintf "Unexpected %s" s) + | None -> failwith "Unexpected none") + | pss -> + failwith + (Format.sprintf "unexpected, number of steps=%d" (List.length pss)) + +let%test_unit "check if parsing works with nested local instances." = + let mod_file = "test_loc_ins.tla" in + let mod_text = + String.concat "\n" + [ + (* Just to keep the items wrapped by line. *) + "---- MODULE test_loc_ins ----"; + "LOCAL INSTANCE FiniteSets"; + "===="; + ] + in + let _mule = + Result.get_ok + (Parser.module_of_string ~content:mod_text ~filename:mod_file + ~loader_paths:[]) + in + () diff --git a/lsp/lib/docs/proof_step.mli b/lsp/lib/docs/proof_step.mli new file mode 100644 index 00000000..7325c665 --- /dev/null +++ b/lsp/lib/docs/proof_step.mli @@ -0,0 +1,25 @@ +(** Proof step, as it is displayed in the editor. + The proof steps are obtained by parsing the TLAPS source file. + Later the proof obligation info is added to the tree as they are + obtained from the prover. + *) + +open Util +open Prover + +type t + +val of_module : Tlapm_lib.Module.T.mule -> t option -> t option +val with_prover_terminated : t option -> int -> t option +val with_prover_result : t option -> int -> Toolbox.Obligation.t -> t option +val with_provers : t option -> int -> int -> string list -> t option +val locate_proof_step : t option -> Range.Position.t -> t option +val locate_proof_range : t option -> Range.t -> Range.t +val is_obl_final : t option -> int -> int -> bool option +val flatten : t option -> t list +val fold : ('a -> t -> 'a) -> 'a -> t option -> 'a +val fold_obs : ('a -> Obl.t -> 'a) -> 'a -> t -> 'a +val as_lsp_tlaps_proof_state_marker : t -> Structs.TlapsProofStepMarker.t + +val as_lsp_tlaps_proof_step_details : + LspT.DocumentUri.t -> t -> Structs.TlapsProofStepDetails.t diff --git a/lsp/lib/docs/util.ml b/lsp/lib/docs/util.ml new file mode 100644 index 00000000..30d7d660 --- /dev/null +++ b/lsp/lib/docs/util.ml @@ -0,0 +1,24 @@ +(** Obligation reference consists of the proof session reference (p_ref) + and the obligation id (obl_id) as assigned by the TLAPS. This reference + is unique across proof attempts. + *) +module OblRef = struct + type t = { p_ref : int; obl_id : int } + + let make ~p_ref ~obl_id = { p_ref; obl_id } + + let compare a b = + let p_ref_cmp = Stdlib.compare a.p_ref b.p_ref in + if p_ref_cmp = 0 then Stdlib.compare a.obl_id b.obl_id else p_ref_cmp +end + +module LspT = Lsp.Types +module DocMap = Map.Make (LspT.DocumentUri) +module OblMap = Map.Make (OblRef) +module StrMap = Map.Make (String) +module RangeMap = Map.Make (Range) + +type parser_fun = + content:string -> + filename:string -> + (Tlapm_lib.Module.T.mule, string option * string) result diff --git a/lsp/lib/dune b/lsp/lib/dune new file mode 100644 index 00000000..77dd70d9 --- /dev/null +++ b/lsp/lib/dune @@ -0,0 +1,14 @@ +(library + (name tlapm_lsp_lib) + (optional) ; Only build, if eio is available, which is only the case for ocaml > 5. + (enabled_if + (>= %{ocaml_version}, "5.0.0")) + (libraries tlapm_lib lsp eio_main dune-build-info re2) + (inline_tests + (deps "../test/tlapm_mock.sh" "../../src/tlapm.exe") + ; (flags -only-test docs/proof_step.ml -verbose) + ) + (preprocess + (pps ppx_inline_test))) + +(include_subdirs qualified) diff --git a/lsp/lib/parser/parser.ml b/lsp/lib/parser/parser.ml new file mode 100644 index 00000000..457c3ae1 --- /dev/null +++ b/lsp/lib/parser/parser.ml @@ -0,0 +1,3 @@ +let module_of_string ~content ~filename ~loader_paths = + Tlapm_lib.module_of_string ~content ~filename ~loader_paths + ~prefer_stdlib:true diff --git a/lsp/lib/parser/parser.mli b/lsp/lib/parser/parser.mli new file mode 100644 index 00000000..c89e24ea --- /dev/null +++ b/lsp/lib/parser/parser.mli @@ -0,0 +1,9 @@ +(** Responsible for parsing the TLA+ documents. + TODO: SANY integration should be added here as well. + *) + +val module_of_string : + content:string -> + filename:string -> + loader_paths:string list -> + (Tlapm_lib.Module.T.mule, string option * string) result diff --git a/lsp/lib/prover/progress.ml b/lsp/lib/prover/progress.ml new file mode 100644 index 00000000..7711e6e2 --- /dev/null +++ b/lsp/lib/prover/progress.ml @@ -0,0 +1,183 @@ +module LspT = Lsp.Types +module OblIdSet = Set.Make (Int) + +type t = { + p_ref : int; + token : LspT.ProgressToken.t; + started : bool; + ended : bool; + obl_count : int option; (* Total number of proof obligations. *) + obl_done : OblIdSet.t; (* Obligations already checked. *) +} + +let title = "Checking TLA+ proofs" + +let message pr = + match pr.obl_count with + | None -> "Obligation count unknown." + | Some total -> + Format.sprintf "%d of %d obligations checked" + (OblIdSet.cardinal pr.obl_done) + total + +let percentage pr = + match pr.obl_count with + | None -> 0 + | Some 0 -> 100 + | Some obl_count -> OblIdSet.cardinal pr.obl_done * 100 / obl_count + +let make_token p_ref = `String (Format.sprintf "tlapm_lsp-p_ref-%d" p_ref) + +let reset p_ref ended = + { + p_ref; + token = make_token p_ref; + started = ended; + ended; + obl_count = None; + obl_done = OblIdSet.empty; + } + +(* --------------- Functions creating LSP packets. --------------- *) + +let make_lsp_req_create pr = + Lsp.Server_request.WorkDoneProgressCreate + (LspT.WorkDoneProgressCreateParams.create ~token:pr.token) + +let make_lsp_notif_begin pr = + let message = message pr in + let percentage = percentage pr in + let value = + Lsp.Progress.Begin + (LspT.WorkDoneProgressBegin.create ~cancellable:true ~message ~percentage + ~title ()) + in + Lsp.Server_notification.WorkDoneProgress + (LspT.ProgressParams.create ~token:pr.token ~value) + +let make_lsp_notif_report pr = + let message = message pr in + let percentage = percentage pr in + let value = + Lsp.Progress.Report + (LspT.WorkDoneProgressReport.create ~cancellable:true ~message ~percentage + ()) + in + Lsp.Server_notification.WorkDoneProgress + (LspT.ProgressParams.create ~token:pr.token ~value) + +let make_lsp_notif_end pr = + let message = message pr in + let value = Lsp.Progress.End (LspT.WorkDoneProgressEnd.create ~message ()) in + Lsp.Server_notification.WorkDoneProgress + (LspT.ProgressParams.create ~token:pr.token ~value) + +(* These should be provided by the session to interact with the environment. *) + +module type Callbacks = sig + type p := t + type t + + val next_req_id : t -> Jsonrpc.Id.t * t + val lsp_send : t -> Jsonrpc.Packet.t -> t + val with_progress : t -> (t -> p -> t * p) -> t +end + +module Make (CB : Callbacks) = struct + let send_notif cb_state lsp_notif = + let rpc_notif = Lsp.Server_notification.to_jsonrpc lsp_notif in + let rpc_packet = Jsonrpc.Packet.Notification rpc_notif in + CB.lsp_send cb_state rpc_packet + + let send_req cb_state lsp_req = + let req_id, cb_state = CB.next_req_id cb_state in + let rpc_req = Lsp.Server_request.to_jsonrpc_request lsp_req ~id:req_id in + let rpc_packet = Jsonrpc.Packet.Request rpc_req in + CB.lsp_send cb_state rpc_packet + + (* --------------- The main functionality. --------------- *) + + let make () = reset 0 true + let is_latest pr token = make_token pr.p_ref = token + + (* End the previous progress bar, if not ended yet, and create a new one. *) + let proof_started ~p_ref cb_state = + CB.with_progress cb_state @@ fun cb_state pr -> + if pr.p_ref < p_ref then + let cb_state = + match pr.ended with + | true -> cb_state + | false -> send_notif cb_state (make_lsp_notif_end pr) + in + let pr = reset p_ref false in + let cb_state = send_req cb_state (make_lsp_req_create pr) in + (cb_state, pr) + else (cb_state, pr) + + let obl_count ~p_ref ~obl_count cb_state = + CB.with_progress cb_state @@ fun cb_state pr -> + if p_ref = pr.p_ref then + let was_started = pr.started in + let pr = { pr with obl_count = Some obl_count; started = true } in + let cb_state = + match was_started with + | true -> send_notif cb_state (make_lsp_notif_report pr) + | false -> send_notif cb_state (make_lsp_notif_begin pr) + in + (cb_state, pr) + else (cb_state, pr) + + let obligation_done ~p_ref ~(obl_id : int) cb_state = + CB.with_progress cb_state @@ fun cb_state pr -> + if + p_ref = pr.p_ref && pr.started && (not pr.ended) + && not (OblIdSet.mem obl_id pr.obl_done) + then + let pr = { pr with obl_done = OblIdSet.add obl_id pr.obl_done } in + let cb_state = send_notif cb_state (make_lsp_notif_report pr) in + (cb_state, pr) + else (cb_state, pr) + + let proof_ended ~p_ref cb_state = + CB.with_progress cb_state @@ fun cb_state pr -> + if p_ref = pr.p_ref && pr.ended = false then + let pr = { pr with ended = true } in + let cb_state = send_notif cb_state (make_lsp_notif_end pr) in + (cb_state, pr) + else (cb_state, pr) +end + +let%test_module "progress reporting tests" = + (module struct + type tst_t = { req_id : int; sent : Jsonrpc.Packet.t list; progress : t } + + module TestCB = struct + type t = tst_t + + let next_req_id cb = + let next = cb.req_id + 1 in + (`Int next, { cb with req_id = next }) + + let lsp_send cb pkt = { cb with sent = pkt :: cb.sent } + + let with_progress st f = + let st, progress = f st st.progress in + { st with progress } + end + + module TestPr = Make (TestCB) + + let fresh = { req_id = 0; sent = []; progress = TestPr.make () } + + let%test_unit "basic" = + let cb = fresh in + let p_ref = 1 in + let cb = TestPr.proof_started ~p_ref cb in + let cb = TestPr.obl_count ~p_ref ~obl_count:10 cb in + let cb = TestPr.obligation_done ~p_ref ~obl_id:2 cb in + let cb = TestPr.obligation_done ~p_ref ~obl_id:5 cb in + let cb = TestPr.proof_ended ~p_ref cb in + match List.length cb.sent with + | 5 -> () + | x -> failwith (Format.sprintf "got unexpected message count: %d" x) + end) diff --git a/lsp/lib/prover/progress.mli b/lsp/lib/prover/progress.mli new file mode 100644 index 00000000..cc7329f3 --- /dev/null +++ b/lsp/lib/prover/progress.mli @@ -0,0 +1,37 @@ +(** Maintains the proof progress in the client app. Here we use the + server initiated progress and cancellation support, because the + VSCode don't support the client-initiated workDoneProgress + with LSP. *) + +module LspT := Lsp.Types + +type t + +module type Callbacks = sig + type p := t + type t + + val next_req_id : t -> Jsonrpc.Id.t * t + val lsp_send : t -> Jsonrpc.Packet.t -> t + val with_progress : t -> (t -> p -> t * p) -> t +end + +module Make (CB : Callbacks) : sig + val make : unit -> t + (** Create new instance of progress tracker. *) + + val is_latest : t -> LspT.ProgressToken.t -> bool + (** Checks if the token is of the last progress. *) + + val proof_started : p_ref:int -> CB.t -> CB.t + (** Called when new TLAPM run is initiated. *) + + val obl_count : p_ref:int -> obl_count:int -> CB.t -> CB.t + (** Called when a number of obligations is received from the TLAPM. *) + + val obligation_done : p_ref:int -> obl_id:int -> CB.t -> CB.t + (** Called when some proof obligation state change is received from TLAPM. *) + + val proof_ended : p_ref:int -> CB.t -> CB.t + (** Called when the TLAPM terminates. *) +end diff --git a/lsp/lib/prover/prover.ml b/lsp/lib/prover/prover.ml new file mode 100644 index 00000000..dfc7f4bb --- /dev/null +++ b/lsp/lib/prover/prover.ml @@ -0,0 +1,293 @@ +(* cSpell:words obligationsnumber getcwd nonblocking submatches *) + +(** Max size for the read buffer, a line should fit into it.*) +let read_buf_max_size = 1024 * 1024 + +module LspT = Lsp.Types +module Progress = Progress +module Toolbox = Toolbox + +(* ***** Prover process management ****************************************** *) + +(** + Returns the tlapm executable path or error, if there is no such in known places. + If installed, both files are in the same dir: + - .../bin/tlapm + - .../bin/tlapm_lsp + Otherwise, if that's development environment, the files are: + - .../src/tlapm.exe + - .../lsp/bin/tlapm_lsp.exe + And during the inline tests: + - .../src/tlapm.exe + - .../lsp/lib/.tlapm_lsp_lib.inline-tests/inline_test_runner_tlapm_lsp_lib.exe + *) +let tlapm_exe () = + let open Filename in + let this_exe = Sys.executable_name in + let this_abs = + match is_relative this_exe with + | true -> concat current_dir_name this_exe + | false -> this_exe + in + let tlapm_in_bin = concat (dirname this_abs) "tlapm" in + let tlapm_in_src = + let base_dir = dirname @@ dirname @@ dirname this_abs in + concat (concat base_dir "src") "tlapm.exe" + in + let tlapm_in_tst = + let base_dir = dirname @@ dirname @@ dirname @@ dirname this_abs in + concat (concat base_dir "src") "tlapm.exe" + in + let paths_to_check = [ tlapm_in_bin; tlapm_in_src; tlapm_in_tst ] in + match List.find_opt Sys.file_exists paths_to_check with + | Some path -> Ok path + | None -> + Error + ("tlapm not found, expected it among these: " + ^ String.concat ", " paths_to_check) + +(* Currently forked tlapm process. *) +type tf = { + proc : [ `Generic | `Unix ] Eio.Process.ty Eio__.Std.r; + complete : unit Eio.Promise.or_exn; + cancel : unit Eio.Promise.u; +} + +type t = { + sw : Eio.Switch.t; + fs : Eio__.Fs.dir_ty Eio.Path.t; + mgr : Eio_unix.Process.mgr_ty Eio.Process.mgr; + forked : tf option; +} + +(** Create instance of a prover process manager. *) +let create sw fs mgr = { sw; fs; mgr; forked = None } + +(** Cancel (all) the preceding prover instances. *) +let cancel_all st = + match st.forked with + | None -> st + | Some { proc; complete; cancel; _ } -> + Eio.Process.signal proc Sys.sigint; + (match Eio.Process.await proc with + | `Exited x -> Eio.traceln "[TLAPM] Process exited %d" x + | `Signaled x -> + Eio.traceln "[TLAPM] Process signalled %d" x; + Eio.Promise.resolve cancel ()); + (match Eio.Promise.await complete with + | Ok () -> Eio.traceln "[TLAPM] Fiber exited" + | Error e -> + Eio.traceln "[TLAPM] Fiber failed with %s" (Printexc.to_string e)); + { st with forked = None } + +(* Start a fiber to read the tlapm stdout asynchronously. *) +let fork_read sw stream r w cancel = + let fib_read () = + Eio.Flow.close w; + let rec read_fun' br acc = + let line = Eio.Buf_read.line br in + Eio.traceln "[TLAPM][O] %s" line; + let acc' = Toolbox.parse_line line acc stream in + if Eio.Buf_read.at_end_of_input br then () else read_fun' br acc' + in + let read_fun br = read_fun' br Toolbox.parse_start in + let read_result = + Eio.Buf_read.parse ~initial_size:5 ~max_size:read_buf_max_size read_fun r + in + (match read_result with + | Ok () -> Eio.traceln "[TLAPM] process completed." + | Error (`Msg msg) -> Eio.traceln "[TLAPM] process failed with: %s" msg); + Eio.Flow.close r; + Eio.traceln "[TLAPM] read fiber completed." + in + let fib_cancel () = Eio.Promise.await cancel in + Eio.Fiber.fork_promise ~sw @@ fun () -> + Eio.Fiber.first fib_read fib_cancel; + stream TlapmTerminated; + Eio.traceln "[TLAPM] main fiber completed" + +(** Start the TLAPM process and attach the reader fiber to it. *) +let start_async_with_exec st doc_uri doc_text range paths events_adder + executable = + let mod_path = LspT.DocumentUri.to_path doc_uri in + let mod_dir = + let open Eio.Path in + st.fs / Filename.dirname mod_path + in + let mod_name = Filename.basename mod_path in + let stdin = Eio.Flow.string_source doc_text in + let r, w = Eio.Process.pipe st.mgr ~sw:st.sw in + let proc_args = + [ + (* First arg s ignored, if executable is specified. *) + executable; + "--toolbox"; + string_of_int (Range.line_from range); + string_of_int (Range.line_till range); + "--toolbox-vsn"; + "2"; + (* "--verbose"; *) + "--printallobs"; + "--prefer-stdlib"; + "--stdin"; + mod_name; + ] + in + let proc_args = + List.append proc_args (List.flatten (List.map (fun p -> [ "-I"; p ]) paths)) + in + Eio.traceln "[TLAPM] cwd=%s, command: %s" + (Eio.Path.native_exn mod_dir) + (String.concat " " proc_args); + let proc = + Eio.Process.spawn st.mgr ~sw:st.sw ~executable ~cwd:mod_dir ~stdin ~stdout:w + ~stderr:w proc_args + in + let cancel_p, cancel_r = Eio.Promise.create () in + let complete = fork_read st.sw events_adder r w cancel_p in + let forked = { proc; complete; cancel = cancel_r } in + { st with forked = Some forked } + +(* Run the tlapm prover, cancel the preceding one, if any. *) +let start_async st doc_uri doc_text range paths events_adder + ?(tlapm_locator = tlapm_exe) () = + Eio.traceln "[TLAPM][I]\n%s" doc_text; + match tlapm_locator () with + | Ok executable -> + let st' = cancel_all st in + Ok + (start_async_with_exec st' doc_uri doc_text range paths events_adder + executable) + | Error reason -> Error reason + +let%test_module "Mocked TLAPM" = + (module struct + let test_case doc_name timeout assert_fun = + Eio_main.run @@ fun env -> + Eio.Switch.run @@ fun sw -> + let fs = Eio.Stdenv.fs env in + let mgr = Eio.Stdenv.process_mgr env in + let du = LspT.DocumentUri.of_path doc_name in + let dt = "any\ncontent" in + let events = Eio.Stream.create 10 in + let events_adder = Eio.Stream.add events in + let pr = create sw fs mgr in + let tlapm_locator () = + let cwd = Sys.getcwd () in + Ok (Filename.concat cwd "../test/tlapm_mock.sh") + in + let clock = Eio.Stdenv.clock env in + let ts_start = Eio.Time.now clock in + let pr = + match + start_async pr du dt (Range.of_lines 3 7) [] events_adder + ~tlapm_locator () + with + | Ok pr -> pr + | Error e -> failwith e + in + let _pr = assert_fun pr clock events in + let ts_end = Eio.Time.now clock in + let () = + match ts_end -. ts_start < timeout with + | true -> () + | false -> + failwith + (Format.sprintf "timeout %f expired in %f" timeout + (ts_end -. ts_start)) + in + () + + (* Check a document which outputs a warning then sleeps for 3s and then + outputs another. We will cancel it in 0.5s, only the first warning + should be received, and the overall time should be less than a second. *) + let%test_unit "Mocked: CancelTiming" = + test_case "CancelTiming.tla" 1.0 @@ fun pr clock stream -> + let () = Eio.Time.sleep clock 0.5 in + let _pr = cancel_all pr in + let () = + match Eio.Stream.length stream with + | 2 -> () + | l -> failwith (Format.sprintf "expected 2 events, got %d" l) + in + let () = + match Eio.Stream.take_nonblocking stream with + | Some (TlapmNotif { msg = "message before delay"; _ }) -> () + | _ -> failwith "expected warning msg" + in + let () = + match Eio.Stream.take_nonblocking stream with + | Some TlapmTerminated -> () + | _ -> failwith "expected termination msg" + in + pr + + (* Check if abnormal tlapm termination don't cause any side effects. + We con't sleep or cancel a process here, just wait for expected messages. *) + let%test_unit "Mocked: AbnormalExit" = + test_case "AbnormalExit.tla" 1.0 @@ fun pr _clock stream -> + let () = + match Eio.Stream.take stream with + | TlapmNotif { msg = "this run is going to fail"; _ } -> () + | _ -> failwith "expected warning msg" + in + let () = + match Eio.Stream.take stream with + | TlapmTerminated -> () + | _ -> failwith "expected termination msg" + in + pr + + (* Check if output of running tlapm on a document with no proofs works. *) + let%test_unit "Mocked: Empty" = + test_case "Empty.tla" 1.0 @@ fun pr _clock stream -> + let () = + match Eio.Stream.take stream with + | TlapmObligationsNumber 0 -> () + | _ -> failwith "expected 0 obligations" + in + let () = + match Eio.Stream.take stream with + | TlapmTerminated -> () + | _ -> failwith "expected termination msg" + in + pr + + (* Check if output of running tlapm on a document with some proofs works. *) + let%test_unit "Mocked: Some" = + test_case "Some.tla" 1.0 @@ fun pr _clock stream -> + let () = + match Eio.Stream.take stream with + | TlapmObligation { status = ToBeProved; _ } -> () + | _ -> failwith "expected obligation" + in + let () = + match Eio.Stream.take stream with + | TlapmObligationsNumber 1 -> () + | _ -> failwith "expected 1 obligations" + in + let () = + match Eio.Stream.take stream with + | TlapmObligation { status = Proved; _ } -> () + | _ -> failwith "expected obligation" + in + let () = + match Eio.Stream.take stream with + | TlapmTerminated -> () + | _ -> failwith "expected termination msg" + in + pr + + (* Check if STDIN is passed properly to the TLAPM process. *) + let%test_unit "Mocked: Echo" = + test_case "Echo.tla" 1.0 @@ fun pr _clock stream -> + let () = + match Eio.Stream.take stream with + | TlapmNotif { msg; _ } -> ( + match msg with + | "any\ncontent" -> () + | _ -> failwith (Format.sprintf "unexpected msg=%S" msg)) + | _ -> failwith "expected obligation" + in + pr + end) diff --git a/lsp/lib/prover/prover.mli b/lsp/lib/prover/prover.mli new file mode 100644 index 00000000..e8022f67 --- /dev/null +++ b/lsp/lib/prover/prover.mli @@ -0,0 +1,107 @@ +module LspT := Lsp.Types + +(** Types representing messages from the prover. *) +module Toolbox : sig + type tlapm_obl_state = + | ToBeProved + | BeingProved + | Normalized + | Proved + | Failed + | Interrupted + | Trivial + | Unknown of string + + val tlapm_obl_state_to_string : tlapm_obl_state -> string + + module Obligation : sig + type t = { + id : int; + loc : Range.t; + status : tlapm_obl_state; + fp : string option; + prover : string option; + meth : string option; + reason : string option; + already : bool option; + obl : string option; + } + end + + type tlapm_notif_severity = TlapmNotifError | TlapmNotifWarning + + type tlapm_notif = { + loc : Range.t; + sev : tlapm_notif_severity; + msg : string; + url : string option; + } + + val notif_of_loc_msg : string option -> string -> tlapm_notif + + module Msg : sig + type t = + | TlapmNotif of tlapm_notif + | TlapmObligationsNumber of int + | TlapmObligationProvers of { id : int; provers : string list } + | TlapmObligation of Obligation.t + | TlapmTerminated + end +end + +module Progress : sig + type t + + module type Callbacks = sig + type p := t + type t + + val next_req_id : t -> Jsonrpc.Id.t * t + val lsp_send : t -> Jsonrpc.Packet.t -> t + val with_progress : t -> (t -> p -> t * p) -> t + end + + module Make (CB : Callbacks) : sig + val make : unit -> t + (** Create new instance of progress tracker. *) + + val is_latest : t -> LspT.ProgressToken.t -> bool + (** Checks if the token is of the last progress. *) + + val proof_started : p_ref:int -> CB.t -> CB.t + (** Called when new TLAPM run is initiated. *) + + val obl_count : p_ref:int -> obl_count:int -> CB.t -> CB.t + (** Called when a number of obligations is received from the TLAPM. *) + + val obligation_done : p_ref:int -> obl_id:int -> CB.t -> CB.t + (** Called when some proof obligation state change is received from TLAPM. *) + + val proof_ended : p_ref:int -> CB.t -> CB.t + (** Called when the TLAPM terminates. *) + end +end + +type t + +val create : + Eio.Switch.t -> + Eio__.Fs.dir_ty Eio.Path.t -> + Eio_unix.Process.mgr_ty Eio.Process.mgr -> + t +(** Create a tlapm process manager. *) + +val cancel_all : t -> t +(** Cancel all the ongoing proof processes, await for their termination. *) + +val start_async : + t -> + LspT.DocumentUri.t -> + string -> + Range.t -> + string list -> + (Toolbox.Msg.t -> unit) -> + ?tlapm_locator:(unit -> (string, string) result) -> + unit -> + (t, string) result +(** Start new proof process after canceling the existing processes. *) diff --git a/lsp/lib/prover/toolbox.ml b/lsp/lib/prover/toolbox.ml new file mode 100644 index 00000000..24912719 --- /dev/null +++ b/lsp/lib/prover/toolbox.ml @@ -0,0 +1,431 @@ +type tlapm_obl_state = + | ToBeProved + | BeingProved + | Normalized + | Proved + | Failed + | Interrupted + | Trivial + | Unknown of string + +let tlapm_obl_state_of_string s = + match s with + | "to be proved" -> ToBeProved + | "being proved" -> BeingProved + | "normalized" -> Normalized + | "proved" -> Proved + | "failed" -> Failed + | "interrupted" -> Interrupted + | "trivial" -> Trivial + | _ -> Unknown s + +(* The strings here don't have to match with the ones above. *) +let tlapm_obl_state_to_string (s : tlapm_obl_state) : string = + match s with + | ToBeProved -> "to be proved" + | BeingProved -> "being proved" + | Normalized -> "normalized" + | Proved -> "proved" + | Failed -> "failed" + | Interrupted -> "interrupted" + | Trivial -> "trivial" + | Unknown s -> "unknown state: " ^ s + +module Obligation = struct + type t = { + id : int; + loc : Range.t; + status : tlapm_obl_state; + fp : string option; + prover : string option; + meth : string option; + reason : string option; + already : bool option; + obl : string option; + } + + (** This is for testing only. *) + module Test = struct + let with_id_status id status = + { + id; + loc = Range.of_unknown; + status; + fp = None; + prover = None; + meth = None; + reason = None; + already = None; + obl = None; + } + end +end + +type tlapm_notif_severity = TlapmNotifError | TlapmNotifWarning + +type tlapm_notif = { + loc : Range.t; + sev : tlapm_notif_severity; + msg : string; + url : string option; +} + +module Msg = struct + type t = + | TlapmNotif of tlapm_notif + | TlapmObligationsNumber of int + | TlapmObligationProvers of { id : int; provers : string list } + | TlapmObligation of Obligation.t + | TlapmTerminated +end + +type parser_part_msg = + | PartWarning of { msg : string option } + | PartError of { url : string option; msg : string option } + | PartObligationsNumber of int option + | PartObligationProvers of { id : int option; provers : string list option } + | PartObligation of { + id : int option; + loc : Range.t option; + status : tlapm_obl_state option; + fp : string option; + prover : string option; + meth : string option; + reason : string option; + already : bool option; + obl : string option; + } + | PartUnknown + +type parser_state = + | Empty + | Begin + | PartMsg of { + field : string option; + acc_val : string; + acc_msg : parser_part_msg; + } + +let match_line line = + let re = Re2.create_exn {|^@!!([a-z]*):(.*)$|} in + match Re2.find_submatches re line with + | Ok [| _all_match; Some k; Some v |] -> Some (k, v) + | Ok _ -> assert false + | Error _ -> None + +let rec guess_notif_loc' str = function + | [] -> (Range.of_unknown, String.trim str) + | `A :: others -> ( + let re = + Re2.create_exn + {|^File "(.*)", line ([0-9]+), character ([0-9]+) to line ([0-9]+), character ([0-9]+) :\n?(.*)$|} + in + match Re2.find_submatches re str with + | Ok + [| + _all_match; + Some _File; + Some line_from; + Some char_from; + Some line_till; + Some char_till; + Some rest_msg; + |] -> + ( Range.of_ints ~lf:(int_of_string line_from) + ~cf:(int_of_string char_from) ~lt:(int_of_string line_till) + ~ct:(int_of_string char_till), + String.trim rest_msg ) + | Ok _ -> assert false + | Error _ -> guess_notif_loc' str others) + | `B :: others -> ( + let re_opts = { Re2.Options.default with dot_nl = true } in + let re = + Re2.create_exn + {|^File "(.*)", line ([0-9]+), characters ([0-9]+)-([0-9]+)\n?(.*)|} + ~options:re_opts + in + match Re2.find_submatches re str with + | Ok + [| + _all_match; + Some _file; + Some line; + Some char_from; + Some char_till; + Some rest_msg; + |] -> + ( Range.of_ints ~lf:(int_of_string line) ~cf:(int_of_string char_from) + ~lt:(int_of_string line) ~ct:(int_of_string char_till), + String.trim rest_msg ) + | Ok _ -> failwith "impossible" + | Error _ -> guess_notif_loc' str others) + | `C :: others -> ( + (* Messages like this: `File "aaa.tla", line 5, character 22` *) + let re_opts = { Re2.Options.default with dot_nl = true } in + let re = + Re2.create_exn + {|^File "(.*)", line ([0-9]+), character ([0-9]+)\n?(.*)|} + ~options:re_opts + in + match Re2.find_submatches re str with + | Ok [| _all_match; Some _file; Some line; Some char; Some rest_msg |] -> + ( Range.of_ints ~lf:(int_of_string line) ~cf:(int_of_string char) + ~lt:(int_of_string line) + ~ct:(int_of_string char + 4), + String.trim rest_msg ) + | Ok _ -> assert false + | Error _ -> guess_notif_loc' str others) + +let guess_notif_loc str = guess_notif_loc' str [ `A; `B; `C ] + +let notif_of_loc_msg loc_opt msg = + let sev = TlapmNotifWarning in + let url = None in + match loc_opt with + | None -> { sev; loc = Range.of_unknown; msg; url } + | Some loc_str -> + let loc, _empty_msg = guess_notif_loc loc_str in + { sev; loc; msg; url } + +let parse_start = Empty + +let parse_line line acc stream = + let new_msg m = PartMsg { field = None; acc_val = ""; acc_msg = m } in + let set_field n v = function + | PartWarning w -> ( + match n with + | "msg" -> PartWarning { msg = Some v } + | _ -> PartWarning w) + | PartError e -> ( + match n with + | "msg" -> PartError { e with msg = Some v } + | "url" -> PartError { e with url = Some v } + | _ -> PartError e) + | PartObligationsNumber e -> ( + match n with + | "count" -> PartObligationsNumber (int_of_string_opt v) + | _ -> PartObligationsNumber e) + | PartObligationProvers o -> ( + match n with + | "id" -> PartObligationProvers { o with id = int_of_string_opt v } + | "provers" -> + PartObligationProvers + { o with provers = Some (String.split_on_char ',' v) } + | _ -> PartObligationProvers o) + | PartObligation o -> ( + match n with + | "id" -> PartObligation { o with id = int_of_string_opt v } + | "loc" -> PartObligation { o with loc = Range.of_string_opt v } + | "status" -> + PartObligation + { o with status = Some (tlapm_obl_state_of_string v) } + | "fp" -> PartObligation { o with fp = Some v } + | "prover" -> PartObligation { o with prover = Some v } + | "meth" -> PartObligation { o with meth = Some v } + | "reason" -> PartObligation { o with reason = Some v } + | "already" -> PartObligation { o with already = bool_of_string_opt v } + | "obl" -> PartObligation { o with obl = Some v } + | _ -> PartObligation o) + | PartUnknown -> PartUnknown + in + let msg_of_part = function + | PartWarning { msg = Some msg } -> + let loc, msg = guess_notif_loc msg in + Some (Msg.TlapmNotif { loc; sev = TlapmNotifWarning; msg; url = None }) + | PartWarning _ -> None + | PartError { msg = Some msg; url } -> + let loc, msg = guess_notif_loc msg in + Some (Msg.TlapmNotif { loc; sev = TlapmNotifError; msg; url }) + | PartError _ -> None + | PartObligationsNumber (Some count) -> Some (TlapmObligationsNumber count) + | PartObligationsNumber _ -> None + | PartObligationProvers { id = Some id; provers = Some provers } -> + Some (TlapmObligationProvers { id; provers }) + | PartObligationProvers _ -> None + | PartObligation + { + id = Some id; + loc = Some loc; + status = Some status; + fp; + prover; + meth; + reason; + already; + obl; + } -> + Some + (TlapmObligation + { id; loc; status; fp; prover; meth; reason; already; obl }) + | PartObligation _ -> None + | PartUnknown -> None + in + match (acc, line) with + | Empty, "@!!BEGIN" -> Begin + | Empty, _ -> Empty + | Begin, "@!!type:warning" -> new_msg (PartWarning { msg = None }) + | Begin, "@!!type:error" -> new_msg (PartError { msg = None; url = None }) + | Begin, "@!!type:obligationsnumber" -> new_msg (PartObligationsNumber None) + | Begin, "@!!type:obligationprovers" -> + new_msg (PartObligationProvers { id = None; provers = None }) + | Begin, "@!!type:obligation" -> + new_msg + (PartObligation + { + id = None; + loc = None; + status = None; + fp = None; + prover = None; + meth = None; + reason = None; + already = None; + obl = None; + }) + | Begin, _ -> new_msg PartUnknown + | PartMsg { field; acc_val; acc_msg }, "@!!END" -> + let maybe_out_msg = + match field with + | Some f -> msg_of_part (set_field f acc_val acc_msg) + | None -> msg_of_part acc_msg + in + (match maybe_out_msg with Some out_msg -> stream out_msg | None -> ()); + Empty + | (PartMsg { field; acc_val; acc_msg } as msg), _ -> ( + match match_line line with + | Some (k, v) -> ( + match field with + | Some f -> + let acc_msg' = set_field f acc_val acc_msg in + PartMsg { field = Some k; acc_val = v; acc_msg = acc_msg' } + | None -> PartMsg { field = Some k; acc_val = v; acc_msg }) + | None -> ( + match field with + | Some _ -> + let acc_val' = acc_val ^ "\n" ^ line in + PartMsg { field; acc_val = acc_val'; acc_msg } + | None -> msg)) + +(* ********************** Test cases ********************** *) + +let%test_unit "parse_line-obl-num" = + let stream = Eio.Stream.create 10 in + let stream_add = Eio.Stream.add stream in + let lines = + [ + (* keep it multiline*) + "@!!BEGIN"; + "@!!type:obligationsnumber"; + "@!!count:17"; + "@!!END"; + ] + in + match + List.fold_left (fun acc l -> parse_line l acc stream_add) parse_start lines + with + | Empty -> ( + match Eio.Stream.length stream with + | 1 -> ( + match Eio.Stream.take stream with + | TlapmObligationsNumber 17 -> () + | _ -> failwith "unexpected msg") + | _ -> failwith "unexpected msg count") + | _ -> failwith "unexpected parser state" + +let%test_unit "parse_line-multiline" = + let stream = Eio.Stream.create 10 in + let stream_add = Eio.Stream.add stream in + let lines = + [ + "@!!BEGIN"; + "@!!type:obligation"; + "@!!id:2"; + "@!!loc:10:3:10:10"; + "@!!status:failed"; + "@!!prover:isabelle"; + "@!!meth:auto; time-limit: 30; time-used: 0.0 (0%)"; + "@!!reason:false"; + "@!!already:false"; + "@!!obl:"; + "ASSUME NEW CONSTANT A"; + "PROVE \\A x \\in A : A \\in x"; + ""; + "@!!END"; + ] + in + match + List.fold_left (fun acc l -> parse_line l acc stream_add) parse_start lines + with + | Empty -> ( + match Eio.Stream.length stream with + | 1 -> ( + let obl = + "\nASSUME NEW CONSTANT A\nPROVE \\A x \\in A : A \\in x\n" + in + match Eio.Stream.take stream with + | TlapmObligation { obl = Some o; _ } when o = obl -> () + | TlapmObligation { obl = Some o; _ } -> + failwith (Format.sprintf "unexpected: %s" o) + | _ -> failwith "unexpected msg") + | _ -> failwith "unexpected msg count") + | _ -> failwith "unexpected parser state" + +let%test_unit "parse-warning-loc" = + let stream = Eio.Stream.create 10 in + let stream_add = Eio.Stream.add stream in + let expected_msg1 = + "Warning: module name \"bbb\" does not match file name \"aaa.tla\"." + in + let expected_msg2 = "Operator \"prover\" not found" in + let expected_msg3 = "Unexpected {" in + let lines = + [ + "@!!BEGIN"; + "@!!type:warning"; + "@!!msg:File \"aaa.tla\", line 1, character 1 to line 17, character 4 :"; + expected_msg1; + "@!!END"; + "@!!BEGIN"; + "@!!type:warning"; + "@!!msg:File \"aaa.tla\", line 5, characters 9-14"; + ""; + expected_msg2; + ""; + "@!!END"; + "@!!BEGIN"; + "@!!type:warning"; + "@!!msg:File \"aaa.tla\", line 5, character 22"; + expected_msg3; + "@!!END"; + ] + in + match + List.fold_left (fun acc l -> parse_line l acc stream_add) parse_start lines + with + | Empty -> ( + match Eio.Stream.length stream with + | 3 -> ( + let expected_loc1 = Range.of_ints ~lf:1 ~cf:1 ~lt:17 ~ct:4 in + let expected_loc2 = Range.of_ints ~lf:5 ~cf:9 ~lt:5 ~ct:14 in + let expected_loc3 = Range.of_ints ~lf:5 ~cf:22 ~lt:5 ~ct:26 in + (match Eio.Stream.take stream with + | TlapmNotif { msg; loc; sev = TlapmNotifWarning; url = None } + when msg = expected_msg1 && loc = expected_loc1 -> + () + | _ -> failwith "unexpected msg1"); + (match Eio.Stream.take stream with + | TlapmNotif { msg; loc; sev = TlapmNotifWarning; url = None } + when msg = expected_msg2 && loc = expected_loc2 -> + () + | TlapmNotif { msg; loc; _ } -> + failwith + (Format.sprintf "msg=%S, loc=%s" msg + (Range.string_of_range loc)) + | _ -> failwith "unexpected msg2"); + match Eio.Stream.take stream with + | TlapmNotif { msg; loc; sev = TlapmNotifWarning; url = None } + when msg = expected_msg3 && loc = expected_loc3 -> + () + | _ -> failwith "unexpected msg3") + | _ -> failwith "unexpected msg count") + | _ -> failwith "unexpected parser state" diff --git a/lsp/lib/prover/toolbox.mli b/lsp/lib/prover/toolbox.mli new file mode 100644 index 00000000..e7870eea --- /dev/null +++ b/lsp/lib/prover/toolbox.mli @@ -0,0 +1,59 @@ +(** Parser for the toolbox protocol and all the related data structures. *) + +type tlapm_obl_state = + | ToBeProved + | BeingProved + | Normalized + | Proved + | Failed + | Interrupted + | Trivial + | Unknown of string + +val tlapm_obl_state_to_string : tlapm_obl_state -> string + +module Obligation : sig + type t = { + id : int; + loc : Range.t; + status : tlapm_obl_state; + fp : string option; + prover : string option; + meth : string option; + reason : string option; + already : bool option; + obl : string option; + } + + (** For testing only. *) + module Test : sig + val with_id_status : int -> tlapm_obl_state -> t + end +end + +type tlapm_notif_severity = TlapmNotifError | TlapmNotifWarning + +type tlapm_notif = { + loc : Range.t; + sev : tlapm_notif_severity; + msg : string; + url : string option; +} + +val notif_of_loc_msg : string option -> string -> tlapm_notif + +module Msg : sig + type t = + | TlapmNotif of tlapm_notif + | TlapmObligationsNumber of int + | TlapmObligationProvers of { id : int; provers : string list } + | TlapmObligation of Obligation.t + | TlapmTerminated +end + +(* Parser. *) + +type parser_state + +val parse_start : parser_state +val parse_line : string -> parser_state -> (Msg.t -> unit) -> parser_state diff --git a/lsp/lib/range.ml b/lsp/lib/range.ml new file mode 100644 index 00000000..c5266505 --- /dev/null +++ b/lsp/lib/range.ml @@ -0,0 +1,198 @@ +(* LSP ranges are 0-based and TLAPM is 1-based. In LSP the last char is exclusive. *) + +module LspT = Lsp.Types + +module Position : sig + type t + + val make : int -> int -> t + val of_pair : int * int -> t + val as_pair : t -> int * int + val as_string : t -> string + val compare : t -> t -> int + val less : t -> t -> bool + val leq : t -> t -> bool + val min : t -> t -> t + val max : t -> t -> t + val line : t -> int +end = struct + type t = P of int * int + + let make l c = P (l, c) + let of_pair (l, c) = P (l, c) + let as_pair (P (l, c)) = (l, c) + let as_string (P (l, c)) = Format.sprintf "%d:%d" l c + + (* Implement Map.OrderedType *) + let compare (P (al, ac)) (P (bl, bc)) = + let l = Stdlib.compare al bl in + if l = 0 then Stdlib.compare ac bc else l + + let less (P (al, ac)) (P (bl, bc)) = + match Stdlib.compare al bl with + | 0 -> Stdlib.compare ac bc < 0 + | l_diff -> l_diff < 0 + + let leq (P (al, ac)) (P (bl, bc)) = + match Stdlib.compare al bl with + | 0 -> Stdlib.compare ac bc <= 0 + | l_diff -> l_diff < 0 + + let min a b = if less a b then a else b + let max a b = if less a b then b else a + let line (P (l, _)) = l +end + +type t = R of (int * int) * (int * int) + +let line_from (R ((fl, _), _)) = fl +let line_till (R (_, (tl, _))) = tl +let from (R ((fl, fc), _)) = Position.make fl fc +let till (R (_, (tl, tc))) = Position.make tl tc + +(* Implement Map.OrderedType *) +let compare (R (af, at)) (R (bf, bt)) = + let f = Position.compare (Position.of_pair af) (Position.of_pair bf) in + if f = 0 then Position.compare (Position.of_pair at) (Position.of_pair bt) + else f + +let as_lsp_range (R ((fl, fc), (tl, tc))) = + let open LspT in + Range.create + ~start:(Position.create ~line:(fl - 1) ~character:(fc - 1)) + ~end_:(Position.create ~line:(tl - 1) ~character:tc) + +let of_lsp_range (range : LspT.Range.t) = + let f = (range.start.line + 1, range.start.character + 1) in + let t = (range.end_.line + 1, range.end_.character) in + R (f, t) + +let of_string_opt s = + match String.split_on_char ':' s with + | [ fl; fc; tl; tc ] -> + let f = (int_of_string fl, int_of_string fc) in + let t = (int_of_string tl, int_of_string tc - 1) in + Some (R (f, t)) + | _ -> None + +let of_locus (locus : Tlapm_lib.Loc.locus) = + match (locus.start, locus.stop) with + | Actual start_pt, Actual stop_pt -> + Some (R ((start_pt.line, start_pt.col), (stop_pt.line, stop_pt.col - 1))) + | Dummy, _ | _, Dummy -> None + +let of_locus_opt (locus : Tlapm_lib.Loc.locus option) = + match locus with None -> None | Some locus -> of_locus locus + +let of_locus_must (locus : Tlapm_lib.Loc.locus) = Option.get (of_locus locus) +let of_wrapped prop = of_locus_opt (Tlapm_lib.Util.query_locus prop) +let of_wrapped_must prop = Option.get (of_wrapped prop) +let of_points f t = R (Position.as_pair f, Position.as_pair t) +let of_ints ~lf ~cf ~lt ~ct = R ((lf, cf), (lt, ct)) +let of_lines fl tl = R ((fl, 1), (tl, 1)) + +let join (R (af, at)) (R (bf, bt)) = + let f = Position.min (Position.of_pair af) (Position.of_pair bf) in + let t = Position.max (Position.of_pair at) (Position.of_pair bt) in + of_points f t + +let string_of_range (R ((fl, fc), (tl, tc))) : string = + Format.sprintf "%d:%d:%d:%d" fl fc tl tc + +let string_of_pos p = Position.as_string p + +(* Where to show the location of error for which the location is unknown. *) +let of_unknown = R ((1, 1), (1, 4)) + +(* To pass it to TLAPM for checking all the document. *) +let of_all = R ((0, 0), (0, 0)) + +(** [before p r] means range [r] is before point [p]. *) +let before p r = Position.less (till r) p + +(** [intersect a b] is true, if ranges [a] and [b] overlaps. *) +let intersect a b = + Position.leq (from a) (till b) && Position.leq (from b) (till a) + +(** [lines_intersect a b] is true if line ranges for [a] and [b] intersect. *) +let lines_intersect a b = + let lfa = line_from a in + let lta = line_till a in + let lfb = line_from b in + let ltb = line_till b in + lfa <= ltb && lfb <= lta + +(** [line_covered r p] is true, if the line of position [p] intersects with the range [r] lines. *) +let line_covered r p = + let l = Position.line p in + line_from r <= l && l <= line_till r + +(* [lines_covered a b] is true if lines of [a] are fully covered by [b], i.e. [a] is inside of [b]. *) +let lines_covered a b = + let lfa = line_from a in + let lta = line_till a in + let lfb = line_from b in + let ltb = line_till b in + lfb <= lfa && lta <= ltb + +let lines_covered_or_all q rs = + match List.filter (lines_intersect q) rs with + | [] -> of_all + | matching -> + List.fold_left + (fun acc m -> + let from = Position.min (from acc) (from m) in + let till = Position.max (till acc) (till m) in + of_points from till) + q matching + +let first_diff_pos a b = + let len = min (String.length a) (String.length b) in + let rec count i l c = + if i = len then Position.make l c + else + let ai = String.get a i in + let bi = String.get b i in + if ai = bi then + let l, c = + match bi with '\n' -> (l + 1, 1) | '\r' -> (l, c) | _ -> (l, c + 1) + in + count (i + 1) l c + else Position.make l c + in + count 0 1 1 + +let%test_module "before" = + (module struct + let p35 = Position.make 3 5 + let%test _ = not (before p35 (R ((1, 1), (5, 3)))) + let%test _ = not (before p35 (R ((1, 1), (3, 6)))) + let%test _ = not (before p35 (R ((1, 1), (3, 5)))) + let%test _ = before p35 (R ((1, 1), (2, 5))) + end) + +let%test_module "first_diff_pos" = + (module struct + let test_fun a b = Position.as_pair (first_diff_pos a b) + let%test "first" = (1, 1) = test_fun "hello" "bye" + let%test "second" = (1, 2) = test_fun "hello" "hallo" + let%test "next_ln" = (2, 1) = test_fun "sa\nme" "sa\ny" + let%test "line_len_a" = (1, 3) = test_fun "same" "sa\n" + let%test "line_len_b" = (1, 3) = test_fun "sa\n" "same" + let%test "index_bounds_1" = (1, 3) = test_fun "mod" "mo" + let%test "index_bounds_2" = (1, 3) = test_fun "mo" "mod" + end) + +let%test_module "lines_covered_or_all" = + (module struct + let some = R ((10, 5), (11, 20)) + let before1 = R ((1, 1), (2, 10)) + let on_from = R ((9, 1), (10, 6)) + let on_till = R ((10, 20), (15, 8)) + let within = R ((10, 20), (11, 10)) + let%test _ = of_all = lines_covered_or_all some [ before1 ] + let%test _ = some = lines_covered_or_all some [ within ] + + let%test _ = + R ((9, 1), (15, 8)) = lines_covered_or_all some [ on_from; on_till ] + end) diff --git a/lsp/lib/range.mli b/lsp/lib/range.mli new file mode 100644 index 00000000..384d6973 --- /dev/null +++ b/lsp/lib/range.mli @@ -0,0 +1,38 @@ +module LspT := Lsp.Types + +module Position : sig + type t + + val compare : t -> t -> int +end + +type t + +val from : t -> Position.t +val till : t -> Position.t +val line_from : t -> int +val line_till : t -> int +val as_lsp_range : t -> LspT.Range.t +val of_lsp_range : LspT.Range.t -> t +val of_string_opt : string -> t option +val of_locus : Tlapm_lib.Loc.locus -> t option +val of_locus_opt : Tlapm_lib.Loc.locus option -> t option +val of_locus_must : Tlapm_lib.Loc.locus -> t +val of_wrapped : 'a Tlapm_lib.Property.wrapped -> t option +val of_wrapped_must : 'a Tlapm_lib.Property.wrapped -> t +val of_points : Position.t -> Position.t -> t +val of_ints : lf:int -> cf:int -> lt:int -> ct:int -> t +val of_lines : int -> int -> t +val of_unknown : t +val of_all : t +val join : t -> t -> t +val string_of_range : t -> string +val string_of_pos : Position.t -> string +val compare : t -> t -> int +val before : Position.t -> t -> bool +val intersect : t -> t -> bool +val lines_intersect : t -> t -> bool +val line_covered : t -> Position.t -> bool +val lines_covered : t -> t -> bool +val lines_covered_or_all : t -> t list -> t +val first_diff_pos : string -> string -> Position.t diff --git a/lsp/lib/server/codec.ml b/lsp/lib/server/codec.ml new file mode 100644 index 00000000..70492f57 --- /dev/null +++ b/lsp/lib/server/codec.ml @@ -0,0 +1,43 @@ +type trace_fun = string -> unit +type input_chan = Eio.Buf_read.t * trace_fun +type output_chan = Eio.Buf_write.t * trace_fun + +module IoState = struct + type 'a t = ('a, exn) result + + let return x = Ok x + let raise exn = Error exn + + module O = struct + let ( let+ ) st f = Result.map f st + let ( let* ) st f = Result.bind st f + end +end + +module IoChan = struct + type input = input_chan + type output = output_chan + + let read_line ((buf, trace) : input) : string option IoState.t = + let line = Eio.Buf_read.line buf in + let () = trace line in + Ok (Some line) + + let read_exactly ((buf, trace) : input) (n : int) : string option IoState.t = + let data = Eio.Buf_read.take n buf in + let () = trace data in + Ok (Some data) + + let rec write ((buf, trace) : output) (lines : string list) : unit IoState.t = + match lines with + | [] -> Ok () + | line :: tail -> + let () = trace line in + let () = Eio.Buf_write.string buf line in + write (buf, trace) tail +end + +module LspIo = Lsp.Io.Make (IoState) (IoChan) + +let read = LspIo.read +let write = LspIo.write diff --git a/lsp/lib/server/codec.mli b/lsp/lib/server/codec.mli new file mode 100644 index 00000000..fc169e38 --- /dev/null +++ b/lsp/lib/server/codec.mli @@ -0,0 +1,11 @@ +(** +Here we construct a decoder/encoder for the LSP protocol on top of Eio flows. +We use the lsp module from the ocaml-lsp server and configure it to run over Eio. +*) + +type trace_fun = string -> unit +type input_chan = Eio.Buf_read.t * trace_fun +type output_chan = Eio.Buf_write.t * trace_fun + +val read : input_chan -> (Jsonrpc.Packet.t option, exn) result +val write : output_chan -> Jsonrpc.Packet.t -> (unit, exn) result diff --git a/lsp/lib/server/handlers.ml b/lsp/lib/server/handlers.ml new file mode 100644 index 00000000..f4e8f8ea --- /dev/null +++ b/lsp/lib/server/handlers.ml @@ -0,0 +1,369 @@ +module LspT = Lsp.Types + +module type Callbacks = sig + type t + + val ready : t -> t + val shutdown : t -> t + val lsp_send : t -> Jsonrpc.Packet.t -> t + val with_docs : t -> (t * Docs.t -> t * Docs.t) -> t + val prove_step : t -> LspT.DocumentUri.t -> int -> LspT.Range.t -> t + val cancel : t -> LspT.ProgressToken.t -> t + val use_paths : t -> string list -> t + + val suggest_proof_range : + t -> LspT.DocumentUri.t -> LspT.Range.t -> t * (int * LspT.Range.t) option + + val track_obligation_proof_state : + t -> LspT.DocumentUri.t -> LspT.Range.t -> t + + val latest_diagnostics : + t -> LspT.DocumentUri.t -> t * (int * LspT.Diagnostic.t list) + + val diagnostic_source : string +end + +module Make (CB : Callbacks) = struct + (** Helper to send responses to requests. *) + let reply_ok (jsonrpc_req : Jsonrpc.Request.t) payload cb_state = + let open Jsonrpc in + let response = Response.ok jsonrpc_req.id payload in + let packet = Packet.Response response in + CB.lsp_send cb_state packet + + (** Helper to send responses to requests. *) + let reply_error (jsonrpc_req : Jsonrpc.Request.t) code message cb_state = + let open Jsonrpc in + let error = Response.Error.make ~code ~message () in + let response = Response.error jsonrpc_req.id error in + let packet = Packet.Response response in + CB.lsp_send cb_state packet + + (** Dispatch notification packets. *) + let handle_jsonrpc_notif jsonrpc_notif cb_state = + let open LspT in + match Lsp.Client_notification.of_jsonrpc jsonrpc_notif with + | Ok Initialized -> + Eio.traceln "CONN: Initialized"; + CB.ready cb_state + | Ok (TextDocumentDidOpen params) -> + let uri = params.textDocument.uri in + let vsn = params.textDocument.version in + let text = params.textDocument.text in + Eio.traceln "DOCUMENT[Open]: %s => %s" (DocumentUri.to_string uri) text; + CB.with_docs cb_state @@ fun (cb_st, docs) -> + let docs = Docs.add docs uri vsn text in + (cb_st, docs) + | Ok (TextDocumentDidChange params) -> ( + let uri = params.textDocument.uri in + let vsn = params.textDocument.version in + match params.contentChanges with + | [ { text; range = None; rangeLength = None } ] -> + Eio.traceln "DOCUMENT[Change]: %s => %s" + (DocumentUri.to_string uri) + text; + CB.with_docs cb_state @@ fun (cb_st, docs) -> + (cb_st, Docs.add docs uri vsn text) + | _ -> failwith "incremental changes not supported") + | Ok (TextDocumentDidClose params) -> + let uri = params.textDocument.uri in + CB.with_docs cb_state @@ fun (cb_st, docs) -> (cb_st, Docs.rem docs uri) + | Ok (DidSaveTextDocument params) -> + let uri = params.textDocument.uri in + Eio.traceln "DOCUMENT[Save]: %s" (DocumentUri.to_string uri); + cb_state + | Ok (SetTrace params) -> + let level = + match params.value with + | Compact -> "Compact" + | Off -> "Off" + | Messages -> "Messages" + | Verbose -> "Verbose" + in + Eio.traceln "CONN: Set trace: %s -- ignored" level; + cb_state + | Ok (WorkDoneProgressCancel params) -> + Eio.traceln "WORK_DONE[CANCEL]"; + CB.cancel cb_state params.token + | Ok (UnknownNotification _params) -> + Eio.traceln "Unknown notification: %s" jsonrpc_notif.method_; + cb_state + | Ok _unsupported -> + Eio.traceln "Unsupported notification: %s" jsonrpc_notif.method_; + cb_state + | Error error -> + Eio.traceln "Failed to decode notification: %s - %s" + jsonrpc_notif.method_ error; + cb_state + + let handle_jsonrpc_req_initialize (jsonrpc_req : Jsonrpc.Request.t) params + cb_state = + let open LspT in + let print_ci (params : InitializeParams.t) = + match params.clientInfo with + | None -> () + | Some ci -> + let ci_version = match ci.version with None -> "?" | Some v -> v in + Eio.traceln "CONN: Client INFO, name=%s, version=%s" ci.name + ci_version + in + print_ci params; + let cb_state = + let open Structs.InitializationOptions in + let init_opts = t_of_yojson params.initializationOptions in + CB.use_paths cb_state (module_search_paths init_opts) + in + let supported_commands = + [ + "tlaplus.tlaps.check-step.lsp"; + "tlaplus.tlaps.proofStepMarkers.fetch.lsp"; + "tlaplus.tlaps.currentProofStep.set.lsp"; + "tlaplus.tlaps.moduleSearchPaths.updated.lsp"; + ] + in + let capabilities = + ServerCapabilities.create + ~textDocumentSync:(`TextDocumentSyncKind TextDocumentSyncKind.Full) + ~executeCommandProvider: + (ExecuteCommandOptions.create ~commands:supported_commands + ~workDoneProgress:true ()) + ~diagnosticProvider: + (`DiagnosticOptions + (DiagnosticOptions.create ~identifier:CB.diagnostic_source + ~interFileDependencies:false ~workspaceDiagnostics:false + ~workDoneProgress:false ())) + ~codeActionProvider: + (`CodeActionOptions + (CodeActionOptions.create ~resolveProvider:false + ~workDoneProgress:false + ~codeActionKinds: + [ CodeActionKind.Other "tlaplus.tlaps.check-step.ca" ] + ())) + ~experimental: + Structs.ServerCapabilitiesExperimental.( + yojson_of_t + (make ~module_search_paths:Tlapm_lib.stdlib_search_paths)) + () + in + let server_version = + match Build_info.V1.version () with + | None -> "development" + | Some v -> Build_info.V1.Version.to_string v + in + let serverInfo = + InitializeResult.create_serverInfo ~name:"tlapm-lsp" + ~version:server_version () + in + let respInfo = InitializeResult.create ~capabilities ~serverInfo () in + reply_ok jsonrpc_req (InitializeResult.yojson_of_t respInfo) cb_state + + let handle_jsonrpc_req_shutdown (_jsonrpc_req : Jsonrpc.Request.t) cb_state = + Eio.traceln "CONN: Shutdown"; + CB.shutdown cb_state + + (* It looks like VSCode treats the diagnostics returned in response to this call + as different from those pushed by the server using notifications. To avoid + duplicated diagnostics we respond always to this request with an empty set, + and update the diagnostics by sending asynchronous notification. *) + let handle_jsonrpc_req_diagnostics (jsonrpc_req : Jsonrpc.Request.t) uri + cb_state = + let cb_state, (p_ref, items) = CB.latest_diagnostics cb_state uri in + let report = + LspT.FullDocumentDiagnosticReport.create ~items + ~resultId:(string_of_int p_ref) () + in + reply_ok jsonrpc_req + (LspT.FullDocumentDiagnosticReport.yojson_of_t report) + cb_state + + let handle_fetch_proof_step_markers (jsonrpc_req : Jsonrpc.Request.t) + (params : LspT.ExecuteCommandParams.t) cb_state = + let cb_state = + match params.arguments with + | Some [ uri ] -> + let tid = LspT.TextDocumentIdentifier.t_of_yojson uri in + let cb_state, (_p_ref, _items) = + CB.latest_diagnostics cb_state tid.uri + in + cb_state + | _ -> + Eio.traceln "Unexpected parameters in handle_fetch_proof_step_markers"; + cb_state + in + reply_ok jsonrpc_req `Null cb_state + + let handle_cmd_current_proof_step_set (jsonrpc_req : Jsonrpc.Request.t) + (params : LspT.ExecuteCommandParams.t) cb_state = + let cb_state = + match params.arguments with + | Some [ uri; range ] -> + let uri = (LspT.TextDocumentIdentifier.t_of_yojson uri).uri in + let range = LspT.Range.t_of_yojson range in + CB.track_obligation_proof_state cb_state uri range + | _ -> + Eio.traceln + "Unexpected parameters in handle_cmd_current_proof_step_set"; + cb_state + in + reply_ok jsonrpc_req `Null cb_state + + let handle_cmd_module_search_paths_updated (jsonrpc_req : Jsonrpc.Request.t) + (params : LspT.ExecuteCommandParams.t) cb_state = + let cb_state = + match params.arguments with + | Some paths -> + let paths = + List.filter_map (function `String p -> Some p | _ -> None) paths + in + CB.use_paths cb_state paths + | _ -> + Eio.traceln + "Unexpected parameters in handle_cmd_module_search_paths_updated"; + cb_state + in + reply_ok jsonrpc_req `Null cb_state + + let handle_jsonrpc_req_unknown (jsonrpc_req : Jsonrpc.Request.t) message + cb_state = + Eio.traceln "Received unknown JsonRPC request, method=%s, error=%s" + jsonrpc_req.method_ message; + let open Jsonrpc.Response.Error in + reply_error jsonrpc_req Code.MethodNotFound message cb_state + + (* Example request: + {"jsonrpc":"2.0","id":6,"method":"workspace/executeCommand","params":{ + "command":"tlaplus.tlaps.check-step.lsp", + "arguments":[ + {"uri":"file:///home/.../aaa.tla","version":1}, + {"start":{"line":2,"character":15},"end":{"line":2,"character":15}} ]}} + *) + let handle_check_step (jsonrpc_req : Jsonrpc.Request.t) + (params : LspT.ExecuteCommandParams.t) cb_state = + Eio.traceln "COMMAND: prove-step"; + match params.arguments with + | Some [ uri_vsn_arg; range_arg ] -> + let uri_vsn = + LspT.VersionedTextDocumentIdentifier.t_of_yojson uri_vsn_arg + in + let range = LspT.Range.t_of_yojson range_arg in + let cb_state = + CB.prove_step cb_state uri_vsn.uri uri_vsn.version range + in + reply_ok jsonrpc_req `Null cb_state + | Some _ -> + reply_error jsonrpc_req Jsonrpc.Response.Error.Code.InvalidParams + "two arguments expected" cb_state + | None -> + reply_error jsonrpc_req Jsonrpc.Response.Error.Code.InvalidParams + "arguments missing" cb_state + + (* Example request: + {"jsonrpc":"2.0", + "id":1, + "method":"workspace/executeCommand", + "params":{ + "command":"...", + "arguments":[...]}} *) + let handle_jsonrpc_req_exec_cmd (jsonrpc_req : Jsonrpc.Request.t) + (params : LspT.ExecuteCommandParams.t) cb_state = + match params.command with + | "tlaplus.tlaps.check-step.lsp" -> + handle_check_step jsonrpc_req params cb_state + | "tlaplus.tlaps.proofStepMarkers.fetch.lsp" -> + handle_fetch_proof_step_markers jsonrpc_req params cb_state + | "tlaplus.tlaps.currentProofStep.set.lsp" -> + handle_cmd_current_proof_step_set jsonrpc_req params cb_state + | "tlaplus.tlaps.moduleSearchPaths.updated.lsp" -> + handle_cmd_module_search_paths_updated jsonrpc_req params cb_state + | unknown -> + handle_jsonrpc_req_unknown jsonrpc_req + (Printf.sprintf "command unknown: %s" unknown) + cb_state + + (** + Provide code actions for a document. + - Code actions can be used for proof decomposition, probably. + *) + let handle_jsonrpc_req_code_action (jsonrpc_req : Jsonrpc.Request.t) + (params : LspT.CodeActionParams.t) cb_state = + let user_range = params.range in + let uri = params.textDocument.uri in + let cb_state, res = CB.suggest_proof_range cb_state uri user_range in + match res with + | None -> + reply_ok jsonrpc_req (LspT.CodeActionResult.yojson_of_t None) cb_state + | Some (version, p_range) -> + let l_from = p_range.start.line + 1 in + let l_till = p_range.end_.line + 1 in + let title = + if l_from = 0 && l_till = 0 then "Check all document proofs" + else if l_from = l_till then + Format.sprintf "Check proof on line %d" l_from + else Format.sprintf "Check proofs on lines %d-%d" l_from l_till + in + let uri_vsn = + LspT.VersionedTextDocumentIdentifier.create ~uri ~version + in + let check_step_ca = + LspT.CodeAction.create ~title + ~command: + (LspT.Command.create ~command:"tlaplus.tlaps.check-step.lsp" + ~title + ~arguments: + [ + LspT.VersionedTextDocumentIdentifier.yojson_of_t uri_vsn; + LspT.Range.yojson_of_t p_range; + ] + ()) + () + in + let acts = Some [ `CodeAction check_step_ca ] in + reply_ok jsonrpc_req (LspT.CodeActionResult.yojson_of_t acts) cb_state + + (** Dispatch request packets. *) + let handle_jsonrpc_request (jsonrpc_req : Jsonrpc.Request.t) cb_state = + let open LspT in + match Lsp.Client_request.of_jsonrpc jsonrpc_req with + | Ok (E (Initialize (params : InitializeParams.t))) -> + handle_jsonrpc_req_initialize jsonrpc_req params cb_state + | Ok (E (ExecuteCommand params)) -> + handle_jsonrpc_req_exec_cmd jsonrpc_req params cb_state + | Ok (E (CodeAction params)) -> + handle_jsonrpc_req_code_action jsonrpc_req params cb_state + | Ok (E Shutdown) -> handle_jsonrpc_req_shutdown jsonrpc_req cb_state + | Ok (E (TextDocumentDiagnostic params)) -> + handle_jsonrpc_req_diagnostics jsonrpc_req params.textDocument.uri + cb_state + | Ok (E _unsupported) -> + handle_jsonrpc_req_unknown jsonrpc_req "method not supported" cb_state + | Error reason -> + let err_msg = Printf.sprintf "cannot decode method: %s" reason in + handle_jsonrpc_req_unknown jsonrpc_req err_msg cb_state + + (* Dispatch client responses to our requests. *) + let handle_jsonrpc_response _jsonrpc_resp state = state + + let handle_jsonrpc_packet (packet : Jsonrpc.Packet.t) state = + match packet with + | Notification notif -> handle_jsonrpc_notif notif state + | Request req -> ( + try handle_jsonrpc_request req state + with exc -> + let open Jsonrpc.Response.Error in + let exc_str = Printexc.to_string exc in + Eio.traceln "LSP request failed with exception %s" exc_str; + reply_error req Code.InternalError exc_str state) + | Response resp -> handle_jsonrpc_response resp state + | Batch_call sub_packets -> + let fold_fun state_acc sub_pkg = + match sub_pkg with + | `Notification notif -> handle_jsonrpc_notif notif state_acc + | `Request req -> handle_jsonrpc_request req state_acc + in + List.fold_left fold_fun state sub_packets + | Batch_response sub_responses -> + let fold_fun state_acc sub_resp = + handle_jsonrpc_response sub_resp state_acc + in + List.fold_left fold_fun state sub_responses +end diff --git a/lsp/lib/server/handlers.mli b/lsp/lib/server/handlers.mli new file mode 100644 index 00000000..cbe81b2d --- /dev/null +++ b/lsp/lib/server/handlers.mli @@ -0,0 +1,32 @@ +(** Here we have all the TLAPM specific LSP action handlers. *) + +module LspT := Lsp.Types + +module type Callbacks = sig + type t + + val ready : t -> t + val shutdown : t -> t + val lsp_send : t -> Jsonrpc.Packet.t -> t + val with_docs : t -> (t * Docs.t -> t * Docs.t) -> t + val prove_step : t -> LspT.DocumentUri.t -> int -> LspT.Range.t -> t + val cancel : t -> LspT.ProgressToken.t -> t + val use_paths : t -> string list -> t + + val suggest_proof_range : + t -> LspT.DocumentUri.t -> LspT.Range.t -> t * (int * LspT.Range.t) option + + val track_obligation_proof_state : + t -> LspT.DocumentUri.t -> LspT.Range.t -> t + (** User selected a position in a document, we have to provide the + obligation info for it. The information has to be re-sent on update. *) + + val latest_diagnostics : + t -> LspT.DocumentUri.t -> t * (int * LspT.Diagnostic.t list) + + val diagnostic_source : string +end + +module Make (CB : Callbacks) : sig + val handle_jsonrpc_packet : Jsonrpc.Packet.t -> CB.t -> CB.t +end diff --git a/lsp/lib/server/server.ml b/lsp/lib/server/server.ml new file mode 100644 index 00000000..c6325a6d --- /dev/null +++ b/lsp/lib/server/server.ml @@ -0,0 +1,122 @@ +(* cSpell:words ipaddr *) + +module Structs = Structs + +(** 50 MB should be enough. *) +let max_size = 50 * 1024 * 1024 + +(** The proof info updates are aggregated for 0.5s before sending them to IDE. *) +let timer_tick_period = 0.5 + +type transport = Stdio | Socket of int + +(** Passed to the IO codec to log the traffic, if needed. *) +let trace_fun trace direction = + match (trace, direction) with + | true, `Input -> fun str -> Eio.traceln "[I] %s" str + | true, `Output -> fun str -> Eio.traceln "[O] %s" str + | false, _ -> fun _ -> () + +let flow_handler_fib_lsp_writer trace output_flow output_taker () = + Eio.Buf_write.with_flow output_flow @@ fun buf_w -> + let output_chan = (buf_w, trace_fun trace `Output) in + let write_packet out_packet = + let buf_w, _ = output_chan in + match Codec.write output_chan out_packet with + | Ok () -> Eio.Buf_write.flush buf_w + | Error exn -> + Eio.traceln "IO Error reading packet: %s" (Printexc.to_string exn) + in + let rec write_loop () = + match output_taker () with + | Some out_packet -> + write_packet out_packet; + write_loop () + | None -> () + in + write_loop () + +let flow_handler_fib_lsp_reader trace input_flow event_adder () = + let buf_r = Eio.Buf_read.of_flow input_flow ~max_size in + let input_chan = (buf_r, trace_fun trace `Input) in + let rec read_loop () = + match Codec.read input_chan with + | Ok (Some packet) -> + event_adder (Session.LspPacket packet); + read_loop () + | Ok None -> + event_adder Session.LspEOF; + Eio.traceln "No packet was read." + | Error exn -> + event_adder Session.LspEOF; + Eio.traceln "IO Error reading packet: %s" (Printexc.to_string exn) + in + read_loop () + +(** Configures the IO for the given input/output flows. *) +let flow_handler trace input_flow output_flow sw fs clock proc_mgr = + let events = Eio.Stream.create 100 in + let event_adder e = Eio.Stream.add events e in + let event_taker () = Eio.Stream.take events in + let output = Eio.Stream.create 100 in + let output_adder e = Eio.Stream.add output e in + let output_taker () = Eio.Stream.take output in + let rec timer () = + Eio.Time.sleep clock timer_tick_period; + event_adder Session.TimerTick; + timer () + in + Eio.Fiber.all + [ + (fun () -> + Session.run event_taker event_adder output_adder sw fs proc_mgr); + flow_handler_fib_lsp_reader trace input_flow event_adder; + flow_handler_fib_lsp_writer trace output_flow output_taker; + timer; + ] + +(** StdIO specifics. *) +module OnStdio = struct + let run trace env = + let fs = Eio.Stdenv.fs env in + let clock = Eio.Stdenv.clock env in + let proc_mgr = Eio.Stdenv.process_mgr env in + let switch_fun sw = + flow_handler trace (Eio.Stdenv.stdin env) (Eio.Stdenv.stdout env) sw fs + clock proc_mgr + in + Eio.Switch.run switch_fun +end + +(** Socket-specifics. *) +module OnSocket = struct + let req_handler trace sw fs clock proc_mgr flow _addr = + Eio.traceln "Server: got connection from client"; + flow_handler trace flow flow sw fs clock proc_mgr + + let switch (net : 'a Eio.Net.ty Eio.Std.r) port trace stop_promise fs clock + proc_mgr sw = + Eio.traceln "Socket switch started"; + let on_error = Eio.traceln "Error handling connection: %a" Fmt.exn in + let addr = `Tcp (Eio.Net.Ipaddr.V4.loopback, port) in + let sock = Eio.Net.listen net ~sw ~reuse_addr:true ~backlog:5 addr in + let stopResult = + Eio.Net.run_server sock + (req_handler trace sw fs clock proc_mgr) + ~on_error ?stop:(Some stop_promise) + in + Eio.traceln "StopResult=%s" stopResult + + let run port trace env stop_promise = + let net = Eio.Stdenv.net env in + let fs = Eio.Stdenv.fs env in + let clock = Eio.Stdenv.clock env in + let proc_mgr = Eio.Stdenv.process_mgr env in + Eio.Switch.run @@ switch net port trace stop_promise fs clock proc_mgr +end + +(** Entry point. *) +let run transport trace env stop_promise = + match transport with + | Stdio -> OnStdio.run trace env + | Socket port -> OnSocket.run port trace env stop_promise diff --git a/lsp/lib/server/server.mli b/lsp/lib/server/server.mli new file mode 100644 index 00000000..ed5a6e5d --- /dev/null +++ b/lsp/lib/server/server.mli @@ -0,0 +1,8 @@ +(** Here we serve the LSP RPC over TCP. + This module contains only the generic server-related functions. + *) + +type transport = Stdio | Socket of int + +val run : + transport -> bool -> Eio_unix.Stdenv.base -> string Eio.Std.Promise.t -> unit diff --git a/lsp/lib/server/session.ml b/lsp/lib/server/session.ml new file mode 100644 index 00000000..ae3cdafe --- /dev/null +++ b/lsp/lib/server/session.ml @@ -0,0 +1,370 @@ +open Prover +module LspT = Lsp.Types +module DocUriSet = Set.Make (LspT.DocumentUri) + +(* A reference to a doc_uri * version * prover launch counter. *) +type doc_ref = LspT.DocumentUri.t * int * int + +type events = + | LspEOF + | LspPacket of Jsonrpc.Packet.t + | TlapmEvent of doc_ref * Toolbox.Msg.t + | TimerTick + +type mode = Initializing | Ready | Shutdown + +type t = { + event_taker : unit -> events; + event_adder : events -> unit; + output_adder : Jsonrpc.Packet.t option -> unit; + last_req_id : int; + next_p_ref : int; + paths : string list; (** Additional paths to look for TLA+ modules. *) + progress : Prover.Progress.t; + mode : mode; + docs : Docs.t; + prov : Prover.t; + (** Prover that is currently running. + We are always running not more than 1 prover to + avoid their interference via fingerprints, etc. *) + delayed : DocUriSet.t; + (** Docs which have delayed proof info updates. + We use this to buffer the updates to the UI.*) + current_ps : LspT.Location.t option; + (** The proof step that is currently selected. + We will send state updates for it. *) +} + +let with_docs' st f = + match st.mode with + | Initializing -> Error "initializing" + | Ready -> + let st', docs' = f (st, st.docs) in + Ok { st' with docs = docs' } + | Shutdown -> Error "going to shutdown" + +let with_docs st f = + match with_docs' st f with + | Ok st' -> st' + | Error err -> + Eio.traceln "Ignoring request: %s" err; + st + +(* For callbacks. *) +let lsp_send st p = + st.output_adder (Some p); + st + +module ProverProgress = Prover.Progress.Make (struct + type nonrec t = t + + let lsp_send = lsp_send + + let next_req_id st = + let next = st.last_req_id + 1 in + (`Int next, { st with last_req_id = next }) + + let with_progress st f = + let st, progress = f st st.progress in + { st with progress } +end) + +let send_diagnostics diagnostics st uri vsn = + let open LspT in + let d_par = + PublishDiagnosticsParams.create ~diagnostics ~uri ~version:vsn () + in + let d_ntf = Lsp.Server_notification.PublishDiagnostics d_par in + let d_pkg = + Jsonrpc.Packet.Notification (Lsp.Server_notification.to_jsonrpc d_ntf) + in + st.output_adder (Some d_pkg) + +let send_proof_state_markers marks st uri = + let open Structs in + let jsonrpc_notif = + Jsonrpc.Notification.create + ~params: + (`List + [ + LspT.DocumentUri.yojson_of_t uri; + `List (List.map TlapsProofStepMarker.yojson_of_t marks); + ]) + ~method_:"tlaplus/tlaps/proofStepMarkers" () + in + let lsp_notif = Lsp.Server_notification.UnknownNotification jsonrpc_notif in + let lsp_packet = + Jsonrpc.Packet.Notification (Lsp.Server_notification.to_jsonrpc lsp_notif) + in + st.output_adder (Some lsp_packet) + +let send_obligation_proof_state st = + let open Structs in + let maybe_st = + with_docs' st @@ fun (st, docs) -> + let docs, notif_data = + match st.current_ps with + | None -> (docs, None) + | Some loc -> + let tlapm_range = Range.of_lsp_range loc.range in + let position = Range.from tlapm_range in + Docs.get_proof_step_details_latest docs loc.uri position + in + let notif_packet = TlapsProofStepDetails.to_jsonrpc_packet notif_data in + st.output_adder (Some notif_packet); + (st, docs) + in + match maybe_st with Ok st -> st | Error _ -> st + +let send_proof_info st uri vsn res = + match res with + | Some res -> + (* Send the current proof step info, if it is in the [uri] file. *) + let st = + match st.current_ps with + | Some current_ps when current_ps.uri = uri -> ( + match DocUriSet.mem current_ps.uri st.delayed with + | true -> send_obligation_proof_state st + | false -> st) + | Some _other -> st + | None -> st + in + (* And then the diagnostics and markers. *) + let diags, marks = Docs.Doc_proof_res.as_lsp res in + send_diagnostics diags st uri vsn; + send_proof_state_markers marks st uri; + let delayed = DocUriSet.remove uri st.delayed in + { st with delayed } + | None -> st + +let send_latest_proof_info st uri = + let docs, vsn_opt, proof_res_opt = Docs.get_proof_res_latest st.docs uri in + let st = { st with docs } in + match (vsn_opt, proof_res_opt) with + | None, _ -> send_proof_info st uri 0 (Some Docs.Doc_proof_res.empty) + | Some vsn, None -> send_proof_info st uri vsn (Some Docs.Doc_proof_res.empty) + | Some vsn, Some p_res -> send_proof_info st uri vsn (Some p_res) + +let delay_proof_info st uri = + let delayed = DocUriSet.add uri st.delayed in + { st with delayed } + +let parser_fun loader_paths = Parser.module_of_string ~loader_paths + +module SessionHandlers = Handlers.Make (struct + module LspT = LspT + + type nonrec t = t + + let ready st = + match st.mode with + | Initializing -> { st with mode = Ready } + | Ready -> st + | Shutdown -> st + + let shutdown st = + match st.mode with + | Initializing -> { st with mode = Shutdown } + | Ready -> { st with mode = Shutdown } + | Shutdown -> st + + let lsp_send = lsp_send + let with_docs = with_docs + + let use_paths st paths = + Eio.traceln "Will use paths: %s" (String.concat ":" paths); + let docs = Docs.with_parser st.docs (parser_fun paths) in + { st with paths; docs } + + let prove_step st (uri : LspT.DocumentUri.t) (vsn : int) + (range : LspT.Range.t) = + Eio.traceln "PROVE_STEP: %s#%d lines %d--%d" + (LspT.DocumentUri.to_string uri) + vsn range.start.line range.end_.line; + let p_ref = st.next_p_ref in + let st = { st with next_p_ref = st.next_p_ref + 1 } in + let docs, proof_opt = + Docs.prover_prepare st.docs uri vsn (Range.of_lsp_range range) ~p_ref + in + let st = { st with docs } in + match proof_opt with + | Some (doc_text, p_range, proof_res) -> ( + let st = ProverProgress.proof_started ~p_ref st in + let st = send_proof_info st uri vsn (Some proof_res) in + let prov_events e = + st.event_adder (TlapmEvent ((uri, vsn, p_ref), e)) + in + match + Prover.start_async st.prov uri doc_text p_range st.paths prov_events + () + with + | Ok prov' -> { st with prov = prov' } + | Error msg -> + Eio.traceln "failed to launch prover: %s" msg; + st) + | None -> + Eio.traceln "cannot find doc/vsn"; + st + + let cancel st (progress_token : LspT.ProgressToken.t) = + match ProverProgress.is_latest st.progress progress_token with + | true -> + let prov = Prover.cancel_all st.prov in + { st with prov } + | false -> st + + let suggest_proof_range st uri range = + let range = Range.of_lsp_range range in + let docs, res = Docs.suggest_proof_range st.docs uri range in + let st = { st with docs } in + match res with + | None -> (st, None) + | Some (vsn, p_range) -> (st, Some (vsn, Range.as_lsp_range p_range)) + + let track_obligation_proof_state (st : t) uri range = + let st = { st with current_ps = Some (LspT.Location.create ~uri ~range) } in + let st = send_obligation_proof_state st in + st + + let latest_diagnostics st uri = + Eio.traceln "PULL_DIAGS: %s" (LspT.DocumentUri.to_string uri); + let st = send_latest_proof_info st uri in + (st, (0, [])) + + let diagnostic_source = Const.diagnostic_source + + let%test_unit "basics" = + Eio_main.run @@ fun env -> + Eio.Switch.run @@ fun sw -> + let fs = Eio.Stdenv.fs env in + let proc_mgr = Eio.Stdenv.process_mgr env in + let st = + { + mode = Initializing; + event_taker = (fun () -> LspEOF); + event_adder = (fun _ -> ()); + output_adder = (fun _ -> ()); + last_req_id = 0; + next_p_ref = 1; + paths = []; + progress = ProverProgress.make (); + docs = Docs.empty (parser_fun []); + prov = Prover.create sw fs proc_mgr; + delayed = DocUriSet.empty; + current_ps = None; + } + in + let () = + match with_docs' st (fun docs -> docs) with + | Ok _ -> failwith "should fail" + | Error _ -> () + in + let st = ready st in + let st = + match with_docs' st (fun docs -> docs) with + | Ok st -> st + | Error e -> failwith e + in + let st = shutdown st in + let () = + match with_docs' st (fun docs -> docs) with + | Ok _ -> failwith "should fail" + | Error _ -> () + in + () +end) + +let handle_lsp_packet p st = Some (SessionHandlers.handle_jsonrpc_packet p st) + +let handle_toolbox_msg ((uri, vsn, p_ref) : doc_ref) msg st = + let open LspT in + Eio.traceln "handle_Toolbox.Msg.t: uri=%s, vsn=%d, p_ref=%d" + (DocumentUri.to_string uri) + vsn p_ref; + match msg with + | Toolbox.Msg.TlapmNotif notif -> + Eio.traceln "---> TlapmNotif: %s" notif.msg; + let docs, _res = Docs.prover_add_notif st.docs uri vsn p_ref notif in + let st = { st with docs } in + let st = delay_proof_info st uri in + Some st + | Toolbox.Msg.TlapmObligationsNumber obl_count -> + Eio.traceln "---> TlapmObligationsNumber"; + let st = ProverProgress.obl_count ~p_ref ~obl_count st in + Some st + | Toolbox.Msg.TlapmObligationProvers { id; provers } -> + Eio.traceln "---> TlapmObligationProvers, id=%d" id; + let docs, obl_is_final = + Docs.prover_add_obl_provers st.docs uri vsn p_ref id provers + in + let st = { st with docs } in + let st = delay_proof_info st uri in + let st = + match obl_is_final with + | None -> st + | Some false -> st + | Some true -> ProverProgress.obligation_done ~p_ref ~obl_id:id st + in + Some st + | Toolbox.Msg.TlapmObligation obl -> + Eio.traceln "---> TlapmObligation, id=%d" obl.id; + let docs, obl_is_final = Docs.prover_add_obl st.docs uri vsn p_ref obl in + let st = { st with docs } in + let st = delay_proof_info st uri in + let st = + match obl_is_final with + | None -> st + | Some false -> st + | Some true -> ProverProgress.obligation_done ~p_ref ~obl_id:obl.id st + in + Some st + | Toolbox.Msg.TlapmTerminated -> + Eio.traceln "---> TlapmTerminated"; + let st = ProverProgress.proof_ended ~p_ref st in + let docs, res = Docs.prover_terminated st.docs uri vsn p_ref in + let st = { st with docs } in + let st = send_proof_info st uri vsn res in + Some st + +let handle_timer_tick st = + let send_for_doc uri stAcc = + Eio.traceln "Sending delayed proof info for %s " + (LspT.DocumentUri.to_string uri); + send_latest_proof_info stAcc uri + in + let st = DocUriSet.fold send_for_doc st.delayed st in + Some { st with delayed = DocUriSet.empty } + +let handle_event e st = + match e with + | LspEOF -> None + | LspPacket p -> handle_lsp_packet p st + | TlapmEvent (ref, msg) -> handle_toolbox_msg ref msg st + | TimerTick -> handle_timer_tick st + +(* The main event processing loop. + At the exit we send EOF to the output thread. *) +let rec loop st = + match handle_event (st.event_taker ()) st with + | Some st' -> loop st' + | None -> st.output_adder None + +(** Entry point to run the session as a fiber. *) +let run event_taker event_adder output_adder sw fs proc_mgr = + let st = + { + mode = Initializing; + event_taker; + event_adder; + output_adder; + last_req_id = 0; + next_p_ref = 1; + paths = []; + progress = ProverProgress.make (); + docs = Docs.empty (parser_fun []); + prov = Prover.create sw fs proc_mgr; + delayed = DocUriSet.empty; + current_ps = None; + } + in + loop st diff --git a/lsp/lib/server/session.mli b/lsp/lib/server/session.mli new file mode 100644 index 00000000..ee154a43 --- /dev/null +++ b/lsp/lib/server/session.mli @@ -0,0 +1,21 @@ +(** State of a single session/connection with the LSP client. *) + +open Prover +module LspT := Lsp.Types + +type doc_ref = LspT.DocumentUri.t * int * int + +type events = + | LspEOF + | LspPacket of Jsonrpc.Packet.t + | TlapmEvent of doc_ref * Toolbox.Msg.t + | TimerTick + +val run : + (unit -> events) -> + (events -> unit) -> + (Jsonrpc.Packet.t option -> unit) -> + Eio.Switch.t -> + Eio__.Fs.dir_ty Eio.Path.t -> + Eio_unix.Process.mgr_ty Eio.Process.mgr -> + unit diff --git a/lsp/lib/structs.ml b/lsp/lib/structs.ml new file mode 100644 index 00000000..58bc121a --- /dev/null +++ b/lsp/lib/structs.ml @@ -0,0 +1,246 @@ +module LspT = Lsp.Types + +let opt_str o = match o with None -> `Null | Some s -> `String s + +(** Corresponds to + ``` + export interface CountByStepStatus { + proved: number; + failed: number; + omitted: number; + missing: number; + pending: number; + progress: number; + } + ``` +*) +module CountByStepStatus = struct + type t = { + proved : int; + failed : int; + omitted : int; + missing : int; + pending : int; + progress : int; + } + + let make ~proved ~failed ~omitted ~missing ~pending ~progress = + { proved; failed; omitted; missing; pending; progress } + + let yojson_of_t (t : t) = + `Assoc + [ + ("proved", `Int t.proved); + ("failed", `Int t.failed); + ("omitted", `Int t.omitted); + ("missing", `Int t.missing); + ("pending", `Int t.pending); + ("progress", `Int t.progress); + ] +end + +(** Corresponds to + ``` + export interface TlapsProofObligationResult { + prover: string; + meth: string; + status: string; + reason: string | null; + obligation: string | null; // Non-null, if prover failed. + } + ``` +*) +module TlapsProofObligationResult = struct + type t = { + prover : string; + meth : string; + status : string; + reason : string option; + obligation : string option; + } + + let make ~prover ~meth ~status ~reason ~obligation = + { prover; meth; status; reason; obligation } + + let yojson_of_t (t : t) = + `Assoc + [ + ("prover", `String t.prover); + ("meth", `String t.meth); + ("status", `String t.status); + ("reason", opt_str t.reason); + ("obligation", opt_str t.obligation); + ] +end + +(** Corresponds to + ``` + export interface TlapsProofObligationState { + role: string; + range: Range; + status: status; + normalized: string; + results: TlapsProofObligationResult[]; + } + ``` + *) +module TlapsProofObligationState = struct + type t = { + role : string; + range : LspT.Range.t; + status : string; + normalized : string option; + results : TlapsProofObligationResult.t list; + } + + let make ~role ~range ~status ~normalized ~results = + { role; range; status; normalized; results } + + let yojson_of_t (t : t) = + `Assoc + [ + ("role", `String t.role); + ("range", LspT.Range.yojson_of_t t.range); + ("status", `String t.status); + ("normalized", opt_str t.normalized); + ( "results", + `List (List.map TlapsProofObligationResult.yojson_of_t t.results) ); + ] +end + +(** Corresponds to + ``` + export interface TlapsProofStepDetails { + kind: string; + status: string; + location: Location; + obligations: TlapsProofObligationState[]; + sub_count: CountByStepStatus; + } + ``` +*) +module TlapsProofStepDetails = struct + type t = { + kind : string; + status : string; + location : LspT.Location.t; + obligations : TlapsProofObligationState.t list; + sub_count : CountByStepStatus.t; + } + + let make ~kind ~status ~location ~obligations ~sub_count = + { kind; status; location; obligations; sub_count } + + let yojson_of_t (t : t option) = + match t with + | None -> `Null + | Some t -> + `Assoc + [ + ("kind", `String t.kind); + ("status", `String t.status); + ("location", LspT.Location.yojson_of_t t.location); + ( "obligations", + `List + (List.map TlapsProofObligationState.yojson_of_t t.obligations) + ); + ("sub_count", CountByStepStatus.yojson_of_t t.sub_count); + ] + + let to_jsonrpc_packet t = + let notif = + Jsonrpc.Notification.create + ~params:(`List [ yojson_of_t t ]) + ~method_:"tlaplus/tlaps/currentProofStep" () + in + let notif_server = Lsp.Server_notification.UnknownNotification notif in + Jsonrpc.Packet.Notification + (Lsp.Server_notification.to_jsonrpc notif_server) +end + +(** Corresponds to + ``` + interface ProofStepMarker { + status: string; + range: vscode.Range; + hover: string; + } + ``` +*) +module TlapsProofStepMarker : sig + type t + + val make : status:string -> range:LspT.Range.t -> hover:string -> t + val yojson_of_t : t -> Yojson.Safe.t +end = struct + type t = { status : string; range : LspT.Range.t; hover : string } + + let make ~status ~range ~hover = { status; range; hover } + + let yojson_of_t (t : t) = + `Assoc + [ + ("status", `String t.status); + ("range", LspT.Range.yojson_of_t t.range); + ("hover", `String t.hover); + ] +end + +(** Passed by the client with the InitializeParams. + Corresponds to: + ``` + export interface InitRequestInItializationOptions { + moduleSearchPaths: string[] | null | undefined + } + ``` +*) +module InitializationOptions : sig + type t + + val module_search_paths : t -> string list + val t_of_yojson : Yojson.Safe.t option -> t +end = struct + type t = { module_search_paths : string list } + + let module_search_paths t = t.module_search_paths + + let t_of_yojson (y : Yojson.Safe.t option) : t = + match y with + | Some (`Assoc els) -> + let module_search_paths = + match List.assoc_opt "moduleSearchPaths" els with + | None -> [] + | Some (`List cps) -> + List.filter_map + (fun cp -> match cp with `String cp -> Some cp | _ -> None) + cps + | Some _ -> [] + in + { module_search_paths } + | _ -> { module_search_paths = [] } +end + +(** Returned by the server in response to the Initialize request. + Corresponds to: + ``` + export interface InitResponseCapabilitiesExperimental { + moduleSearchPaths: string[] | null | undefined + } + ``` +*) +module ServerCapabilitiesExperimental : sig + type t + + val make : module_search_paths:string list -> t + val yojson_of_t : t -> Yojson.Safe.t +end = struct + type t = { module_search_paths : string list } + + let make ~module_search_paths = { module_search_paths } + + let yojson_of_t (t : t) = + let module_search_paths = + List.map (fun s -> `String s) t.module_search_paths + in + `Assoc [ ("moduleSearchPaths", `List module_search_paths) ] +end diff --git a/lsp/lib/structs.mli b/lsp/lib/structs.mli new file mode 100644 index 00000000..a16c220d --- /dev/null +++ b/lsp/lib/structs.mli @@ -0,0 +1,87 @@ +(** Extensions to the LSP protocol. *) + +module LspT := Lsp.Types + +module CountByStepStatus : sig + type t + + val make : + proved:int -> + failed:int -> + omitted:int -> + missing:int -> + pending:int -> + progress:int -> + t + + val yojson_of_t : t -> Yojson.Safe.t +end + +module TlapsProofObligationResult : sig + type t + + val make : + prover:string -> + meth:string -> + status:string -> + reason:string option -> + obligation:string option -> + t + + val yojson_of_t : t -> Yojson.Safe.t +end + +module TlapsProofObligationState : sig + type t + + val make : + role:string -> + range:LspT.Range.t -> + status:string -> + normalized:string option -> + results:TlapsProofObligationResult.t list -> + t + + val yojson_of_t : t -> Yojson.Safe.t +end + +module TlapsProofStepDetails : sig + type t + + val make : + kind:string -> + status:string -> + location:LspT.Location.t -> + obligations:TlapsProofObligationState.t list -> + sub_count:CountByStepStatus.t -> + t + + val yojson_of_t : t option -> Yojson.Safe.t + val to_jsonrpc_packet : t option -> Jsonrpc.Packet.t +end + +(** This is the structure used to create proof step decorators in the client. *) +module TlapsProofStepMarker : sig + type t + + val make : status:string -> range:LspT.Range.t -> hover:string -> t + val yojson_of_t : t -> Yojson.Safe.t +end + +module InitializationOptions : sig + type t + + val module_search_paths : t -> string list + (** Additional paths to use in TLAPS. *) + + val t_of_yojson : Yojson.Safe.t option -> t +end + +module ServerCapabilitiesExperimental : sig + type t + + val make : module_search_paths:string list -> t + (** Paths proposed by TLAPS for other tools. *) + + val yojson_of_t : t -> Yojson.Safe.t +end diff --git a/lsp/lib/tlapm_lsp_lib.ml b/lsp/lib/tlapm_lsp_lib.ml new file mode 100644 index 00000000..0c735b4d --- /dev/null +++ b/lsp/lib/tlapm_lsp_lib.ml @@ -0,0 +1 @@ +module Server = Server diff --git a/lsp/lib/tlapm_lsp_lib.mli b/lsp/lib/tlapm_lsp_lib.mli new file mode 100644 index 00000000..63420190 --- /dev/null +++ b/lsp/lib/tlapm_lsp_lib.mli @@ -0,0 +1,10 @@ +module Server : sig + type transport = Stdio | Socket of int + + val run : + transport -> + bool -> + Eio_unix.Stdenv.base -> + string Eio.Std.Promise.t -> + unit +end diff --git a/lsp/test/test_obl_expand.tla b/lsp/test/test_obl_expand.tla new file mode 100644 index 00000000..092d0f23 --- /dev/null +++ b/lsp/test/test_obl_expand.tla @@ -0,0 +1,16 @@ +---- MODULE test_obl_expand ---- +EXTENDS FiniteSetTheorems +THEOREM FALSE + <1>1. TRUE OBVIOUS + <1>2. TRUE + <1>3. TRUE + <1>q. QED BY <1>1, <1>2, <1>3 +THEOREM FALSE + <1>q. QED + <2>1. TRUE + <2>q. QED BY <2>1 + ----- MODULE sub ------ + VARIABLE X + LEMMA X = X + ======================= +==== diff --git a/lsp/test/test_proof_steps.tla b/lsp/test/test_proof_steps.tla new file mode 100644 index 00000000..c0e68491 --- /dev/null +++ b/lsp/test/test_proof_steps.tla @@ -0,0 +1,22 @@ +---- MODULE test_proof_steps ---- + +(* +This file is just to check how proof steps are identified for the +steps that take no explicit proofs, but actually generate an obligation. +I.e. HAVE, TAKE, WITNESS. +See: https://lamport.azurewebsites.net/tla/tla2-guide.pdf +*) + +THEOREM + ASSUME NEW P(_) + PROVE (\A n : P(n)) => \E n : P(n) + <1>1. HAVE \A n : P(n) \* Destruct the implication in the goal. + <1>2. \A n : P(n) + <2>1. TAKE n \* Prove forall. + <2>2. P(n) BY <1>1 + <2>q. QED BY <2>2 + <1>3. PICK n : P(n) BY <1>1 + <1>4. WITNESS n + <1>q. QED BY <1>1 + +==== diff --git a/lsp/test/tlapm_mock.sh b/lsp/test/tlapm_mock.sh new file mode 100755 index 00000000..6d8e60d6 --- /dev/null +++ b/lsp/test/tlapm_mock.sh @@ -0,0 +1,128 @@ +#!/bin/bash + +## +## That's a tlapm mock for some of the tlapm_lsp_parser test cases. +## + +trap '{ echo "Interrupted."; exit 1; }' SIGINT + +if [ "$1" != "--toolbox" ] ; then + echo "ERROR: Expected --toolbox as a first argument." + exit 2 +fi + +################################################################################ +function CancelTiming() { +cat << EOF +@!!BEGIN +@!!type:warning +@!!msg:message before delay +@!!END +EOF +# Sleep has to be split in order to stip it faster. +for i in {1..30} ; do sleep 0.1; done +cat << EOF +@!!BEGIN +@!!type:warning +@!!msg:message after delay +@!!END +EOF +} + +################################################################################ +function AbnormalExit() { +cat << EOF +@!!BEGIN +@!!type:warning +@!!msg:this run is going to fail +@!!END +EOF +exit 1 # This. +} + +################################################################################ +function Empty() { +cat << EOF +\* TLAPM version 1.5.0 +\* launched at 2023-09-30 23:39:35 with command line: +\* tlapm --toolbox 0 0 Empty.tla + +@!!BEGIN +@!!type:obligationsnumber +@!!count:0 +@!!END + +(* created new ".tlacache/Empty.tlaps/Some.thy" *) +(* fingerprints written in ".tlacache/Empty.tlaps/fingerprints" *) +File "./Empty.tla", line 1, character 1 to line 5, character 4: +[INFO]: All 0 obligation proved. +EOF +} + +################################################################################ +function Some() { +cat << EOF +\* TLAPM version 1.5.0 +\* launched at 2023-09-30 23:43:15 with command line: +\* tlapm --toolbox 0 0 Some.tla + +(* loading fingerprints in ".tlacache/Some.tlaps/fingerprints" *) +@!!BEGIN +@!!type:obligation +@!!id:1 +@!!loc:5:3:5:10 +@!!status:to be proved +@!!END + +@!!BEGIN +@!!type:obligationsnumber +@!!count:1 +@!!END + +** Unexpanded symbols: --- + +@!!BEGIN +@!!type:obligation +@!!id:1 +@!!loc:5:3:5:10 +@!!status:proved +@!!prover:smt +@!!meth:time-limit: 5; time-used: 0.0 (0%) +@!!already:false +@!!END + +(* created new ".tlacache/Some.tlaps/Some.thy" *) +(* fingerprints written in ".tlacache/Some.tlaps/fingerprints" *) +File "./Some.tla", line 1, character 1 to line 6, character 4: +[INFO]: All 1 obligation proved. +EOF +} + +################################################################################ +function Echo() { +cat <<-EOF +@!!BEGIN +@!!type:warning +@!!msg: +EOF +cat # pipe stdin to stdout. +cat << EOF + +@!!END +EOF +} + +################################################################################ +# We differentiate the testcases by the last argument, which is usually a TLA file. +last_arg=${@: -1} +case "$last_arg" in + CancelTiming.tla) CancelTiming ;; + AbnormalExit.tla) AbnormalExit ;; + Empty.tla) Empty ;; + Some.tla) Some ;; + Echo.tla) Echo ;; + *) + echo "ERROR: Unexpected testcase, last_arg=$last_arg." + exit 2 + ;; +esac diff --git a/misc/tla_mode/dune b/misc/tla_mode/dune index 77f700d1..eaa7e8b0 100644 --- a/misc/tla_mode/dune +++ b/misc/tla_mode/dune @@ -1,3 +1,4 @@ (install (section lib) - (files ("tla-mode.el" as "emacs/tla-mode/tla-mode.el"))) + (files + ("tla-mode.el" as "emacs/tla-mode/tla-mode.el"))) diff --git a/src/alexer.mli b/src/alexer.mli index a324d09f..7c832a07 100644 --- a/src/alexer.mli +++ b/src/alexer.mli @@ -19,4 +19,4 @@ val lex: NOTE: does not handle the beginning-of-file stuff. *) val lex_string: - string -> Token.token LazyList.t * Loc.locus + ?fn:string -> string -> Token.token LazyList.t * Loc.locus diff --git a/src/alexer.mll b/src/alexer.mll index 6b32d377..7653bfbf 100644 --- a/src/alexer.mll +++ b/src/alexer.mll @@ -296,9 +296,9 @@ and comment depth = parse in lex_channel fn ich - let lex_string s = + let lex_string ?(fn = "") s = let lb = Lexing.from_string s in - lb.lex_curr_p <- {pos_fname = ""; pos_cnum = 0; pos_lnum = 1; pos_bol = 0}; + lb.lex_curr_p <- {pos_fname = fn; pos_cnum = 0; pos_lnum = 1; pos_bol = 0}; let buffer = ref [] in let next () = try diff --git a/src/backend.ml b/src/backend.ml index 3fd7ab4a..fa743ed4 100644 --- a/src/backend.ml +++ b/src/backend.ml @@ -9,3 +9,4 @@ module Fingerprints = Fingerprints module Fpfile = Fpfile module Smtlib = Smtlib module Prep = Prep +module Interrupted = Interrupted diff --git a/src/backend.mli b/src/backend.mli index b374b15b..34aed396 100644 --- a/src/backend.mli +++ b/src/backend.mli @@ -67,9 +67,12 @@ module Toolbox: sig val print_message: string -> unit val print_message_url: string -> string -> unit -end + val normalize: bool -> Proof.T.obligation -> Proof.T.obligation +end module Smtlib: sig val repls: (char * string) list end + +module Interrupted = Interrupted diff --git a/src/backend/interrupted.ml b/src/backend/interrupted.ml new file mode 100644 index 00000000..6cc73443 --- /dev/null +++ b/src/backend/interrupted.ml @@ -0,0 +1,3 @@ +let state = Atomic.make false +let is_interrupted () = Atomic.get state +let mark_interrupted () = Atomic.exchange state true diff --git a/src/backend/interrupted.mli b/src/backend/interrupted.mli new file mode 100644 index 00000000..a800e9a5 --- /dev/null +++ b/src/backend/interrupted.mli @@ -0,0 +1,2 @@ +val is_interrupted : unit -> bool +val mark_interrupted : unit -> bool diff --git a/src/backend/prep.ml b/src/backend/prep.ml index 097977c2..00d94257 100644 --- a/src/backend/prep.ml +++ b/src/backend/prep.ml @@ -1416,6 +1416,7 @@ let ship ob fpout thyout record = print_obl_and_msg ob "Proof obligation before `find_meth`:\n"; let ob = find_meth ob in print_obl_and_msg ob "Proof obligation after `find_meth`:\n"; + Toolbox.print_ob_provers ob; let meths = get ob.obl Proof.T.Props.meth in let expand_enabled = List.exists (fun x -> (x = Method.ExpandENABLED)) meths in diff --git a/src/backend/schedule.ml b/src/backend/schedule.ml index a3a080b8..38809eb8 100644 --- a/src/backend/schedule.ml +++ b/src/backend/schedule.ml @@ -117,7 +117,7 @@ let run max_threads tl = let now = Unix.gettimeofday () in (* First check stdin for commands from the toolbox. *) (* "stop" command *) - if Toolbox.is_stopped () then begin + if Toolbox.is_stopped () || Interrupted.is_interrupted () then begin List.iter (fun d -> ignore (kill_process now Stopped_kill d)) running; raise Exit end; diff --git a/src/backend/toolbox.ml b/src/backend/toolbox.ml index 8e502d45..2168a8a2 100644 --- a/src/backend/toolbox.ml +++ b/src/backend/toolbox.ml @@ -144,6 +144,13 @@ let print_message_url msg url = if !Params.toolbox then Toolbox_msg.print_error msg url +let print_ob_provers ob = + if !Params.toolbox then + let provers = Property.get ob.obl Proof.T.Props.meth in + let provers = List.filter_map Method.prover_name_of_tac provers in + let provers = List.unique provers in + Toolbox_msg.print_obligationprovers (Option.get ob.id) provers + let print_ob_number n = if !Params.toolbox then Toolbox_msg.print_obligationsnumber n diff --git a/src/backend/toolbox.mli b/src/backend/toolbox.mli index a57c5a76..404cbf68 100644 --- a/src/backend/toolbox.mli +++ b/src/backend/toolbox.mli @@ -37,6 +37,10 @@ val print_old_res: bool -> unit (* tlapm.ml *) +val print_ob_provers: Proof.T.obligation -> unit val print_ob_number: int -> unit val print_message_url: string -> string -> unit + +(* lsp *) +val normalize : bool -> Proof.T.obligation -> Proof.T.obligation diff --git a/src/dune b/src/dune index 3a389f87..50199be2 100644 --- a/src/dune +++ b/src/dune @@ -1,24 +1,36 @@ (env - (_ - (flags (:standard -w +a-4-7-9-27-29-30-32..42-44-45-48-50-52-60-66..70)))) + (_ + (flags + (:standard -w +a-4-7-9-27-29-30-32..42-44-45-48-50-52-60-66..70)))) (executable - (name tlapm) - (modes byte exe) - (public_name tlapm) - (modules tlapm) - (libraries tlapm_lib) - (promote (until-clean))) ; Required to get `tlapm --version` during a release. + (name tlapm) + (modes byte exe) + (public_name tlapm) + (modules tlapm) + (libraries tlapm_lib) + (promote (until-clean))) ; Required to get `tlapm --version` during a release. (library (name tlapm_lib) - (modules (:standard \ tlapm test_schedule why3_interface abstractor)) + (modules + (:standard \ tlapm test_schedule why3_interface abstractor)) (libraries - unix str dune-site dune-build-info ; main deps. - sexplib) ; for inline tests only (ppx_assert). - (foreign_stubs (language c) (names sysconf_stubs)) - (inline_tests (deps "../test/resources/module/m_save/TLC.tla")) - (preprocess (pps ppx_inline_test ppx_assert))) + unix + threads + str + dune-site + dune-build-info + camlzip ; main deps. + sexplib) + ; for inline tests only (ppx_assert). + (foreign_stubs + (language c) + (names sysconf_stubs)) + (inline_tests + (deps "../test/resources/module/m_save/TLC.tla")) + (preprocess + (pps ppx_inline_test ppx_assert))) (ocamllex alexer) @@ -27,3 +39,6 @@ (sites tlapm)) (include_subdirs unqualified) + +(cram + (deps %{bin:tlapm})) diff --git a/src/errors.ml b/src/errors.ml index 09970ce1..c0434b1a 100644 --- a/src/errors.ml +++ b/src/errors.ml @@ -95,3 +95,9 @@ let set st mesg = Some (Loc.string_of_locus ~cap:true loc) end; msg := Some (mesg^"\n\n"^(sget !msg)) + +let reset () = + Buffer.clear warnbuf; + loc := None; + msg := None; + warning := false; \ No newline at end of file diff --git a/src/errors.mli b/src/errors.mli index b443eebd..df28436d 100644 --- a/src/errors.mli +++ b/src/errors.mli @@ -51,3 +51,5 @@ val loc: string option ref val msg: string option ref val warning: bool ref (* FIXME remove this obsolete variable *) val set: 'a Property.wrapped -> string -> unit + +val reset : unit -> unit \ No newline at end of file diff --git a/src/expr/e_anon.ml b/src/expr/e_anon.ml index 731d4eac..6582ecb9 100644 --- a/src/expr/e_anon.ml +++ b/src/expr/e_anon.ml @@ -209,7 +209,9 @@ class anon_sg = object (self: 'self) let index = depth + 1 in let op = e $$ defn in anon_apply index op args - | Recursive _ -> assert false + | Recursive _ -> + Errors.set defn "Recursive operators not supported by TLAPS"; + failwith "Expr.Anon: Recursive" end (* declared operator *) | Some (depth, ({core=Fresh _} as decl)) -> diff --git a/src/expr/e_levels.ml b/src/expr/e_levels.ml index 5109416c..b071b3b1 100644 --- a/src/expr/e_levels.ml +++ b/src/expr/e_levels.ml @@ -223,6 +223,10 @@ class virtual ['s] level_computation = object (self : 'self) parameters, as declared in `self#hyp` below. *) let f weights values op c = + if List.length weights <> List.length values then ( + Util.eprintf ~at:op_ "Invalid number of arguments"; + Errors.set op_ (Printf.sprintf "Invalid number of arguments"); + failwith "Expr.Levels: ARITY"); let pairs = List.combine weights values in let w (weight, value) = if weight then value else c in let values = List.map w pairs in diff --git a/src/expr/e_subst.ml b/src/expr/e_subst.ml index a72e0db7..74568610 100644 --- a/src/expr/e_subst.ml +++ b/src/expr/e_subst.ml @@ -100,6 +100,7 @@ and app_exprs s es = and normalize ?(cx = Deque.empty) op args = match op.core with | Lambda (vs, e) -> if List.length vs <> List.length args then begin + Errors.set op "Arity mismatch"; Util.eprintf ~at:op "@[Arity mismatch:@,op =@, %a@,args =@, @[%a@]@]@." (Fmt.pp_print_expr (cx, Ctx.dot)) op @@ -442,6 +443,7 @@ class map = object (self : 'self) method normalize ?(cx = Deque.empty) op args = match op.core with | Lambda (vs, e) -> if List.length vs <> List.length args then begin + Errors.set op "Arity mismatch"; Util.eprintf ~at:op "@[Arity mismatch:@,op =@, %a@,args =@, @[%a@]@]@." (Fmt.pp_print_expr (cx, Ctx.dot)) op diff --git a/src/loader.ml b/src/loader.ml new file mode 100644 index 00000000..ea0e86ee --- /dev/null +++ b/src/loader.ml @@ -0,0 +1,125 @@ +module StrMap = Map.Make (String) + +type zip_path = { + zip_file : Zip.in_file Lazy.t; (** The jar/zip file. *) + entry_path : string -> string; + (** Function to obtain a path of a module within the zip file. *) +} + +type t = { + zips : zip_path list; (** All the zip files specified as paths. *) + dirs : string list; (** All the folders specified as paths. *) + mods : string StrMap.t; + (** Maps mod_name to file_content. + A list of files specified explicitly. *) +} + +let rec drop_prefix prefixes path = + match prefixes with + | [] -> None + | prefix :: prefixes -> ( + match String.starts_with ~prefix path with + | true -> + let p_len = String.length prefix in + let path = String.sub path p_len (String.length path - p_len) in + Some path + | false -> drop_prefix prefixes path) + +let drop_prefix_if_any prefixes path = + Option.value ~default:path (drop_prefix prefixes path) + +let make paths = + let partition path (zips, dirs) = + match drop_prefix [ "jar:"; "zip:" ] path with + | Some path -> + let zip_path, entry_path = + match String.split_on_char '!' path with + | [ path ] -> (path, fun p -> p) + | [ file_part; entry_part ] -> ( + let file_part = drop_prefix_if_any [ "file:" ] file_part in + let entry_part = drop_prefix_if_any [ "/" ] entry_part in + match entry_part with + | "" -> (file_part, fun m -> m) + | _ -> (file_part, fun m -> String.concat "/" [ entry_part; m ])) + | _ -> failwith (Format.sprintf "unexpected path format: %s" path) + in + let zip_file = lazy (Zip.open_in zip_path) in + let zip_path = { zip_file; entry_path } in + (zip_path :: zips, dirs) + | None -> (zips, path :: dirs) + in + let zips, dirs = List.fold_right partition paths ([], []) in + { zips; dirs; mods = StrMap.empty } + +let close t = + List.iter + (fun zip_path -> + match Lazy.is_val zip_path.zip_file with + | true -> Zip.close_in (Lazy.force zip_path.zip_file) + | false -> ()) + t.zips; + { t with zips = [] } + +let with_dir t dir_name = + match List.mem dir_name t.dirs with + | true -> t + | false -> { t with dirs = dir_name :: t.dirs } + +let with_module t mod_name content = + let mods = StrMap.add mod_name content t.mods in + { t with mods } + +let rec load_from_zips t mod_name = + let check zip = + let zip_file = Lazy.force zip.zip_file in + match Zip.find_entry zip_file (zip.entry_path mod_name) with + | zip_entry -> Some (Zip.read_entry zip_file zip_entry) + | exception Not_found -> None + in + List.find_map check t.zips + +let load_from_dirs t mod_name = + let try_read_file path = + try + let ic = open_in path in + let content = In_channel.input_all ic in + let () = close_in ic in + Some content + with Sys_error _ -> None + in + let check dir = + let path = Filename.concat dir mod_name in + match Sys.file_exists path with + | true -> try_read_file path + | false -> None + in + match List.find_map check t.dirs with + | None -> load_from_zips t mod_name + | Some content -> Some content + +let load_from_mods t mod_name = + match StrMap.find_opt mod_name t.mods with + | None -> load_from_dirs t mod_name + | Some content -> Some content + +let load t mod_name = load_from_mods t mod_name + +module Global = struct + let loader : t option ref = ref None + + let close () = + match !loader with None -> () | Some l -> loader := Some (close l) + + let reset () = + close (); + loader := None + + let setup paths = + close (); + loader := Some (make paths) + + let add_module mod_name content = + loader := Some (with_module (Option.get !loader) mod_name content) + + let load mod_name = load (Option.get !loader) mod_name +end diff --git a/src/loader.mli b/src/loader.mli new file mode 100644 index 00000000..3e586422 --- /dev/null +++ b/src/loader.mli @@ -0,0 +1,53 @@ +(** This module is responsible for loading modules by name. + It will search for them in the specified paths and zips/jars. + To support the stdin or content from the LSP server it takes + also the module contents explicitly. *) + +type t + +val make : string list -> t +(** Initialize the loader with a set of paths. + The paths can be of two kinds: + - Paths to directories/folders. A regular path is assumed: + + `/path/to/dir/ + + - Paths to zips or jars. They can be of the following format: + + `jar:file:/path/to.jar!path/in/archive/` + + Here `zip` can be specified instead of `jar`. + The `file:` part is optional. + Path in the archive can have the leading `/`, it will be removed. + *) + +val close : t -> t +(** Close all the zips/jars that were opened. *) + +val with_dir : t -> string -> t +(** Add directory to the search path. + Can be used to add the current or file dir temporarily. *) + +val with_module : t -> string -> string -> t +(** Add a specific module explicitly. + Can be used to add the current or file dir temporarily. *) + +val load : t -> string -> string option +(** Resolve a module name to its content. *) + +(** The [Loader.Global] is a wrapper around the [Loader] to make it easier + to pass the instance in the current prover's implementation. + In the future this global module should be removed probably. *) +module Global : sig + val reset : unit -> unit + (** Cleanup all the paths to avoid reusing them in the next iteration. *) + + val setup : string list -> unit + (** Configure new instance with the specified paths. *) + + val add_module : string -> string -> unit + (** Add a module content explicitly. *) + + val load : string -> string option + (** Loads a module by name and returns its content, if found. *) +end diff --git a/src/method.ml b/src/method.ml index f2823b72..df4dab6d 100644 --- a/src/method.ml +++ b/src/method.ml @@ -174,6 +174,10 @@ let prover_meth_of_tac tac = | LevelComparison -> (Some "levelcomparison", None) | Trivial -> (Some "trivial", None) +let prover_name_of_tac tac = + let prover, _meth = prover_meth_of_tac tac in + prover + type result = | Proved of string | Failed of string diff --git a/src/method.mli b/src/method.mli index c786655b..cb5ead85 100644 --- a/src/method.mli +++ b/src/method.mli @@ -37,6 +37,7 @@ val pp_print_method: Format.formatter -> t -> unit (* backend/isabelle.ml *) val prover_meth_of_tac: t -> string option * string option +val prover_name_of_tac: t -> string option (* backend/prep.ml *) val timeout: t -> float diff --git a/src/module.mli b/src/module.mli index 1eb66146..e8f6efdb 100644 --- a/src/module.mli +++ b/src/module.mli @@ -109,6 +109,8 @@ end module Save : sig open T + type module_content = Channel of in_channel | String of string | Filesystem + val module_content_prop: module_content Property.pfuncs val parse_file : ?clock:Timing.clock -> Util.hint -> mule val store_module : ?clock:Timing.clock -> mule -> unit val complete_load : ?clock:Timing.clock -> ?root:string -> modctx -> modctx @@ -144,9 +146,9 @@ module Visit : sig open T class map : object - method module_units: Expr.T.ctx -> M_t.modunit list -> - ctx * M_t.modunit list - method module_unit: ctx -> M_t.modunit -> + method module_units: Expr.T.ctx -> modunit list -> + ctx * modunit list + method module_unit: ctx -> modunit -> ctx * modunit method constants: ctx -> (hint * shape) list -> ctx * modunit_ diff --git a/src/module/m_save.ml b/src/module/m_save.ml index 5953fe1f..470f26b9 100644 --- a/src/module/m_save.ml +++ b/src/module/m_save.ml @@ -28,7 +28,12 @@ let clocking cl fn x = fn x -let file_search fh = + +type module_content = Channel of in_channel | String of string | Filesystem + +let module_content_prop = Property.make "module_content" + +let file_search' fh = if Filename.is_implicit fh.core then let rec scan = function | [] -> None @@ -43,6 +48,23 @@ let file_search fh = Some fh else None +let file_search'' fh = + match file_search' fh with + | None -> ( + match Loader.Global.load fh.core with + | Some content -> + let fh = Property.assign fh module_content_prop (String content) in + Some fh + | None -> None) + | Some fh -> Some fh + +let file_search fh = + match Property.query fh module_content_prop with + | Some (Channel _) + | Some (String _) -> Some fh + | Some Filesystem + | None -> file_search'' fh + let really_parse_file fn = match file_search fn with @@ -52,7 +74,12 @@ let really_parse_file fn = fn.core; failwith "Module.Parser.parse_file" | Some fn -> - let (flex, _) = Alexer.lex fn.core in + let (flex, _) = match Property.query fn module_content_prop with + | Some (Channel ch) -> Alexer.lex_channel fn.core ch + | Some (String str) -> Alexer.lex_string ~fn:fn.core str + | Some Filesystem + | None -> Alexer.lex fn.core + in let hparse = use parse in match P.run hparse ~init:Tla_parser.init ~source:flex with | None -> @@ -207,7 +234,7 @@ let complete_load ?clock ?root:(r="") mcx = (* if module name is also a name of a standrd module, try to load it anyway *) - if (Sm.mem ed.core M_standard.initctx) then + if ((not !Params.prefer_stdlib) && (Sm.mem ed.core M_standard.initctx)) then try let emule = load_module ~root:r ed in mods := Deque.snoc !mods emule; @@ -341,6 +368,7 @@ let%test_module _ = (module struct end M_standard.initctx ls let%test "t1: load external modules correctly for external modules which has the same name as a standard module - load local module" = + Loader.Global.setup []; let test_case_list = [("a",["TLC"],"B")] in let test_case = create_test_case test_case_list in let rfold = List.fold_left Filename.concat ".." ["test"; "resources"; "module"; "m_save"] in @@ -351,6 +379,7 @@ let%test_module _ = (module struct (Sm.find "TLC" (complete_load ~root:rfold test_case)).core.body) let%test "t2: load external modules correctly for external modules which has the same name as a standard module - load standard module" = + Loader.Global.setup []; let test_case_list = [("a",["TLC"],"B")] in let test_case = create_test_case test_case_list in (Sm.mem "TLC" (complete_load test_case)) diff --git a/src/module/m_save.mli b/src/module/m_save.mli index 8709517b..320311aa 100644 --- a/src/module/m_save.mli +++ b/src/module/m_save.mli @@ -1,11 +1,12 @@ (* Writing and loading of modules. -Copyright (C) 2008-2010 INRIA and Microsoft Corporation + Copyright (C) 2008-2010 INRIA and Microsoft Corporation *) open M_t +type module_content = Channel of in_channel | String of string | Filesystem -val parse_file: ?clock:Timing.clock -> Util.hint -> mule -val store_module: ?clock:Timing.clock -> mule -> unit -val complete_load: - ?clock:Timing.clock -> ?root:string -> modctx -> modctx +val module_content_prop : module_content Property.pfuncs +val parse_file : ?clock:Timing.clock -> Util.hint -> mule +val store_module : ?clock:Timing.clock -> mule -> unit +val complete_load : ?clock:Timing.clock -> ?root:string -> modctx -> modctx diff --git a/src/params.ml b/src/params.ml index 1c1dea1b..5ad2fbbd 100644 --- a/src/params.ml +++ b/src/params.ml @@ -31,6 +31,7 @@ let tb_el = ref max_int (* toolbox end line *) let input_files = ref [] (* List of input file names *) let toolbox = ref false (* Run in toolbox mode. *) +let toolbox_vsn = ref 1 (* Toolbox protocol version. *) let no_fp = ref false (* Don't use the fingerprints but still save them with the old ones. *) @@ -48,18 +49,18 @@ let safefp = ref false let wait = ref 3 (* Wait time before sending a "being proved" message to the toolbox. *) +let use_stdin = ref false +(* Read the document from stdin, if only one file is provided as an input. *) + +let prefer_stdlib = ref false +(* If set to true, the TLAPM will prefer the modules from the STDLIB + instead of modules with the same names in the search path. *) + let noproving = ref false (* Don't send any obligation to the back-ends. *) let printallobs = ref false (* print unnormalized and normalized versions of obligations in toolbox mode *) -(* The default library path. The relative paths (-I +some) are based on this. *) -let library_path = - let d = Sys.executable_name in - let d = Filename.dirname (Filename.dirname d) in - let d = Filename.concat d "lib" in - let d = Filename.concat d "tlaps" in - d (* The backends directory should be resolved via the dune sites mechanism. If the sites are not available, then we assume this file layout to locate @@ -97,26 +98,9 @@ type executable = type exec = executable ref -(* If the backends site is not available ([]), then look for executables in the PATH, - otherwise we are in the dune-based build and should look for the backends in the - specified site locations. *) -let path = - match Setup_paths.Sites.backends with - | [] -> - let mydir = Filename.dirname Sys.executable_name in - let auxdir = Filename.concat library_path "bin" in - let extrapath = sprintf ":%s:%s" mydir auxdir in - let path = Sys.getenv "PATH" in - sprintf "%s%s" path extrapath - | backends_site -> - let site_bin bs = Filename.concat bs "bin" in - let site_isa bs = Filename.concat (Filename.concat bs "Isabelle") "bin" in - let site_paths bs = [site_bin bs; site_isa bs] in - let path_elems = List.concat (List.map site_paths backends_site) in - sprintf "%s:%s" (String.concat ":" path_elems) (Sys.getenv "PATH") let path_prefix = - sprintf "PATH='%s';" path + sprintf "PATH='%s';" Paths.backend_path_string let get_exec e = match !e with @@ -143,7 +127,7 @@ let get_exec e = let msg1 = sprintf "Executable %S not found" exec in let msg2 = if Filename.is_relative exec - then sprintf " in this PATH:\n%s\n" path + then sprintf " in this PATH:\n%s\n" Paths.backend_path_string else "." in let msg = msg1 ^ msg2 in @@ -289,18 +273,38 @@ let set_smt_logic logic = smt_logic := logic let max_threads = ref nprocs -(* The actual list of paths at which the library TLA files are searched. *) -let rev_search_path = ref (library_path :: Setup_paths.Sites.stdlib) +let stdlib_search_paths = Paths.stdlib_paths + +(** Finds the actual path containing the STDLIB modules. + The relative paths (-I +some) are based on this. *) +let stdlib_path : string option = + Paths.find_path_containing Paths.stdlib_paths "TLAPS.tla" + +(** The actual list of paths at which the library TLA files are searched. *) +let rev_search_path = ref (match stdlib_path with None -> [] | Some p -> [p]) (* Additional paths are added to the search list by keeping the base path as the first one. *) let add_search_dir dir = + let add dir = + let rsp = !rev_search_path in + let hd, tl = match stdlib_path with None -> ([], rsp) | Some p -> ([p], List.tl rsp) in + if List.for_all (fun lp -> lp <> dir) rsp then + rev_search_path := List.concat([hd; [dir]; tl]) + in let dir = - if dir.[0] = '+' - then Filename.concat library_path (String.sub dir 1 (String.length dir - 1)) + if dir.[0] = '+' then + match stdlib_path with + | None -> failwith "base stdlib path unknown"; + | Some p -> Filename.concat p (String.sub dir 1 (String.length dir - 1)) else dir - in - if List.for_all (fun lp -> lp <> dir) !rev_search_path then - rev_search_path := library_path :: dir :: List.tl !rev_search_path + in add dir + +(* Reset the search path to the specified list. *) +let set_search_path dirs = + let p = match stdlib_path with + | None -> dirs + | Some p -> p :: dirs + in rev_search_path := p let output_dir = ref "." @@ -467,12 +471,16 @@ let external_tool_config force (name, tool) = let configuration toolbox force = + let library_path = (match stdlib_path with + | Some path -> "\"" ^ (String.escaped path) ^ "\""; + | None -> "N/A") + in let lines = [ "version == \"" ^ rawversion () ^ "\"" ; "built_with == \"OCaml " ^ Sys.ocaml_version ^ "\"" ; "tlapm_executable == \"" ^ Sys.executable_name ^ "\"" ; "max_threads == " ^ string_of_int !max_threads - ; "library_path == \"" ^ String.escaped library_path ^ "\"" ] + ; "library_path == " ^ library_path ] @ begin match !rev_search_path with | [] -> ["search_path == << >>"] | [p] -> ["search_path == << \"" ^ p ^ "\" >>"] diff --git a/src/params.mli b/src/params.mli index 1519b2e1..52592cd3 100644 --- a/src/params.mli +++ b/src/params.mli @@ -4,6 +4,9 @@ (* pars/error.ml *) val toolbox: bool ref +val toolbox_vsn: int ref +val use_stdin: bool ref +val prefer_stdlib: bool ref (* expr/fmt.ml *) val debugging: string -> bool @@ -66,6 +69,7 @@ val fp_deb: bool ref val configuration: bool -> bool -> string list (* module/save.ml *) +val stdlib_search_paths : string list val rev_search_path: string list ref val self_sum: Digest.t val use_xtla: bool ref @@ -81,12 +85,13 @@ val tb_sl: int ref val tb_el: int ref val input_files: string list ref val set_default_method: string -> unit -val library_path: string +val stdlib_path: string option val cleanfp: bool ref val fpf_in: string option ref val summary: bool ref val stats: bool ref val add_search_dir: string -> unit +val set_search_path: string list -> unit val keep_going: bool ref (* FIXME check still used ? *) val suppress_all: bool ref val set_smt_logic: string -> unit diff --git a/src/pars/error.ml b/src/pars/error.ml index 85846b17..9176a879 100644 --- a/src/pars/error.ml +++ b/src/pars/error.ml @@ -46,6 +46,10 @@ let print_error ?(verbose = false) ouch (Error (err, locus)) = output_string ouch ints ; flush ouch; + Errors.set + (Util.set_locus (Property.noprops err) locus) + (unexp ^ exps ^ msgs ^ ints); + if !Params.toolbox then Toolbox_msg.print_warning (loc ^ unexp ^ exps ^ msgs ^ ints) diff --git a/src/paths.ml b/src/paths.ml new file mode 100644 index 00000000..7d03a34c --- /dev/null +++ b/src/paths.ml @@ -0,0 +1,30 @@ +(** Take paths from the sites, or fallback to the the path relative to the exec. *) +let site_paths sites sub_path = + match sites with + | [] -> + let bin_dir = Filename.dirname Sys.executable_name in + let prefix_dir = Filename.dirname bin_dir in + [ List.fold_left Filename.concat prefix_dir sub_path ] + | _ :: _ -> sites + +(** A list of paths potentially containing the backend execs. *) +let backend_paths = + site_paths Setup_paths.Sites.backends [ "lib"; "tlapm"; "backends" ] + +(** A list of paths potentially containing the STDLIB modules. *) +let stdlib_paths = + site_paths Setup_paths.Sites.stdlib [ "lib"; "tlapm"; "stdlib" ] + +(** If the backends site is not available ([]), then look for executables in the PATH, + otherwise we are in the dune-based build and should look for the backends in the + specified site locations. *) +let backend_path_string = + let site_bin bs = Filename.concat bs "bin" in + let site_isa bs = List.fold_left Filename.concat bs [ "Isabelle"; "bin" ] in + let site_paths bs = [ site_bin bs; site_isa bs ] in + let path_elems = List.concat (List.map site_paths backend_paths) in + Printf.sprintf "%s:%s" (String.concat ":" path_elems) (Sys.getenv "PATH") + +let find_path_containing paths file = + let find_actual path = Sys.file_exists (Filename.concat path file) in + List.find_opt find_actual paths diff --git a/src/paths.mli b/src/paths.mli new file mode 100644 index 00000000..c3cdab3a --- /dev/null +++ b/src/paths.mli @@ -0,0 +1,4 @@ +val backend_path_string : string +val backend_paths : string list +val stdlib_paths : string list +val find_path_containing : string list -> string -> string option diff --git a/src/proof.mli b/src/proof.mli index 95ae89b1..69245157 100644 --- a/src/proof.mli +++ b/src/proof.mli @@ -144,6 +144,7 @@ end module Parser : sig type supp = Emit | Suppress + val qed_loc_prop : Loc.locus Property.pfuncs val usebody : T.usable Tla_parser.lprs val proof : T.proof Tla_parser.lprs val suppress : supp Tla_parser.lprs diff --git a/src/proof/p_parser.ml b/src/proof/p_parser.ml index 57ff58bd..e2eccc94 100644 --- a/src/proof/p_parser.ml +++ b/src/proof/p_parser.ml @@ -11,6 +11,8 @@ open Expr.T open P_t +let qed_loc_prop : Loc.locus pfuncs = make ~uuid:"2fb9a59e-6c30-11ee-b962-0242ac120002" "Parser.qed_loc" + let enlarge_loc x y = Util.locate x (Loc.merge (Util.get_locus x) (Util.get_locus y)) @@ -59,7 +61,7 @@ and prestep = type step_or_qed = | STEP of step - | QED of proof + | QED of Loc.locus * proof exception Backtrack @@ -140,8 +142,14 @@ and to_steps ?(first = false) currlv ps = match ps with let thislv = Util.locate thislv (Loc.right_of (Util.get_locus s)) in let (ss, qp, ps) = to_steps thislv nps in (s :: ss, qp, ps) - | (QED qp, ps) -> - let qp = { core = {core = Qed qp; props = [Props.step.Property.set sn]} ; props = [Props.step.Property.set sn] } in + | (QED (qed_loc, qp), ps) -> + let loc = Loc.merge qed_loc (Util.get_locus qp) in + let qp = Util.locate (Qed qp) loc in + let qp = Property.assign qp Props.step sn in + let qp = Property.assign qp qed_loc_prop qed_loc in + let qp = Util.locate qp loc in + let qp = Property.assign qp Props.step sn in + let qp = Property.assign qp qed_loc_prop qed_loc in ([], qp, ps) end | p :: _ -> @@ -161,10 +169,12 @@ and to_steps ?(first = false) currlv ps = match ps with Errors.set currlv ("Unexpected end of (sub)proof at level "^(string_of_int currlv.core)^" before QED step\n"); failwith "Proof.Parser" -and to_step currlv st ps = match st.core with +and to_step currlv st ps = + match st.core with | PreQed -> + let qed_loc = Util.get_locus st in let (p, ps) = to_proof (currlv + 1 @@ st) ps in - (QED p, ps) + (QED (qed_loc, p), ps) | PreHide us -> (STEP (Hide us @@ st), ps) | PreUse (supp, onl, us, meth) -> diff --git a/src/proof/p_parser.mli b/src/proof/p_parser.mli index 127a09d9..bd3ee4e9 100644 --- a/src/proof/p_parser.mli +++ b/src/proof/p_parser.mli @@ -7,6 +7,9 @@ type supp = Emit | Suppress +val qed_loc_prop : Loc.locus Property.pfuncs +(** Represents the location of the QED step, excluding its proof. *) + val usebody : P_t.usable Tla_parser.lprs val proof : P_t.proof Tla_parser.lprs val suppress : supp Tla_parser.lprs diff --git a/src/tlapm.t b/src/tlapm.t new file mode 100644 index 00000000..c44345eb --- /dev/null +++ b/src/tlapm.t @@ -0,0 +1,42 @@ +Test the --stdin option + $ cat <&1 | grep -e '^@!!' | grep -v 'time-used') + > ---- MODULE A ---- + > THEOREM + > ASSUME + > NEW A, + > NEW B, + > A, + > A => B + > PROVE B + > OBVIOUS + > ==== + > EOF + @!!BEGIN + @!!type:obligation + @!!id:1 + @!!loc:9:3:9:10 + @!!status:to be proved + @!!END + @!!BEGIN + @!!type:obligationsnumber + @!!count:1 + @!!END + @!!BEGIN + @!!type:obligation + @!!id:1 + @!!loc:9:3:9:10 + @!!status:proved + @!!prover:smt + @!!already:false + @!!END + +Check if an understandable error is reported if an operator is called with wrong number of arguments. + $ cat <&1 | grep -e '^File' -e '^Error') + > ---- MODULE test_bad_op ---- + > Op(x) == TRUE + > Po == Op({}, {}) + > THEOREM Po OBVIOUS + > ==== + > EOF + File "test_bad_op.tla", line 3, characters 7-16: + Error: Invalid number of arguments diff --git a/src/tlapm_args.ml b/src/tlapm_args.ml index 156f32a9..48c8599d 100644 --- a/src/tlapm_args.ml +++ b/src/tlapm_args.ml @@ -33,6 +33,10 @@ let set_target_start s = let set_target_end e = tb_el := if e = 0 then max_int else e +let set_toolbox_vsn vsn = + toolbox := true; + toolbox_vsn := vsn + let set_target_line s = toolbox := true; if s = 0 then begin @@ -59,8 +63,13 @@ let parse_args args opts mods usage_fmt = exit 2 let show_where () = - Printf.printf "%s\n" library_path ; - exit 0 + match stdlib_path with + | Some path -> + Printf.printf "%s\n" path; + exit 0 + | None -> + Printf.printf "N/A\n"; + exit 1 let set_nofp_start s = nofp_sl := s @@ -181,10 +190,18 @@ let init () = blank; "--toolbox", (Arg.Tuple [Arg.Int set_target_start;Arg.Int set_target_end]), " toolbox mode"; + "--toolbox-vsn", (Arg.Int set_toolbox_vsn), + " Toolbox protocol version, 1|2, 1 by default."; "--line", Arg.Int set_target_line, " line to prove"; "--wait", Arg.Set_int wait, "