From 0e88295ceea10ac42d6579b52ef2c82d81018f01 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Wed, 5 Jun 2024 17:07:59 -0700 Subject: [PATCH 1/8] Make SimpleEventually proof a bit less simple. Signed-off-by: Markus Alexander Kuppe --- examples/SimpleEventually.tla | 83 +++++++++++++++++++++++------------ 1 file changed, 56 insertions(+), 27 deletions(-) diff --git a/examples/SimpleEventually.tla b/examples/SimpleEventually.tla index 04a0d3da8..fc7d4fd4a 100644 --- a/examples/SimpleEventually.tla +++ b/examples/SimpleEventually.tla @@ -3,33 +3,62 @@ EXTENDS TLAPS -VARIABLE x - - -Init == x = FALSE -Next == x = FALSE /\ x' = TRUE -System == Init /\ [][Next]_x /\ WF_x(Next) - - -THEOREM System => <>(x = TRUE) -<1>1. SUFFICES (System /\ []~(x = TRUE)) => FALSE - BY <1>1, PTL -<1> DEFINE TypeOK == x \in BOOLEAN -<1> HIDE DEF TypeOK -<1>2. (Init /\ [][Next]_x) => []TypeOK - <2>1. Init => TypeOK - BY DEF Init, TypeOK - <2>2. ASSUME TypeOK /\ [Next]_x - PROVE TypeOK' - BY <2>2 DEF TypeOK, Next - <2> QED - BY <2>1, <2>2, PTL -<1>3. ASSUME TypeOK /\ ~(x = TRUE) - PROVE ENABLED <>_x - BY <1>3, ExpandENABLED DEF Next -<1>4. ASSUME <>_x +VARIABLE x, y +vars == <> + +TypeOK == + /\ x \in BOOLEAN + /\ y \in BOOLEAN + +Init == + /\ x = FALSE + /\ y = FALSE + +A == + /\ x = FALSE + /\ x' = TRUE + /\ UNCHANGED y + +B == + /\ y = FALSE + /\ y' = TRUE + /\ UNCHANGED x + +Next == + A \/ B + +System == + Init /\ [][Next]_vars /\ WF_vars(Next) + +Prop == + <>(x = TRUE) + +------------------------------------------------------------------------------- +(* Ordinary safety proof. *) +LEMMA TypeCorrect == System => []TypeOK +<1>1. Init => TypeOK BY DEF Init, TypeOK +<1>2. TypeOK /\ [Next]_vars => TypeOK' BY DEF TypeOK, Next, vars, A, B +<1>. QED BY <1>1, <1>2, PTL DEF System, TypeOK, Init, Next, A, B + +------------------------------------------------------------------------------- + +\* The PM needs this hint for the liveness proof to be accepted. +LEMMA Equiv == ~(x = TRUE) <=> (x = FALSE) OBVIOUS +USE Equiv + +------------------------------------------------------------------------------- + +(* Proof of liveness property. *) +THEOREM System => Prop +<1>1. SUFFICES (System /\ [](x = FALSE)) => FALSE + BY <1>1, PTL DEF Prop +<1>3. ASSUME TypeOK /\ (x = FALSE) + PROVE ENABLED <>_vars + BY <1>3, ExpandENABLED DEF Next, vars, A, B +<1>4. ASSUME <>_vars PROVE (x = TRUE)' - BY <1>4 DEF Next + BY <1>4 DEF Next, vars, A, B <1> QED - BY <1>2, <1>3, <1>4, PTL DEF System, Init + BY TypeCorrect, <1>3, <1>4, PTL DEF System, Init, Prop + ================================================================================ From 63c7e6a2e5be553414df8b60f46d12cd70817c00 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Fri, 7 Jun 2024 13:20:24 -0700 Subject: [PATCH 2/8] Align fairness constraint with the proof. Signed-off-by: Markus Alexander Kuppe --- examples/SimpleEventually.tla | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/SimpleEventually.tla b/examples/SimpleEventually.tla index fc7d4fd4a..b347b0786 100644 --- a/examples/SimpleEventually.tla +++ b/examples/SimpleEventually.tla @@ -28,7 +28,7 @@ Next == A \/ B System == - Init /\ [][Next]_vars /\ WF_vars(Next) + Init /\ [][Next]_vars /\ WF_vars(A) Prop == <>(x = TRUE) From 3857d4739bc89bb95f6eaa05f42f1b05d27cfbf5 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Fri, 7 Jun 2024 13:21:25 -0700 Subject: [PATCH 3/8] Remove bogus lemma. Signed-off-by: Markus Alexander Kuppe --- examples/SimpleEventually.tla | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/examples/SimpleEventually.tla b/examples/SimpleEventually.tla index b347b0786..7309cdc19 100644 --- a/examples/SimpleEventually.tla +++ b/examples/SimpleEventually.tla @@ -42,17 +42,11 @@ LEMMA TypeCorrect == System => []TypeOK ------------------------------------------------------------------------------- -\* The PM needs this hint for the liveness proof to be accepted. -LEMMA Equiv == ~(x = TRUE) <=> (x = FALSE) OBVIOUS -USE Equiv - -------------------------------------------------------------------------------- - (* Proof of liveness property. *) THEOREM System => Prop -<1>1. SUFFICES (System /\ [](x = FALSE)) => FALSE +<1>1. SUFFICES (System /\ []~(x = TRUE)) => FALSE BY <1>1, PTL DEF Prop -<1>3. ASSUME TypeOK /\ (x = FALSE) +<1>3. ASSUME TypeOK /\ ~(x = TRUE) PROVE ENABLED <>_vars BY <1>3, ExpandENABLED DEF Next, vars, A, B <1>4. ASSUME <>_vars From 22e824e2fe05651dbb886d0aecfb77669e454c81 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Fri, 7 Jun 2024 13:27:42 -0700 Subject: [PATCH 4/8] Adopt Stephan's proposed proof. Signed-off-by: Markus Alexander Kuppe --- examples/SimpleEventually.tla | 28 +++++++++++++++++----------- 1 file changed, 17 insertions(+), 11 deletions(-) diff --git a/examples/SimpleEventually.tla b/examples/SimpleEventually.tla index 7309cdc19..c6486bf97 100644 --- a/examples/SimpleEventually.tla +++ b/examples/SimpleEventually.tla @@ -28,7 +28,7 @@ Next == A \/ B System == - Init /\ [][Next]_vars /\ WF_vars(A) + Init /\ [][Next]_vars /\ WF_vars(Next) Prop == <>(x = TRUE) @@ -42,17 +42,23 @@ LEMMA TypeCorrect == System => []TypeOK ------------------------------------------------------------------------------- -(* Proof of liveness property. *) +(* + Proof of liveness property. Informally: + <1>1 proves that x can become true because Next is enabled. + <1>2 proves that x becomes true by taking a Next step if y is already true. + <1>3 proves that y will become true eventually. + <1>4 proves that action B will be disable. Thus, []<>ENABLED <>_vars... effectively becomes []<>ENABLED <>_vars... +*) THEOREM System => Prop -<1>1. SUFFICES (System /\ []~(x = TRUE)) => FALSE - BY <1>1, PTL DEF Prop -<1>3. ASSUME TypeOK /\ ~(x = TRUE) - PROVE ENABLED <>_vars - BY <1>3, ExpandENABLED DEF Next, vars, A, B -<1>4. ASSUME <>_vars - PROVE (x = TRUE)' - BY <1>4 DEF Next, vars, A, B +<1>1. TypeOK /\ ~(x = TRUE) => ENABLED <>_vars + BY ExpandENABLED DEF TypeOK, Next, A, B, vars +<1>2. TypeOK /\ ~(x = TRUE) /\ (y = TRUE) /\ <>_vars => (x = TRUE)' + BY DEF TypeOK, Next, A, B, vars +<1>3. TypeOK /\ ~(x = TRUE) /\ ~(y = TRUE) /\ ~(x = TRUE)' /\ <>_vars => (y = TRUE)' + BY DEF TypeOK, Next, A, B, vars +<1>4. TypeOK /\ (y = TRUE) /\ [Next]_vars => (y = TRUE)' \* Could replace [Next]_vars with UNCHANGED vars. + BY DEF TypeOK, Next, A, B, vars <1> QED - BY TypeCorrect, <1>3, <1>4, PTL DEF System, Init, Prop + BY TypeCorrect, <1>1, <1>2, <1>3, <1>4, PTL DEF System, Prop ================================================================================ From 07326736a0a4af79d35a99e5095f8abd32110c04 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Fri, 7 Jun 2024 14:24:16 -0700 Subject: [PATCH 5/8] Leave note why WF_vars(Next) suffices. Signed-off-by: Markus Alexander Kuppe --- examples/SimpleEventually.tla | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/SimpleEventually.tla b/examples/SimpleEventually.tla index c6486bf97..04726655b 100644 --- a/examples/SimpleEventually.tla +++ b/examples/SimpleEventually.tla @@ -20,7 +20,7 @@ A == /\ UNCHANGED y B == - /\ y = FALSE +\* /\ y = FALSE \* WF_vars(Next) suffices hinges on the fact that a B step disables B (s.t. it leaves the vars unchanged). /\ y' = TRUE /\ UNCHANGED x From e0ce98e8b01738ddc900d757bbd721e87fe615ac Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Fri, 7 Jun 2024 14:57:55 -0700 Subject: [PATCH 6/8] Add a third variable to be able to better discuss stuttering. Signed-off-by: Markus Alexander Kuppe --- examples/SimpleEventually.tla | 31 ++++++++++++++++++++----------- 1 file changed, 20 insertions(+), 11 deletions(-) diff --git a/examples/SimpleEventually.tla b/examples/SimpleEventually.tla index 04726655b..7c9f24add 100644 --- a/examples/SimpleEventually.tla +++ b/examples/SimpleEventually.tla @@ -3,29 +3,38 @@ EXTENDS TLAPS -VARIABLE x, y -vars == <> +VARIABLE x, y, flip +vars == <> TypeOK == /\ x \in BOOLEAN /\ y \in BOOLEAN + /\ flip \in BOOLEAN Init == /\ x = FALSE /\ y = FALSE + /\ flip = FALSE A == /\ x = FALSE /\ x' = TRUE - /\ UNCHANGED y + /\ UNCHANGED <> B == -\* /\ y = FALSE \* WF_vars(Next) suffices hinges on the fact that a B step disables B (s.t. it leaves the vars unchanged). + /\ y = FALSE \* WF_vars(Next) hinges on the fact that a B step disables B, i.e., additional B steps will leave vars unchanged. /\ y' = TRUE + /\ flip' = ~flip + /\ UNCHANGED x + +C == + /\ y = FALSE \* WF_vars(Next) hinges on the fact that a C step disables C. + /\ y' = TRUE + /\ flip' = ~flip /\ UNCHANGED x Next == - A \/ B + A \/ B \/ C System == Init /\ [][Next]_vars /\ WF_vars(Next) @@ -37,8 +46,8 @@ Prop == (* Ordinary safety proof. *) LEMMA TypeCorrect == System => []TypeOK <1>1. Init => TypeOK BY DEF Init, TypeOK -<1>2. TypeOK /\ [Next]_vars => TypeOK' BY DEF TypeOK, Next, vars, A, B -<1>. QED BY <1>1, <1>2, PTL DEF System, TypeOK, Init, Next, A, B +<1>2. TypeOK /\ [Next]_vars => TypeOK' BY DEF TypeOK, Next, vars, A, B, C +<1>. QED BY <1>1, <1>2, PTL DEF System, TypeOK, Init, Next, A, B, C ------------------------------------------------------------------------------- @@ -51,13 +60,13 @@ LEMMA TypeCorrect == System => []TypeOK *) THEOREM System => Prop <1>1. TypeOK /\ ~(x = TRUE) => ENABLED <>_vars - BY ExpandENABLED DEF TypeOK, Next, A, B, vars + BY ExpandENABLED DEF TypeOK, Next, A, B, C, vars <1>2. TypeOK /\ ~(x = TRUE) /\ (y = TRUE) /\ <>_vars => (x = TRUE)' - BY DEF TypeOK, Next, A, B, vars + BY DEF TypeOK, Next, A, B, C, vars <1>3. TypeOK /\ ~(x = TRUE) /\ ~(y = TRUE) /\ ~(x = TRUE)' /\ <>_vars => (y = TRUE)' - BY DEF TypeOK, Next, A, B, vars + BY DEF TypeOK, Next, A, B, C, vars <1>4. TypeOK /\ (y = TRUE) /\ [Next]_vars => (y = TRUE)' \* Could replace [Next]_vars with UNCHANGED vars. - BY DEF TypeOK, Next, A, B, vars + BY DEF TypeOK, Next, A, B, C, vars <1> QED BY TypeCorrect, <1>1, <1>2, <1>3, <1>4, PTL DEF System, Prop From 05a8e2e348dc3c0a9777bf91095fe8f110732ef9 Mon Sep 17 00:00:00 2001 From: Karolis Petrauskas Date: Thu, 2 Jan 2025 22:27:11 +0200 Subject: [PATCH 7/8] Fix instantiation of a module containing USE. It was failing before with `tlapm ending abnormally with Failure("unknown bound variable")`. Signed-off-by: Karolis Petrauskas --- src/module/m_visit.ml | 1 + test/bugs/instance_mutate.tla | 5 +++++ test/bugs/instance_mutate_test.tla | 7 +++++++ 3 files changed, 13 insertions(+) create mode 100644 test/bugs/instance_mutate.tla create mode 100644 test/bugs/instance_mutate_test.tla diff --git a/src/module/m_visit.ml b/src/module/m_visit.ml index 57328662a..b70cec1c4 100644 --- a/src/module/m_visit.ml +++ b/src/module/m_visit.ml @@ -165,6 +165,7 @@ class map = method mutate cx change usable = let mu = Mutate ( change, usable) in + let cx = update_cx cx mu in (cx, mu) method submod cx tla_module = diff --git a/test/bugs/instance_mutate.tla b/test/bugs/instance_mutate.tla new file mode 100644 index 000000000..8572f7fc0 --- /dev/null +++ b/test/bugs/instance_mutate.tla @@ -0,0 +1,5 @@ +---- MODULE instance_mutate ---- +Op(x) == TRUE +USE TRUE +OpAll == \A x : Op(x) +==== diff --git a/test/bugs/instance_mutate_test.tla b/test/bugs/instance_mutate_test.tla new file mode 100644 index 000000000..deb2669fd --- /dev/null +++ b/test/bugs/instance_mutate_test.tla @@ -0,0 +1,7 @@ +---- MODULE instance_mutate_test ---- +(* +Instantiation was failing on use of an operator if there was +a Mutation (USE) involved in the instantiated module. +*) +INSTANCE instance_mutate +==== From c5e566be9231abbb5838377a6927a1f941d3a693 Mon Sep 17 00:00:00 2001 From: Karolis Petrauskas Date: Mon, 6 Jan 2025 10:34:09 +0200 Subject: [PATCH 8/8] 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 8adea03ec..f2116634b 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 5b5e0dce7..878e3d3a2 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 dcdf0f8ee..a08691121 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 bc807f21a..197a27c83 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 5fa0e4bd6..a453ff7c2 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 a48b3dab5..15e2e2e9f 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 d5bdb2213..36615061d 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 c7544e5db..4f20079d4 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 7325c6658..c67ab5d77 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 30d7d6602..9f027c764 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 b24dca02d..6d2d3b953 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 c89e24eab..61b3df555 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 cc7329f3e..768c24dc7 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 dfc7f4bb7..8d19b1955 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 e8022f670..0624eba20 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 c52665055..a0e10a349 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 fc169e382..602919958 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 f4e8f8ea0..4bc49f71a 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 cbe81b2d7..0ea948126 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 c6325a6d8..aa2b9a0fb 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 ed5a6e5de..85a5c3015 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 ae3cdafe1..1e4bf1ff3 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 a16c220dd..e1cceba0d 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