Commit 8dff5008 authored by Johannes Kanig's avatar Johannes Kanig

session scheduler now sets -j option for why3server

parent 5ccaf91f
let standalone : bool ref = ref true
let socket : Unix.file_descr option ref = ref None
let max_running_provers : int ref = ref 1
let set_max_running_provers x =
max_running_provers := x
let client_connect socket_name =
if Sys.os_type = "Win32" then begin
......@@ -70,7 +74,9 @@ let disconnect () =
let run_server () =
let exec = Filename.concat Config.libdir "why3server" in
Unix.create_process exec
[|exec; "--socket"; !socket_name; "--single-client"|]
[|exec; "--socket"; !socket_name;
"--single-client";
"-j"; string_of_int !max_running_provers |]
Unix.stdin Unix.stdout Unix.stderr
let force_connect () =
......
val standalone : bool ref
val set_socket_name : string -> unit
val set_max_running_provers : int -> unit
val connect : unit -> unit
......
......@@ -111,11 +111,13 @@ type t =
}
let set_maximum_running_proofs max sched =
Prove_client.set_max_running_provers max;
(* TODO dequeue actions if maximum_running_proofs increase *)
sched.maximum_running_proofs <- max
let init max =
Debug.dprintf debug "[Sched] init scheduler max=%i@." max;
Prove_client.set_max_running_provers max;
{ actions_queue = Queue.create ();
maximum_running_proofs = max;
running_proofs = [];
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment