Merge PR #10246: Investigations in the initialization of coq binaries and command line (part 1)

Reviewed-by: ejgallego
Ack-by: gares
Ack-by: herbelin

1 files changed, 9 insertions, 9 deletions

diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 044ac29e92..909804d0c9 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -115,7 +115,7 @@ module Make(T : Task) () = struct
   type process = Worker.process
   type extra = (T.task * cancel_switch) TQueue.t
 
-  let spawn id =
+  let spawn id priority =
     let name = Printf.sprintf "%s:%d" !T.name id in
     let proc, ic, oc =
       (* Filter arguments for slaves. *)
@@ -123,9 +123,9 @@ module Make(T : Task) () = struct
         | [] -> !async_proofs_flags_for_workers @
                 ["-worker-id"; name;
                  "-async-proofs-worker-priority";
-                 CoqworkmgrApi.(string_of_priority !async_proofs_worker_priority)]
+                 CoqworkmgrApi.(string_of_priority priority)]
         (* Options to discard: 0 arguments *)
-        | ("-emacs"|"-batch")::tl ->
+        | "-emacs"::tl ->
           set_slave_opt tl
         (* Options to discard: 1 argument *)
         | ( "-async-proofs" | "-vio2vo" | "-o"
@@ -155,8 +155,8 @@ module Make(T : Task) () = struct
       let args =
         Array.of_list (set_slave_opt (List.tl (Array.to_list Sys.argv))) in
       let env = Array.append (T.extra_env ()) (Unix.environment ()) in
-    let worker_name = System.get_toplevel_path ("coq" ^ !T.name) in
-    Worker.spawn ~env worker_name args in
+      let worker_name = System.get_toplevel_path ("coq" ^ !T.name) in
+      Worker.spawn ~env worker_name args in
     name, proc, CThread.prepare_in_channel_for_thread_friendly_io ic, oc
 
   let manager cpanel (id, proc, ic, oc) =
@@ -262,7 +262,7 @@ module Make(T : Task) () = struct
     cleaner : Thread.t option;
   }
 
-  let create size =
+  let create size priority =
     let cleaner queue =
       while true do
         try ignore(TQueue.pop ~picky:(fun (_,cancelled) -> !cancelled) queue)
@@ -270,7 +270,7 @@ module Make(T : Task) () = struct
       done in
     let queue = TQueue.create () in
     {
-      active = Pool.create queue ~size;
+      active = Pool.create queue ~size priority;
       queue;
       cleaner = if size > 0 then Some (CThread.create cleaner queue) else None;
     }
@@ -369,8 +369,8 @@ module Make(T : Task) () = struct
      (TQueue.wait_until_n_are_waiting_then_snapshot
        (Pool.n_workers active) queue)
 
-  let with_n_workers n f =
-    let q = create n in
+  let with_n_workers n priority f =
+    let q = create n priority in
     try let rc = f q in destroy q; rc
     with e -> let e = CErrors.push e in destroy q; iraise e