diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/asyncTaskQueue.ml | 16 | ||||
| -rw-r--r-- | stm/lemmas.ml | 6 | ||||
| -rw-r--r-- | stm/lemmas.mli | 4 | ||||
| -rw-r--r-- | stm/stm.ml | 13 |
4 files changed, 31 insertions, 8 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 49b51b1715..fa6422cdc5 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -298,10 +298,24 @@ module Make(T : Task) = struct let slave_handshake () = Pool.worker_handshake (Option.get !slave_ic) (Option.get !slave_oc) + let pp_pid pp = + (* Breaking all abstraction barriers... very nice *) + let get_xml pp = match Richpp.repr pp with + | Xml_datatype.Element("_", [], xml) -> xml + | _ -> assert false in + Richpp.richpp_of_xml (Xml_datatype.Element("_", [], + get_xml (Richpp.richpp_of_pp Pp.(str (System.process_id ()^ " "))) @ + get_xml pp)) + + let debug_with_pid = Feedback.(function + | { contents = Message(Debug, loc, pp) } as fb -> + { fb with contents = Message(Debug,loc,pp_pid pp) } + | x -> x) + let main_loop () = (* We pass feedback to master *) let slave_feeder oc fb = - Marshal.to_channel oc (RespFeedback fb) []; flush oc in + Marshal.to_channel oc (RespFeedback (debug_with_pid fb)) []; flush oc in Feedback.add_feeder (fun x -> slave_feeder (Option.get !slave_oc) x); Feedback.set_logger Feedback.feedback_logger; (* We ask master to allocate universe identifiers *) diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 50f2b82c3b..022c89ad9a 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -449,7 +449,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook = call_hook (fun exn -> exn) hook strength ref) thms_data in start_proof_univs id ?pl kind ctx t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard -let start_proof_com kind thms hook = +let start_proof_com ?inference_hook kind thms hook = let env0 = Global.env () in let levels = Option.map snd (fst (List.hd thms)) in let evdref = ref (match levels with @@ -459,7 +459,9 @@ let start_proof_com kind thms hook = let thms = List.map (fun (sopt,(bl,t,guard)) -> let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in let t', imps' = interp_type_evars_impls ~impls env evdref t in - evdref := solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref); + let flags = all_and_fail_flags in + let flags = { flags with use_hook = inference_hook } in + evdref := solve_remaining_evars flags env !evdref (Evd.empty,!evdref); let ids = List.map get_name ctx in (compute_proof_name (pi1 kind) sopt, (nf_evar !evdref (it_mkProd_or_LetIn t' ctx), diff --git a/stm/lemmas.mli b/stm/lemmas.mli index f751598f04..39c089be9f 100644 --- a/stm/lemmas.mli +++ b/stm/lemmas.mli @@ -33,7 +33,9 @@ val start_proof_univs : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_ma ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> unit -val start_proof_com : goal_kind -> Vernacexpr.proof_expr list -> +val start_proof_com : + ?inference_hook:Pretyping.inference_hook -> + goal_kind -> Vernacexpr.proof_expr list -> unit declaration_hook -> unit val start_proof_with_initialization : diff --git a/stm/stm.ml b/stm/stm.ml index cf9fa54922..bb4f5f72f3 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -37,10 +37,12 @@ let state_computed, state_computed_hook = Hook.make let state_ready, state_ready_hook = Hook.make ~default:(fun state_id -> ()) () -let forward_feedback, forward_feedback_hook = Hook.make - ~default:(function +let forward_feedback, forward_feedback_hook = + let m = Mutex.create () in + Hook.make ~default:(function | { id = id; route; contents } -> - feedback ~id:id ~route contents) () + try Mutex.lock m; feedback ~id:id ~route contents; Mutex.unlock m + with e -> Mutex.unlock m; raise e) () let parse_error, parse_error_hook = Hook.make ~default:(fun id loc msg -> @@ -2175,7 +2177,10 @@ let known_state ?(redefine_qed=false) ~cache id = Slaves.build_proof ~loc ~drop_pt ~exn_info ~start ~stop ~name in Future.replace ofp fp; - qed.fproof <- Some (fp, cancel) + qed.fproof <- Some (fp, cancel); + (* We don't generate a new state, but we still need + * to install the right one *) + State.install_cached id | { VCS.kind = `Proof _ }, Some _ -> assert false | { VCS.kind = `Proof _ }, None -> reach ~cache:`Shallow start; |