diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/asyncTaskQueue.ml | 4 | ||||
| -rw-r--r-- | stm/stm.ml | 98 | ||||
| -rw-r--r-- | stm/stm.mli | 3 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 8 |
4 files changed, 58 insertions, 55 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 31ede2d8b7..5d9b595d36 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -237,7 +237,7 @@ module Make(T : Task) = struct type queue = { active : Pool.pool; queue : (T.task * expiration) TQueue.t; - cleaner : Thread.t; + cleaner : Thread.t option; } let create size = @@ -250,7 +250,7 @@ module Make(T : Task) = struct { active = Pool.create queue ~size; queue; - cleaner = Thread.create cleaner queue; + cleaner = if size > 0 then Some (Thread.create cleaner queue) else None; } let destroy { active; queue } = diff --git a/stm/stm.ml b/stm/stm.ml index 3386044f26..984a874296 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1044,12 +1044,22 @@ end = struct (* {{{ *) match f acc (id, vcs, ids, tactic, undo) with | `Stop x -> x | `Cont acc -> next acc - + + let undo_costly_in_batch_mode = + CWarnings.create ~name:"undo-batch-mode" ~category:"non-interactive" Pp.(fun v -> + str "Command " ++ Ppvernac.pr_vernac v ++ + str (" is not recommended in batch mode. In particular, going back in the document" ^ + " is not efficient in batch mode due to Coq not caching previous states for memory optimization reasons." ^ + " If your use is intentional, you may want to disable this warning and pass" ^ + " the \"-async-proofs-cache force\" option to Coq.")) + let undo_vernac_classifier v = + if !Flags.batch_mode && !Flags.async_proofs_cache <> Some Flags.Force + then undo_costly_in_batch_mode v; 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 +1067,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 +1097,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 +1395,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 +1535,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 +1986,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 @@ -2001,24 +2010,24 @@ let collect_proof keep cur hd brkind id = | { expr = (VernacRequire _ | VernacImport _) } -> true | ast -> may_pierce_opaque ast in let parent = function Some (p, _) -> p | None -> assert false in - let is_empty = function `Async(_,_,[],_,_) | `MaybeASync(_,_,[],_,_) -> true | _ -> false in + let is_empty = function `Async(_,[],_,_) | `MaybeASync(_,[],_,_) -> true | _ -> false in let rec collect last accn id = let view = VCS.visit id in match view.step with | (`Sideff (ReplayCommand x,_) | `Cmd { cast = x }) - when too_complex_to_delegate x -> `Sync(no_name,None,`Print) + when too_complex_to_delegate x -> `Sync(no_name,`Print) | `Cmd { cast = x } -> collect (Some (id,x)) (id::accn) view.next | `Sideff (ReplayCommand x,_) -> collect (Some (id,x)) (id::accn) view.next (* An Alias could jump everywhere... we hope we can ignore it*) - | `Alias _ -> `Sync (no_name,None,`Alias) + | `Alias _ -> `Sync (no_name,`Alias) | `Fork((_,_,_,_::_::_), _) -> - `Sync (no_name,proof_using_ast last,`MutualProofs) + `Sync (no_name,`MutualProofs) | `Fork((_,_,Doesn'tGuaranteeOpacity,_), _) -> - `Sync (no_name,proof_using_ast last,`Doesn'tGuaranteeOpacity) + `Sync (no_name,`Doesn'tGuaranteeOpacity) | `Fork((_,hd',GuaranteesOpacity,ids), _) when has_proof_using last -> assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch); let name = name ids in - `ASync (parent last,proof_using_ast last,accn,name,delegate name) + `ASync (parent last,accn,name,delegate name) | `Fork((_, hd', GuaranteesOpacity, ids), _) when has_proof_no_using last && not (State.is_cached_and_valid (parent last)) && !Flags.compilation_mode = Flags.BuildVio -> @@ -2027,31 +2036,32 @@ let collect_proof keep cur hd brkind id = let name, hint = name ids, get_hint_ctx loc in let t, v = proof_no_using last in v.expr <- VernacProof(t, Some hint); - `ASync (parent last,proof_using_ast last,accn,name,delegate name) + `ASync (parent last,accn,name,delegate name) with Not_found -> let name = name ids in - `MaybeASync (parent last, None, accn, name, delegate name)) + `MaybeASync (parent last, accn, name, delegate name)) | `Fork((_, hd', GuaranteesOpacity, ids), _) -> assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch); let name = name ids in - `MaybeASync (parent last, None, accn, name, delegate name) + `MaybeASync (parent last, accn, name, delegate name) | `Sideff _ -> warn_deprecated_nested_proofs (); - `Sync (no_name,None,`NestedProof) - | _ -> `Sync (no_name,None,`Unknown) in + `Sync (no_name,`NestedProof) + | _ -> `Sync (no_name,`Unknown) in let make_sync why = function - | `Sync(name,pua,_) -> `Sync (name,pua,why) - | `MaybeASync(_,pua,_,name,_) -> `Sync (name,pua,why) - | `ASync(_,pua,_,name,_) -> `Sync (name,pua,why) in + | `Sync(name,_) -> `Sync (name,why) + | `MaybeASync(_,_,name,_) -> `Sync (name,why) + | `ASync(_,_,name,_) -> `Sync (name,why) in + let check_policy rc = if async_policy () then rc else make_sync `Policy rc in match cur, (VCS.visit id).step, brkind with | (parent, { expr = VernacExactProof _ }), `Fork _, _ | (parent, { expr = VernacTime (_, VernacExactProof _) }), `Fork _, _ -> - `Sync (no_name,None,`Immediate) + `Sync (no_name,`Immediate) | _, _, { VCS.kind = `Edit _ } -> check_policy (collect (Some cur) [] id) | _ -> - if is_defined cur then `Sync (no_name,None,`Transparent) - else if keep == VtDrop then `Sync (no_name,None,`Aborted) + if is_defined cur then `Sync (no_name,`Transparent) + else if keep == VtDrop then `Sync (no_name,`Aborted) else let rc = collect (Some cur) [] id in if is_empty rc then make_sync `AlreadyEvaluated rc @@ -2223,7 +2233,7 @@ let known_state ?(redefine_qed=false) ~cache id = ), `Yes, true | `Qed ({ qast = x; keep; brinfo; brname } as qed, eop) -> let rec aux = function - | `ASync (block_start, pua, nodes, name, delegate) -> (fun () -> + | `ASync (block_start, nodes, name, delegate) -> (fun () -> assert(keep == VtKeep || keep == VtKeepAsAxiom); let drop_pt = keep == VtKeepAsAxiom in let block_stop, exn_info, loc = eop, (id, eop), x.loc in @@ -2270,10 +2280,10 @@ let known_state ?(redefine_qed=false) ~cache id = end; Proof_global.discard_all () ), (if redefine_qed then `No else `Yes), true - | `Sync (name, _, `Immediate) -> (fun () -> + | `Sync (name, `Immediate) -> (fun () -> reach eop; stm_vernac_interp id x; Proof_global.discard_all () ), `Yes, true - | `Sync (name, pua, reason) -> (fun () -> + | `Sync (name, reason) -> (fun () -> log_processing_sync id name reason; reach eop; let wall_clock = Unix.gettimeofday () in @@ -2298,12 +2308,12 @@ let known_state ?(redefine_qed=false) ~cache id = (Printf.sprintf "%.3f" (wall_clock3 -. wall_clock2)); Proof_global.discard_all () ), `Yes, true - | `MaybeASync (start, pua, nodes, name, delegate) -> (fun () -> + | `MaybeASync (start, nodes, name, delegate) -> (fun () -> reach ~cache:`Shallow start; (* no sections *) if CList.is_empty (Environ.named_context (Global.env ())) - then Util.pi1 (aux (`ASync (start, pua, nodes, name, delegate))) () - else Util.pi1 (aux (`Sync (name, pua, `NoPU_NoHint_NoES))) () + then Util.pi1 (aux (`ASync (start, nodes, name, delegate))) () + else Util.pi1 (aux (`Sync (name, `NoPU_NoHint_NoES))) () ), (if redefine_qed then `No else `Yes), true in aux (collect_proof keep (view.next, x) brname brinfo eop) @@ -2373,6 +2383,7 @@ let finish () = | _ -> () let wait () = + finish (); Slaves.wait_all_done (); VCS.print () @@ -2386,7 +2397,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 +2494,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 +2514,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 +2783,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 188b176bab..3f01fca013 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 c2ebea961f..158ad90846 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 |