Commit 873821c5 authored by François Bobot's avatar François Bobot

call_provers: add the possibility to wait on all children.

Don't work for Win32 but that keep the possibility for Unix.
parent 2f3e0a7f
......@@ -124,8 +124,12 @@ let rec grep out l = match l with
let debug = Debug.register_info_flag "call_prover"
~desc:"About@ external@ prover@ calls@ and@ results."
type res_waitpid = int * Unix.process_status
type post_prover_call = unit -> prover_result
type prover_call = Unix.wait_flag list -> post_prover_call
type prover_call =
{ call: ?res_waitpid:res_waitpid -> Unix.wait_flag list -> post_prover_call;
pid: int}
type pre_prover_call = unit -> prover_call
let save f = f ^ ".save"
......@@ -173,9 +177,12 @@ let call_on_file ~command ?(timelimit=0) ?(memlimit=0)
Unix.close fd_in;
close_out cout;
fun wait_flags ->
let call = fun ?res_waitpid wait_flags ->
(* TODO? check that we haven't given the result earlier *)
let res,ret = Unix.waitpid wait_flags pid in
let res,ret =
match res_waitpid with
| Some ((res,_) as res_waitpid) when pid = res -> res_waitpid
| _ -> Unix.waitpid wait_flags pid in
if res = 0 then raise Exit;
let time = Unix.gettimeofday () -. time in
let cout = open_in fout in
......@@ -209,7 +216,8 @@ let call_on_file ~command ?(timelimit=0) ?(memlimit=0)
{ pr_answer = ans;
pr_status = ret;
pr_output = out;
pr_time = time }
pr_time = time } in
{call = call; pid = pid}
let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0)
~regexps ~timeregexps ~exitcodes ~filename
......@@ -225,7 +233,17 @@ let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0)
call_on_file ~command ~timelimit ~memlimit
~regexps ~timeregexps ~exitcodes ~cleanup:true ~inplace fin
let query_call call = try Some (call [Unix.WNOHANG]) with Exit -> None
let query_call ?res_waitpid call =
try Some (call.call ?res_waitpid [Unix.WNOHANG]) with Exit -> None
let wait_on_call ?res_waitpid call = call.call ?res_waitpid []
let query_wait_all wait_flags =
let res,_ as res_waitpid = Unix.waitpid wait_flags 0 in
if res = 0 then raise Exit;
res_waitpid
let wait_on_call call = call []
let query_all () = try Some (query_wait_all [Unix.WNOHANG]) with Exit -> None
let wait_all () = query_wait_all []
let prover_call_pid pc = pc.pid
......@@ -68,6 +68,9 @@ val timeregexp : string -> timeregexp
(** Converts a regular expression with special markers '%h','%m',
'%s','%i' (for milliseconds) into a value of type [timeregexp] *)
type res_waitpid = int * Unix.process_status
(** pid of a process that stopped and its status *)
type prover_call
(** Type that represents a single prover run *)
......@@ -121,10 +124,24 @@ val call_on_buffer :
@param filename : the suffix of the proof task's file, if the prover
doesn't accept stdin. *)
val query_call : prover_call -> post_prover_call option
val query_call :
?res_waitpid:res_waitpid -> prover_call -> post_prover_call option
(** Thread-safe non-blocking function that checks if the prover
has finished. *)
val wait_on_call : prover_call -> post_prover_call
val wait_on_call :
?res_waitpid:res_waitpid -> prover_call -> post_prover_call
(** Thread-safe blocking function that waits until the prover finishes. *)
val query_all : unit -> res_waitpid option
(** Just a wrapper around Unix.wait_pid with the same flag than query_call
Don't work on Win32
*)
val wait_all : unit -> res_waitpid
(** Just a wrapper around Unix.wait_pid with the same flag than wait_on_call
Don't work on Win32
*)
val prover_call_pid : prover_call -> int
(** return the pid of the prover *)
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