From c5e566be9231abbb5838377a6927a1f941d3a693 Mon Sep 17 00:00:00 2001 From: Karolis Petrauskas Date: Mon, 6 Jan 2025 10:34:09 +0200 Subject: [PATCH] Code re-formatted under `./lsp`. No real changes are made, only changes done by `(cd lsp; dune fmt)`. This is to make other PRs less cluttered by the reformatted comments, etc. Signed-off-by: Karolis Petrauskas --- .ocamlformat | 2 +- lsp/lib/docs/doc.mli | 3 +- lsp/lib/docs/doc_actual.ml | 12 ++++---- lsp/lib/docs/doc_proof_res.mli | 5 ++- lsp/lib/docs/doc_vsn.mli | 7 ++--- lsp/lib/docs/docs.mli | 11 ++++--- lsp/lib/docs/obl.ml | 12 ++++---- lsp/lib/docs/proof_step.ml | 56 ++++++++++++++++++---------------- lsp/lib/docs/proof_step.mli | 8 ++--- lsp/lib/docs/util.ml | 7 ++--- lsp/lib/parser/parser.ml | 2 +- lsp/lib/parser/parser.mli | 4 +-- lsp/lib/prover/progress.mli | 9 +++--- lsp/lib/prover/prover.ml | 13 ++++---- lsp/lib/prover/prover.mli | 5 +-- lsp/lib/range.ml | 3 +- lsp/lib/server/codec.mli | 7 ++--- lsp/lib/server/handlers.ml | 22 ++++++------- lsp/lib/server/handlers.mli | 4 +-- lsp/lib/server/server.ml | 3 +- lsp/lib/server/server.mli | 5 ++- lsp/lib/server/session.ml | 21 ++++++------- lsp/lib/structs.mli | 2 +- 23 files changed, 111 insertions(+), 112 deletions(-) diff --git a/.ocamlformat b/.ocamlformat index 8adea03e..f2116634 100644 --- a/.ocamlformat +++ b/.ocamlformat @@ -1,2 +1,2 @@ -version=0.26.2 +version=0.27.0 profile=default diff --git a/lsp/lib/docs/doc.mli b/lsp/lib/docs/doc.mli index 5b5e0dce..878e3d3a 100644 --- a/lsp/lib/docs/doc.mli +++ b/lsp/lib/docs/doc.mli @@ -1,4 +1,5 @@ -(** Represents a document identified by its uri. It can contain multiple versions and all the related info. *) +(** Represents a document identified by its uri. It can contain multiple + versions and all the related info. *) open Util diff --git a/lsp/lib/docs/doc_actual.ml b/lsp/lib/docs/doc_actual.ml index dcdf0f8e..a0869112 100644 --- a/lsp/lib/docs/doc_actual.ml +++ b/lsp/lib/docs/doc_actual.ml @@ -8,9 +8,9 @@ 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. *) + (** 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 @@ -42,9 +42,9 @@ type 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. *) +(** 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 -> diff --git a/lsp/lib/docs/doc_proof_res.mli b/lsp/lib/docs/doc_proof_res.mli index bc807f21..197a27c8 100644 --- a/lsp/lib/docs/doc_proof_res.mli +++ b/lsp/lib/docs/doc_proof_res.mli @@ -1,6 +1,5 @@ -(** Proof results of a document. Includes the errors returned from the prover - as well as all the proof steps with their current state. - *) +(** 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 diff --git a/lsp/lib/docs/doc_vsn.mli b/lsp/lib/docs/doc_vsn.mli index 5fa0e4bd..a453ff7c 100644 --- a/lsp/lib/docs/doc_vsn.mli +++ b/lsp/lib/docs/doc_vsn.mli @@ -1,7 +1,6 @@ -(** 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. - *) +(** 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 diff --git a/lsp/lib/docs/docs.mli b/lsp/lib/docs/docs.mli index a48b3dab..15e2e2e9 100644 --- a/lsp/lib/docs/docs.mli +++ b/lsp/lib/docs/docs.mli @@ -17,7 +17,7 @@ type t (** A document store type. *) type parser_fun = Util.parser_fun -(** Parser function to use to parse modules. *) +(** Parser function to use to parse modules. *) type tk = LspT.DocumentUri.t (** Key type to identify documents. *) @@ -38,7 +38,8 @@ 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. *) +(** Either add document or its revision. Forgets all previous unused revisions. +*) val rem : t -> tk -> t (** Remove a document with all its revisions. *) @@ -71,7 +72,8 @@ 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. *) +(** 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. *) @@ -86,4 +88,5 @@ val get_proof_step_details : 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. *) +(** 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 index d5bdb221..36615061 100644 --- a/lsp/lib/docs/obl.ml +++ b/lsp/lib/docs/obl.ml @@ -23,8 +23,8 @@ type t = { 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. *) + (** 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; @@ -95,8 +95,8 @@ let is_for_obl_id obl p_ref obl_id = 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. *) +(** 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 @@ -112,8 +112,8 @@ 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. *) +(** 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 diff --git a/lsp/lib/docs/proof_step.ml b/lsp/lib/docs/proof_step.ml index c7544e5d..4f20079d 100644 --- a/lsp/lib/docs/proof_step.ml +++ b/lsp/lib/docs/proof_step.ml @@ -1,7 +1,8 @@ open Util open Prover -(** We categorize the proof steps just to make the presentation in the UI clearer. *) +(** We categorize the proof steps just to make the presentation in the UI + clearer. *) module Kind = struct type t = Module | Struct | Leaf @@ -13,31 +14,30 @@ end type t = { kind : Kind.t; - (** Kind/Type of this proof step. - We want to show the proof steps differently based in its type. *) + (** 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 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. *) + (** 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. *) + (** 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. *) + (** 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). *) + (** [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. *) + (** 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. *) } @@ -290,13 +290,15 @@ and of_step (step : Tlapm_lib.Proof.T.step) acc : t option * Acc.t = (of_implicit_proof_step (Range.of_wrapped_must step) suppl_locs acc) | Proof.T.TakeTuply tuply_bounds -> let suppl_locs = - List.concat (List.map (fun (tuply_name, _) -> - begin match tuply_name with - | Expr.T.Bound_name hint -> - List.filter_map Range.of_wrapped [ hint ] - | Expr.T.Bound_names hints -> - List.filter_map Range.of_wrapped hints - end) tuply_bounds) + List.concat + (List.map + (fun (tuply_name, _) -> + match tuply_name with + | Expr.T.Bound_name hint -> + List.filter_map Range.of_wrapped [ hint ] + | Expr.T.Bound_names hints -> + List.filter_map Range.of_wrapped hints) + tuply_bounds) in Acc.some (of_implicit_proof_step (Range.of_wrapped_must step) suppl_locs acc) diff --git a/lsp/lib/docs/proof_step.mli b/lsp/lib/docs/proof_step.mli index 7325c665..c67ab5d7 100644 --- a/lsp/lib/docs/proof_step.mli +++ b/lsp/lib/docs/proof_step.mli @@ -1,8 +1,6 @@ -(** 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. - *) +(** 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 diff --git a/lsp/lib/docs/util.ml b/lsp/lib/docs/util.ml index 30d7d660..9f027c76 100644 --- a/lsp/lib/docs/util.ml +++ b/lsp/lib/docs/util.ml @@ -1,7 +1,6 @@ -(** 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. - *) +(** 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 } diff --git a/lsp/lib/parser/parser.ml b/lsp/lib/parser/parser.ml index b24dca02..6d2d3b95 100644 --- a/lsp/lib/parser/parser.ml +++ b/lsp/lib/parser/parser.ml @@ -4,4 +4,4 @@ let module_of_string ~content ~filename ~loader_paths = ~prefer_stdlib:true with | Ok (_mcx, mule) -> Ok mule - | Error err -> Error err \ No newline at end of file + | Error err -> Error err diff --git a/lsp/lib/parser/parser.mli b/lsp/lib/parser/parser.mli index c89e24ea..61b3df55 100644 --- a/lsp/lib/parser/parser.mli +++ b/lsp/lib/parser/parser.mli @@ -1,6 +1,6 @@ (** Responsible for parsing the TLA+ documents. - TODO: SANY integration should be added here as well. - *) + + TODO: SANY integration should be added here as well. *) val module_of_string : content:string -> diff --git a/lsp/lib/prover/progress.mli b/lsp/lib/prover/progress.mli index cc7329f3..768c24dc 100644 --- a/lsp/lib/prover/progress.mli +++ b/lsp/lib/prover/progress.mli @@ -1,7 +1,6 @@ -(** 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. *) +(** 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 @@ -21,7 +20,7 @@ module Make (CB : Callbacks) : sig (** Create new instance of progress tracker. *) val is_latest : t -> LspT.ProgressToken.t -> bool - (** Checks if the token is of the last progress. *) + (** 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. *) diff --git a/lsp/lib/prover/prover.ml b/lsp/lib/prover/prover.ml index dfc7f4bb..8d19b195 100644 --- a/lsp/lib/prover/prover.ml +++ b/lsp/lib/prover/prover.ml @@ -9,18 +9,19 @@ 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: +(** 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: + + Otherwise, if that's development environment, the files are: - .../src/tlapm.exe - .../lsp/bin/tlapm_lsp.exe - And during the inline tests: + + 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 diff --git a/lsp/lib/prover/prover.mli b/lsp/lib/prover/prover.mli index e8022f67..0624eba2 100644 --- a/lsp/lib/prover/prover.mli +++ b/lsp/lib/prover/prover.mli @@ -66,7 +66,7 @@ module Progress : sig (** Create new instance of progress tracker. *) val is_latest : t -> LspT.ProgressToken.t -> bool - (** Checks if the token is of the last progress. *) + (** 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. *) @@ -75,7 +75,8 @@ module Progress : sig (** 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. *) + (** 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. *) diff --git a/lsp/lib/range.ml b/lsp/lib/range.ml index c5266505..a0e10a34 100644 --- a/lsp/lib/range.ml +++ b/lsp/lib/range.ml @@ -122,7 +122,8 @@ let lines_intersect a b = 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. *) +(** [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 diff --git a/lsp/lib/server/codec.mli b/lsp/lib/server/codec.mli index fc169e38..60291995 100644 --- a/lsp/lib/server/codec.mli +++ b/lsp/lib/server/codec.mli @@ -1,7 +1,6 @@ -(** -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. -*) +(** 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 diff --git a/lsp/lib/server/handlers.ml b/lsp/lib/server/handlers.ml index f4e8f8ea..4bc49f71 100644 --- a/lsp/lib/server/handlers.ml +++ b/lsp/lib/server/handlers.ml @@ -129,16 +129,16 @@ module Make (CB : Callbacks) = struct ~workDoneProgress:true ()) ~diagnosticProvider: (`DiagnosticOptions - (DiagnosticOptions.create ~identifier:CB.diagnostic_source - ~interFileDependencies:false ~workspaceDiagnostics:false - ~workDoneProgress:false ())) + (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" ] - ())) + (CodeActionOptions.create ~resolveProvider:false + ~workDoneProgress:false + ~codeActionKinds: + [ CodeActionKind.Other "tlaplus.tlaps.check-step.ca" ] + ())) ~experimental: Structs.ServerCapabilitiesExperimental.( yojson_of_t @@ -280,10 +280,8 @@ module Make (CB : Callbacks) = struct (Printf.sprintf "command unknown: %s" unknown) cb_state - (** - Provide code actions for a document. - - Code actions can be used for proof decomposition, probably. - *) + (** 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 diff --git a/lsp/lib/server/handlers.mli b/lsp/lib/server/handlers.mli index cbe81b2d..0ea94812 100644 --- a/lsp/lib/server/handlers.mli +++ b/lsp/lib/server/handlers.mli @@ -18,8 +18,8 @@ module type Callbacks = sig 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. *) + (** 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) diff --git a/lsp/lib/server/server.ml b/lsp/lib/server/server.ml index c6325a6d..aa2b9a0f 100644 --- a/lsp/lib/server/server.ml +++ b/lsp/lib/server/server.ml @@ -5,7 +5,8 @@ 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. *) +(** 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 diff --git a/lsp/lib/server/server.mli b/lsp/lib/server/server.mli index ed5a6e5d..85a5c301 100644 --- a/lsp/lib/server/server.mli +++ b/lsp/lib/server/server.mli @@ -1,6 +1,5 @@ -(** Here we serve the LSP RPC over TCP. - This module contains only the generic server-related functions. - *) +(** Here we serve the LSP RPC over TCP. This module contains only the generic + server-related functions. *) type transport = Stdio | Socket of int diff --git a/lsp/lib/server/session.ml b/lsp/lib/server/session.ml index ae3cdafe..1e4bf1ff 100644 --- a/lsp/lib/server/session.ml +++ b/lsp/lib/server/session.ml @@ -24,15 +24,14 @@ type 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. *) + (** 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.*) + (** 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. *) + (** The proof step that is currently selected. We will send state updates + for it. *) } let with_docs' st f = @@ -86,10 +85,10 @@ let send_proof_state_markers marks st uri = Jsonrpc.Notification.create ~params: (`List - [ - LspT.DocumentUri.yojson_of_t uri; - `List (List.map TlapsProofStepMarker.yojson_of_t marks); - ]) + [ + 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 diff --git a/lsp/lib/structs.mli b/lsp/lib/structs.mli index a16c220d..e1cceba0 100644 --- a/lsp/lib/structs.mli +++ b/lsp/lib/structs.mli @@ -72,7 +72,7 @@ module InitializationOptions : sig type t val module_search_paths : t -> string list - (** Additional paths to use in TLAPS. *) + (** Additional paths to use in TLAPS. *) val t_of_yojson : Yojson.Safe.t option -> t end