diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 34 | ||||
| -rw-r--r-- | stm/stm.mli | 6 |
2 files changed, 24 insertions, 16 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 5c6df26cbb..eff2403eca 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -170,7 +170,7 @@ type fork_t = aast * Vcs_.Branch.t * opacity_guarantee * Names.Id.t list type qed_t = { qast : aast; keep : vernac_qed_type; - mutable fproof : (future_proof * AsyncTaskQueue.cancel_switch) option; + mutable fproof : (future_proof option * AsyncTaskQueue.cancel_switch) option; brname : Vcs_.Branch.t; brinfo : branch_type Vcs_.branch_info } @@ -2460,8 +2460,8 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = let fp, cancel = Slaves.build_proof ~doc ?loc ~drop_pt ~exn_info ~block_start ~block_stop ~name in - Future.replace ofp fp; - qed.fproof <- Some (fp, cancel); + Future.replace (Option.get ofp) fp; + qed.fproof <- Some (Some fp, cancel); (* We don't generate a new state, but we still need * to install the right one *) State.install_cached id @@ -2476,7 +2476,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = ProofTask.build_proof_here ~doc ?loc ~drop_pt exn_info block_stop, ref false in - qed.fproof <- Some (fp, cancel); + qed.fproof <- Some (Some fp, cancel); let opaque = match keep' with | VtKeepAxiom | VtKeepOpaque -> Proof_global.Opaque (* Admitted -> Opaque should be OK. *) @@ -2510,9 +2510,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = match keep with | VtDrop -> None | VtKeep VtKeepAxiom -> - let ctx = UState.empty in - let fp = Future.from_val ([],ctx) in - qed.fproof <- Some (fp, ref false); None + qed.fproof <- Some (None, ref false); None | VtKeep opaque -> let opaque = let open Proof_global in match opaque with | VtKeepOpaque -> Opaque | VtKeepDefined -> Transparent @@ -2709,7 +2707,7 @@ let rec join_admitted_proofs id = let view = VCS.visit id in match view.step with | `Qed ({ keep = VtKeep VtKeepAxiom; fproof = Some (fp,_) },_) -> - ignore(Future.force fp); + Option.iter (fun fp -> ignore(Future.force fp)) fp; join_admitted_proofs view.next | _ -> join_admitted_proofs view.next @@ -2801,13 +2799,21 @@ let handle_failure (e, info) vcs = VCS.print (); Exninfo.iraise (e, info) -let snapshot_vio ~doc ~output_native_objects ldir long_f_dot_vo = +let snapshot_vio ~create_vos ~doc ~output_native_objects ldir long_f_dot_vo = let doc = finish ~doc in if List.length (VCS.branches ()) > 1 then CErrors.user_err ~hdr:"stm" (str"Cannot dump a vio with open proofs"); - Library.save_library_to ~todo:(dump_snapshot ()) ~output_native_objects - ldir long_f_dot_vo - (Global.opaque_tables ()); + (* LATER: when create_vos is true, it could be more efficient to not allocate the futures; but for now it seems useful for synchronization of the workers, + below, [snapshot] gets computed even if [create_vos] is true. *) + let (tasks,counters) = dump_snapshot() in + let except = List.fold_left (fun e (r,_) -> + Future.UUIDSet.add r.Stateid.uuid e) Future.UUIDSet.empty tasks in + let todo_proofs = + if create_vos + then Library.ProofsTodoSomeEmpty except + else Library.ProofsTodoSome (except,tasks,counters) + in + Library.save_library_to todo_proofs ~output_native_objects ldir long_f_dot_vo (Global.opaque_tables ()); doc let reset_task_queue = Slaves.reset_task_queue @@ -2884,7 +2890,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) | VtStartProof (guarantee, names) -> if not (get_allow_nested_proofs ()) && VCS.proof_nesting () > 0 then - "Nested proofs are not allowed unless you turn option Nested Proofs Allowed on." + "Nested proofs are not allowed unless you turn the Nested Proofs Allowed flag on." |> Pp.str |> (fun s -> (UserError (None, s), Exninfo.null)) |> State.exn_on ~valid:Stateid.dummy newtip @@ -3106,7 +3112,7 @@ let edit_at ~doc id = (VCS.reachable (VCS.get_branch_pos (VCS.current_branch ()))) in let has_failed qed_id = match VCS.visit qed_id with - | { step = `Qed ({ fproof = Some (fp,_) }, _) } -> Future.is_exn fp + | { step = `Qed ({ fproof = Some (Some fp,_) }, _) } -> Future.is_exn fp | _ -> false in let rec master_for_br root tip = if Stateid.equal tip Stateid.initial then tip else diff --git a/stm/stm.mli b/stm/stm.mli index 29e4b02e3f..841adcf05b 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -159,8 +159,10 @@ val join : doc:doc -> doc - if the worker pool is empty, all tasks are saved - if the worker proof is not empty, then it waits until all workers are done with their current jobs and then dumps (or fails if one - of the completed tasks is a failure) *) -val snapshot_vio : doc:doc -> output_native_objects:bool -> DirPath.t -> string -> doc + of the completed tasks is a failure). + Note: the create_vos argument is used in the "-vos" mode, where the + proof tasks are not dumped into the output file. *) +val snapshot_vio : create_vos:bool -> doc:doc -> output_native_objects:bool -> DirPath.t -> string -> doc (* Empties the task queue, can be used only if the worker pool is empty (E.g. * after having built a .vio in batch mode *) |