From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 stm/asyncTaskQueue.ml | 48 ++++++++++++++++++++++++++++++++++--------------
 1 file changed, 34 insertions(+), 14 deletions(-)

(limited to 'stm/asyncTaskQueue.ml')

diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index cc973260..fa6422cd 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)
 
@@ -125,7 +124,7 @@ module Make(T : Task) = struct
                  "-async-proofs-worker-priority";
                    Flags.string_of_priority !Flags.async_proofs_worker_priority]
         | ("-ideslave"|"-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl
-        | ("-async-proofs" |"-toploop" |"-vi2vo"
+        | ("-async-proofs" |"-toploop" |"-vio2vo"
           |"-load-vernac-source" |"-l" |"-load-vernac-source-verbose" |"-lv"
           |"-compile" |"-compile-verbose"
           |"-async-proofs-worker-priority" |"-worker-id") :: _ :: tl ->
@@ -184,6 +183,13 @@ module Make(T : Task) = struct
         let () = Unix.sleep 1 in
         kill_if ()
     in
+    let kill_if () =
+      try kill_if ()
+      with Sys.Break ->
+        let () = stop_waiting := true in
+        let () = TQueue.broadcast queue in
+        Worker.kill proc
+    in
     let _ = Thread.create kill_if () in
 
     try while true do
@@ -223,10 +229,8 @@ module Make(T : Task) = struct
     | (Die | TQueue.BeingDestroyed) ->
         giveback_exec_token (); kill proc; exit ()
     | Sys_error _ | Invalid_argument _ | End_of_file ->
-        giveback_exec_token ();
         T.on_task_cancellation_or_expiration_or_slave_death !last_task;
-        kill proc;
-        exit ()
+        giveback_exec_token (); kill proc; exit ()
   end
 
   module Pool = WorkerPool.Make(Model)
@@ -294,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
@@ -314,7 +334,7 @@ module Make(T : Task) = struct
         let response = slave_respond request in
         report_status "Idle";
         marshal_response (Option.get !slave_oc) response;
-        Ephemeron.clear ()
+        CEphemeron.clear ()
       with
       | MarshalError s ->
         pr_err ("Fatal marshal error: " ^ s); flush_all (); exit 2
@@ -337,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
 
-- 
cgit v1.2.3