aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/idetop.ml11
-rw-r--r--stm/asyncTaskQueue.ml12
-rw-r--r--stm/asyncTaskQueue.mli12
-rw-r--r--stm/coqworkmgrApi.ml3
-rw-r--r--stm/coqworkmgrApi.mli2
-rw-r--r--stm/stm.ml29
-rw-r--r--stm/stm.mli2
-rw-r--r--stm/workerPool.ml16
-rw-r--r--stm/workerPool.mli5
-rw-r--r--toplevel/coqargs.ml5
-rw-r--r--toplevel/coqtop.ml2
-rw-r--r--toplevel/workerLoop.ml3
12 files changed, 58 insertions, 44 deletions
diff --git a/ide/idetop.ml b/ide/idetop.ml
index c7638343b0..f39c59f5d8 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -563,8 +563,13 @@ let islave_parse ~opts extra_args =
print_string (String.concat "\n" extra_args);
run_mode, []
-let islave_init ~opts =
- CoqworkmgrApi.(init High)
+let islave_init ~opts = ()
+
+let islave_default_opts =
+ Coqargs.{ default with
+ config = { default.config with
+ stm_flags = { default.config.stm_flags with
+ Stm.AsyncOpts.async_proofs_worker_priority = CoqworkmgrApi.High }}}
let () =
let open Coqtop in
@@ -573,5 +578,5 @@ let () =
help = (fun _ -> output_string stderr "Same options as coqtop");
init = islave_init;
run = loop;
- opts = Coqargs.default } in
+ opts = islave_default_opts } in
start_coq custom
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index fa6044fe88..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,7 +123,7 @@ 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"::tl ->
set_slave_opt tl
@@ -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
diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli
index ea438f3f76..e6cf6343c8 100644
--- a/stm/asyncTaskQueue.mli
+++ b/stm/asyncTaskQueue.mli
@@ -144,10 +144,10 @@ module MakeQueue(T : Task) () : sig
(** [queue] is the abstract queue type. *)
type queue
- (** [create n] will initialize the queue with [n] workers. If [n] is
- 0, the queue won't spawn any process, working in a lazy local
- manner. [not imposed by the this API] *)
- val create : int -> queue
+ (** [create n pri] will initialize the queue with [n] workers having
+ priority [pri]. If [n] is 0, the queue won't spawn any process,
+ working in a lazy local manner. [not imposed by the this API] *)
+ val create : int -> CoqworkmgrApi.priority -> queue
(** [destroy q] Deallocates [q], cancelling all pending tasks. *)
val destroy : queue -> unit
@@ -203,9 +203,9 @@ module MakeQueue(T : Task) () : sig
(** [clear q] Clears [q], only if the worker prool is empty *)
val clear : queue -> unit
- (** [with_n_workers n f] create a queue, run the function, destroy
+ (** [with_n_workers n pri f] creates a queue, runs the function, destroys
the queue. The user should call join *)
- val with_n_workers : int -> (queue -> 'a) -> 'a
+ val with_n_workers : int -> CoqworkmgrApi.priority -> (queue -> 'a) -> 'a
end
diff --git a/stm/coqworkmgrApi.ml b/stm/coqworkmgrApi.ml
index c21f057742..92dc77172f 100644
--- a/stm/coqworkmgrApi.ml
+++ b/stm/coqworkmgrApi.ml
@@ -13,7 +13,8 @@ let debug = false
type priority = Low | High
(* Default priority *)
-let async_proofs_worker_priority = ref Low
+
+let default_async_proofs_worker_priority = Low
let string_of_priority = function Low -> "low" | High -> "high"
let priority_of_string = function
diff --git a/stm/coqworkmgrApi.mli b/stm/coqworkmgrApi.mli
index d53af84071..29eba5bc91 100644
--- a/stm/coqworkmgrApi.mli
+++ b/stm/coqworkmgrApi.mli
@@ -15,7 +15,7 @@ val string_of_priority : priority -> string
val priority_of_string : string -> priority
(* Default priority *)
-val async_proofs_worker_priority : priority ref
+val default_async_proofs_worker_priority : priority
(* Connects to a work manager if any. If no worker manager, then
-async-proofs-j and -async-proofs-tac-j are used *)
diff --git a/stm/stm.ml b/stm/stm.ml
index ceb62582cd..4db4579e38 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -51,6 +51,8 @@ module AsyncOpts = struct
async_proofs_tac_error_resilience : tac_error_filter;
async_proofs_cmd_error_resilience : bool;
async_proofs_delegation_threshold : float;
+
+ async_proofs_worker_priority : CoqworkmgrApi.priority;
}
let default_opts = {
@@ -67,6 +69,8 @@ module AsyncOpts = struct
async_proofs_tac_error_resilience = `Only [ "curly" ];
async_proofs_cmd_error_resilience = true;
async_proofs_delegation_threshold = 0.03;
+
+ async_proofs_worker_priority = CoqworkmgrApi.Low;
}
let cur_opt = ref default_opts
@@ -1636,7 +1640,7 @@ and Slaves : sig
val wait_all_done : unit -> unit
(* initialize the whole machinery (optional) *)
- val init : unit -> unit
+ val init : CoqworkmgrApi.priority -> unit
type 'a tasks = (('a,VCS.vcs) Stateid.request * bool) list
val dump_snapshot : unit -> Future.UUID.t tasks
@@ -1658,11 +1662,11 @@ end = struct (* {{{ *)
module TaskQueue = AsyncTaskQueue.MakeQueue(ProofTask) ()
let queue = ref None
- let init () =
+ let init priority =
if async_proofs_is_master !cur_opt then
- queue := Some (TaskQueue.create !cur_opt.async_proofs_n_workers)
+ queue := Some (TaskQueue.create !cur_opt.async_proofs_n_workers priority)
else
- queue := Some (TaskQueue.create 0)
+ queue := Some (TaskQueue.create 0 priority)
let check_task_aux extra name l i =
let { Stateid.stop; document; loc; name = r_name }, drop = List.nth l i in
@@ -1978,7 +1982,7 @@ and Partac : sig
val vernac_interp :
solve:bool -> abstract:bool -> cancel_switch:AsyncTaskQueue.cancel_switch ->
- int -> Stateid.t -> Stateid.t -> aast -> unit
+ int -> CoqworkmgrApi.priority -> Stateid.t -> Stateid.t -> aast -> unit
end = struct (* {{{ *)
@@ -1990,7 +1994,7 @@ end = struct (* {{{ *)
else
f ()
- let vernac_interp ~solve ~abstract ~cancel_switch nworkers safe_id id
+ let vernac_interp ~solve ~abstract ~cancel_switch nworkers priority safe_id id
{ indentation; verbose; expr = e; strlen } : unit
=
let e, time, batch, fail =
@@ -2003,7 +2007,7 @@ end = struct (* {{{ *)
let st = Vernacstate.freeze_interp_state ~marshallable:false in
stm_fail ~st fail (fun () ->
(if time then System.with_time ~batch ~header:(Pp.mt ()) else (fun x -> x)) (fun () ->
- TaskQueue.with_n_workers nworkers (fun queue ->
+ TaskQueue.with_n_workers nworkers priority (fun queue ->
PG_compat.map_proof (fun p ->
let Proof.{goals} = Proof.data p in
let open TacTask in
@@ -2118,7 +2122,7 @@ end (* }}} *)
and Query : sig
- val init : unit -> unit
+ val init : CoqworkmgrApi.priority -> unit
val vernac_interp : cancel_switch:AsyncTaskQueue.cancel_switch -> Stateid.t -> Stateid.t -> aast -> unit
end = struct (* {{{ *)
@@ -2132,7 +2136,7 @@ end = struct (* {{{ *)
TaskQueue.enqueue_task (Option.get !queue)
QueryTask.({ t_where = prev; t_for = id; t_what = q }) ~cancel_switch
- let init () = queue := Some (TaskQueue.create 0)
+ let init priority = queue := Some (TaskQueue.create 0 priority)
end (* }}} *)
@@ -2410,7 +2414,8 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
resilient_tactic id cblock (fun () ->
reach ~cache:true view.next;
Partac.vernac_interp ~solve ~abstract ~cancel_switch
- !cur_opt.async_proofs_n_tacworkers view.next id x)
+ !cur_opt.async_proofs_n_tacworkers
+ !cur_opt.async_proofs_worker_priority view.next id x)
), cache, true
| `Cmd { cast = x; cqueue = `QueryQueue cancel_switch }
when async_proofs_is_master !cur_opt -> (fun () ->
@@ -2679,10 +2684,10 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } =
(* We record the state at this point! *)
State.define ~doc ~cache:true ~redefine:true (fun () -> ()) Stateid.initial;
Backtrack.record ();
- Slaves.init ();
+ Slaves.init stm_options.async_proofs_worker_priority;
if async_proofs_is_master !cur_opt then begin
stm_prerr_endline (fun () -> "Initializing workers");
- Query.init ();
+ Query.init stm_options.async_proofs_worker_priority;
let opts = match !cur_opt.async_proofs_private_flags with
| None -> []
| Some s -> Str.split_delim (Str.regexp ",") s in
diff --git a/stm/stm.mli b/stm/stm.mli
index 92a782d965..29e4b02e3f 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -34,6 +34,8 @@ module AsyncOpts : sig
async_proofs_tac_error_resilience : tac_error_filter;
async_proofs_cmd_error_resilience : bool;
async_proofs_delegation_threshold : float;
+
+ async_proofs_worker_priority : CoqworkmgrApi.priority;
}
val default_opts : stm_opt
diff --git a/stm/workerPool.ml b/stm/workerPool.ml
index 15c6510f7c..f77ced2f3a 100644
--- a/stm/workerPool.ml
+++ b/stm/workerPool.ml
@@ -19,7 +19,7 @@ type 'a cpanel = {
module type PoolModel = sig
(* this shall come from a Spawn.* model *)
type process
- val spawn : int -> worker_id * process * CThread.thread_ic * out_channel
+ val spawn : int -> CoqworkmgrApi.priority -> worker_id * process * CThread.thread_ic * out_channel
(* this defines the main loop of the manager *)
type extra
@@ -79,20 +79,20 @@ let locking { lock; pool = p } f =
x
with e -> Mutex.unlock lock; raise e
-let rec create_worker extra pool id =
+let rec create_worker extra pool priority id =
let cancel = ref false in
- let name, process, ic, oc as worker = Model.spawn id in
+ let name, process, ic, oc as worker = Model.spawn id priority in
master_handshake name ic oc;
- let exit () = cancel := true; cleanup pool; Thread.exit () in
+ let exit () = cancel := true; cleanup pool priority; Thread.exit () in
let cancelled () = !cancel in
let cpanel = { exit; cancelled; extra } in
let manager = CThread.create (Model.manager cpanel) worker in
{ name; cancel; manager; process }
-and cleanup x = locking x begin fun { workers; count; extra_arg } ->
+and cleanup x priority = locking x begin fun { workers; count; extra_arg } ->
workers := List.map (function
| { cancel } as w when !cancel = false -> w
- | _ -> let n = !count in incr count; create_worker extra_arg x n)
+ | _ -> let n = !count in incr count; create_worker extra_arg x priority n)
!workers
end
@@ -102,7 +102,7 @@ end
let is_empty x = locking x begin fun { workers } -> !workers = [] end
-let create extra_arg ~size = let x = {
+let create extra_arg ~size priority = let x = {
lock = Mutex.create ();
pool = {
extra_arg;
@@ -110,7 +110,7 @@ let create extra_arg ~size = let x = {
count = ref size;
}} in
locking x begin fun { workers } ->
- workers := CList.init size (create_worker extra_arg x)
+ workers := CList.init size (create_worker extra_arg x priority)
end;
x
diff --git a/stm/workerPool.mli b/stm/workerPool.mli
index 5a6c968993..5468a24959 100644
--- a/stm/workerPool.mli
+++ b/stm/workerPool.mli
@@ -19,7 +19,8 @@ type 'a cpanel = {
module type PoolModel = sig
(* this shall come from a Spawn.* model *)
type process
- val spawn : int -> worker_id * process * CThread.thread_ic * out_channel
+ val spawn : int -> CoqworkmgrApi.priority ->
+ worker_id * process * CThread.thread_ic * out_channel
(* this defines the main loop of the manager *)
type extra
@@ -31,7 +32,7 @@ module Make(Model : PoolModel) : sig
type pool
- val create : Model.extra -> size:int -> pool
+ val create : Model.extra -> size:int -> CoqworkmgrApi.priority -> pool
val is_empty : pool -> bool
val n_workers : pool -> int
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index b1f823cd1a..d05bf6378a 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -386,8 +386,9 @@ let parse_args ~help ~init arglist : t * string list =
}}}
|"-async-proofs-worker-priority" ->
- CoqworkmgrApi.async_proofs_worker_priority := get_priority opt (next ());
- oval
+ { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
+ Stm.AsyncOpts.async_proofs_worker_priority = get_priority opt (next ())
+ }}}
|"-async-proofs-private-flags" ->
{ oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 79b9d5d501..560ba35a42 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -233,6 +233,7 @@ let init_execution opts custom_init =
let top_lp = Coqinit.toplevel_init_load_path () in
List.iter Loadpath.add_coq_path top_lp;
custom_init ~opts;
+ CoqworkmgrApi.(init opts.config.stm_flags.Stm.AsyncOpts.async_proofs_worker_priority);
Mltop.init_known_plugins ();
(* Configuration *)
Global.set_engagement opts.config.logic.impredicative_set;
@@ -315,7 +316,6 @@ let start_coq custom =
let coqtop_init ~opts =
init_color opts.config;
- CoqworkmgrApi.(init !async_proofs_worker_priority);
Flags.if_verbose print_header ()
let coqtop_parse_extra ~opts extras =
diff --git a/toplevel/workerLoop.ml b/toplevel/workerLoop.ml
index 1fcc106348..c2bd8213b0 100644
--- a/toplevel/workerLoop.ml
+++ b/toplevel/workerLoop.ml
@@ -18,8 +18,7 @@ let worker_parse_extra ~opts extra_args =
let worker_init init ~opts =
Flags.quiet := true;
- init ();
- CoqworkmgrApi.(init !async_proofs_worker_priority)
+ init ()
let start ~init ~loop =
let open Coqtop in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:34:27 +0000