diff options
Diffstat (limited to 'stm/asyncTaskQueue.ml')
| -rw-r--r-- | stm/asyncTaskQueue.ml | 33 |
1 files changed, 24 insertions, 9 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 613ddb4da5..fa6422cdc5 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Pp open Util @@ -60,9 +60,7 @@ module Make(T : Task) = struct type more_data = | MoreDataUnivLevel of Univ.universe_level list - - let request_expiry_of_task (t, c) = T.request_of_task t, c - + let slave_respond (Request r) = let res = T.perform r in Response res @@ -106,7 +104,8 @@ module Make(T : Task) = struct marshal_err ("unmarshal_more_data: "^s) let report_status ?(id = !Flags.async_proofs_worker_id) s = - Pp.feedback ~state_id:Stateid.initial (Feedback.WorkerStatus(id, s)) + let open Feedback in + feedback ~id:(State Stateid.initial) (WorkerStatus(id, s)) module Worker = Spawn.Sync(struct end) @@ -299,11 +298,27 @@ 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 - Pp.set_feeder (fun x -> slave_feeder (Option.get !slave_oc) x); - Pp.log_via_feedback (); + 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 *) Universes.set_remote_new_univ_level (bufferize (fun () -> marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel; match unmarshal_more_data (Option.get !slave_ic) with @@ -342,7 +357,7 @@ module Make(T : Task) = struct let with_n_workers n f = let q = create n in try let rc = f q in destroy q; rc - with e -> let e = Errors.push e in destroy q; iraise e + with e -> let e = CErrors.push e in destroy q; iraise e let n_workers { active } = Pool.n_workers active |