Merge remote-tracking branch 'origin/main' into fix-lsp-use

examples/SimpleEventually.tla

@@ -3,33 +3,71 @@
 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 <<Next>>_x
-    BY <1>3, ExpandENABLED DEF Next
-<1>4. ASSUME <<Next>>_x
-      PROVE (x = TRUE)'
-    BY <1>4 DEF Next
+VARIABLE x, y, flip
+vars == <<x, y, flip>>
+
+TypeOK ==
+    /\ x \in BOOLEAN
+    /\ y \in BOOLEAN
+    /\ flip \in BOOLEAN
+
+Init ==
+    /\ x = FALSE
+    /\ y = FALSE
+    /\ flip = FALSE
+
+A ==
+    /\ x = FALSE
+    /\ x' = TRUE
+    /\ UNCHANGED <<y, flip>>
+
+B ==
+    /\ 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 \/ C
+
+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, C
+<1>. QED BY <1>1, <1>2, PTL DEF System, TypeOK, Init, Next, A, B, C
+
+-------------------------------------------------------------------------------
+
+(* 
+    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 <<Next>>_vars... effectively becomes []<>ENABLED <<A>>_vars...
+*)
+THEOREM System => Prop
+<1>1. TypeOK /\ ~(x = TRUE) => ENABLED <<Next>>_vars
+  BY ExpandENABLED DEF TypeOK, Next, A, B, C, vars
+<1>2. TypeOK /\ ~(x = TRUE) /\ (y = TRUE) /\ <<Next>>_vars => (x = TRUE)'
+  BY DEF TypeOK, Next, A, B, C, vars
+<1>3. TypeOK /\ ~(x = TRUE) /\ ~(y = TRUE) /\ ~(x = TRUE)' /\ <<Next>>_vars => (y = TRUE)'
+  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, C, vars
 <1> QED
-    BY <1>2, <1>3, <1>4, PTL DEF System, Init
+  BY TypeCorrect, <1>1, <1>2, <1>3, <1>4, PTL DEF System, Prop
+
 ================================================================================

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
 

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 ->

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

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
 

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. *)

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

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 }
 

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
+  | Error err -> Error err

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 ->

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. *)

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

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. *)

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

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

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

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)

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