aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm
diff options
context:
space:
mode:
Diffstat (limited to 'stm')
-rw-r--r--stm/asyncTaskQueue.ml2
-rw-r--r--stm/stm.ml39
-rw-r--r--stm/stm.mli3
-rw-r--r--stm/vernac_classifier.ml8
4 files changed, 22 insertions, 30 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index d89bf5d34..5d9b595d3 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -10,7 +10,7 @@ open CErrors
open Pp
open Util
-let stm_pr_err pp = Format.eprintf "%s] @[%a@]%!\n" (System.process_id ()) Pp.pp_with pp
+let stm_pr_err pp = Format.eprintf "%s] @[%a@]\n%!" (System.process_id ()) Pp.pp_with pp
let stm_prerr_endline s = if !Flags.debug then begin stm_pr_err (str s) end else ()
diff --git a/stm/stm.ml b/stm/stm.ml
index 3386044f2..75ec946f0 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1049,7 +1049,7 @@ end = struct (* {{{ *)
try
match v with
| VernacResetInitial ->
- VtStm (VtBack Stateid.initial, true), VtNow
+ VtBack (true, Stateid.initial), VtNow
| VernacResetName (_,name) ->
let id = VCS.get_branch_pos (VCS.current_branch ()) in
(try
@@ -1057,20 +1057,20 @@ end = struct (* {{{ *)
fold_until (fun b (id,_,label,_,_) ->
if b then `Stop id else `Cont (List.mem name label))
false id in
- VtStm (VtBack oid, true), VtNow
+ VtBack (true, oid), VtNow
with Not_found ->
- VtStm (VtBack id, true), VtNow)
+ VtBack (true, id), VtNow)
| VernacBack n ->
let id = VCS.get_branch_pos (VCS.current_branch ()) in
let oid = fold_until (fun n (id,_,_,_,_) ->
if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in
- VtStm (VtBack oid, true), VtNow
+ VtBack (true, oid), VtNow
| VernacUndo n ->
let id = VCS.get_branch_pos (VCS.current_branch ()) in
let oid = fold_until (fun n (id,_,_,tactic,undo) ->
let value = (if tactic then 1 else 0) - undo in
if Int.equal n 0 then `Stop id else `Cont (n-value)) n id in
- VtStm (VtBack oid, true), VtLater
+ VtBack (true, oid), VtLater
| VernacUndoTo _
| VernacRestart as e ->
let m = match e with VernacUndoTo m -> m | _ -> 0 in
@@ -1087,16 +1087,16 @@ end = struct (* {{{ *)
0 id in
let oid = fold_until (fun n (id,_,_,_,_) ->
if Int.equal n 0 then `Stop id else `Cont (n-1)) (n-m-1) id in
- VtStm (VtBack oid, true), VtLater
+ VtBack (true, oid), VtLater
| VernacAbortAll ->
let id = VCS.get_branch_pos (VCS.current_branch ()) in
let oid = fold_until (fun () (id,vcs,_,_,_) ->
match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ())
() id in
- VtStm (VtBack oid, true), VtLater
+ VtBack (true, oid), VtLater
| VernacBacktrack (id,_,_)
| VernacBackTo id ->
- VtStm (VtBack (Stateid.of_int id), not !Flags.batch_mode), VtNow
+ VtBack (not !Flags.batch_mode, Stateid.of_int id), VtNow
| _ -> VtUnknown, VtNow
with
| Not_found ->
@@ -1385,7 +1385,7 @@ end = struct (* {{{ *)
stm_vernac_interp stop
~proof:(pobject, terminator)
{ verbose = false; loc; indentation = 0; strlen = 0;
- expr = (VernacEndProof (Proved (Opaque None,None))) }) in
+ expr = (VernacEndProof (Proved (Opaque,None))) }) in
ignore(Future.join checked_proof);
end;
RespBuiltProof(proof,time)
@@ -1525,7 +1525,7 @@ end = struct (* {{{ *)
Reach.known_state ~cache:`No start;
stm_vernac_interp stop ~proof
{ verbose = false; loc; indentation = 0; strlen = 0;
- expr = (VernacEndProof (Proved (Opaque None,None))) };
+ expr = (VernacEndProof (Proved (Opaque,None))) };
`OK proof
end
with e ->
@@ -1976,7 +1976,6 @@ let collect_proof keep cur hd brkind id =
| id :: _ -> Names.Id.to_string id in
let loc = (snd cur).loc in
let rec is_defined_expr = function
- | VernacEndProof (Proved ((Transparent|Opaque (Some _)),_)) -> true
| VernacTime (_, e) -> is_defined_expr e
| VernacRedirect (_, (_, e)) -> is_defined_expr e
| VernacTimeout (_, e) -> is_defined_expr e
@@ -2373,6 +2372,7 @@ let finish () =
| _ -> ()
let wait () =
+ finish ();
Slaves.wait_all_done ();
VCS.print ()
@@ -2386,7 +2386,6 @@ let rec join_admitted_proofs id =
| _ -> join_admitted_proofs view.next
let join () =
- finish ();
wait ();
stm_prerr_endline (fun () -> "Joining the environment");
Global.join_safe_environment ();
@@ -2484,14 +2483,8 @@ let process_transaction ?(newtip=Stateid.fresh ())
stm_prerr_endline (fun () ->
" classified as: " ^ string_of_vernac_classification c);
match c with
- (* Joining various parts of the document *)
- | VtStm (VtJoinDocument, b), VtNow -> join (); `Ok
- | VtStm (VtWait, b), VtNow -> finish (); wait (); `Ok
- | VtStm ((VtJoinDocument|VtWait),_), VtLater ->
- anomaly(str"classifier: join actions cannot be classified as VtLater.")
-
(* Back *)
- | VtStm (VtBack oid, true), w ->
+ | VtBack (true, oid), w ->
let id = VCS.new_node ~id:newtip () in
let { mine; others } = Backtrack.branches_of oid in
let valid = VCS.get_branch_pos head in
@@ -2510,12 +2503,12 @@ let process_transaction ?(newtip=Stateid.fresh ())
VCS.checkout_shallowest_proof_branch ();
VCS.commit id (Alias (oid,x));
Backtrack.record (); if w == VtNow then finish (); `Ok
- | VtStm (VtBack id, false), VtNow ->
+ | VtBack (false, id), VtNow ->
stm_prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id);
Backtrack.backto id;
VCS.checkout_shallowest_proof_branch ();
Reach.known_state ~cache:(interactive ()) id; `Ok
- | VtStm (VtBack id, false), VtLater ->
+ | VtBack (false, id), VtLater ->
anomaly(str"classifier: VtBack + VtLater must imply part_of_script.")
(* Query *)
@@ -2779,8 +2772,8 @@ let query ~at ~route s =
let clas = classify_vernac ast in
let aast = { verbose = true; indentation; strlen; loc; expr = ast } in
match clas with
- | VtStm (w,_), _ ->
- ignore(process_transaction aast (VtStm (w,false), VtNow))
+ | VtBack (_,id), _ -> (* TODO: can this still happen ? *)
+ ignore(process_transaction aast (VtBack (false,id), VtNow))
| _ ->
ignore(process_transaction aast (VtQuery (false, route), VtNow)))
s
diff --git a/stm/stm.mli b/stm/stm.mli
index 188b176ba..3f01fca01 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -51,6 +51,9 @@ val edit_at : Stateid.t -> [ `NewTip | `Focus of focus ]
(* Evaluates the tip of the current branch *)
val finish : unit -> unit
+(* Internal use (fake_ide) only, do not use *)
+val wait : unit -> unit
+
val observe : Stateid.t -> unit
val stop_worker : string -> unit
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index c2ebea961..158ad9084 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -31,8 +31,7 @@ let string_of_vernac_type = function
Option.default "" proof_block_detection
| VtProofMode s -> "ProofMode " ^ s
| VtQuery (b, route) -> "Query " ^ string_of_in_script b ^ " route " ^ string_of_int route
- | VtStm ((VtJoinDocument|VtWait), b) -> "Stm " ^ string_of_in_script b
- | VtStm (VtBack _, b) -> "Stm Back " ^ string_of_in_script b
+ | VtBack (b, _) -> "Stm Back " ^ string_of_in_script b
let string_of_vernac_when = function
| VtLater -> "Later"
@@ -64,9 +63,6 @@ let rec classify_vernac e =
* look at the entire dag to detect this option. *)
| VernacSetOption (["Universe"; "Polymorphism"],_)
| VernacUnsetOption (["Universe"; "Polymorphism"]) -> VtSideff [], VtNow
- (* Stm *)
- | VernacStm Wait -> VtStm (VtWait, true), VtNow
- | VernacStm JoinDocument -> VtStm (VtJoinDocument, true), VtNow
(* Nested vernac exprs *)
| VernacProgram e -> classify_vernac e
| VernacLocal (_,e) -> classify_vernac e
@@ -79,7 +75,7 @@ let rec classify_vernac e =
| VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
(match classify_vernac e with
| ( VtQuery _ | VtProofStep _ | VtSideff _
- | VtStm _ | VtProofMode _ ), _ as x -> x
+ | VtBack _ | VtProofMode _ ), _ as x -> x
| VtQed _, _ ->
VtProofStep { parallel = `No; proof_block_detection = None },
VtNow
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 12:27:17 +0000