Commit 47a8801e authored by Guillaume Melquiond's avatar Guillaume Melquiond

Record the exit status of a prover as part of its result.

The goal is to keep track of unexpected termination, especially when the
output of the prover is empty.
parent 6793ee63
......@@ -79,6 +79,7 @@ type prover_answer =
type prover_result = {
pr_answer : prover_answer;
pr_status : Unix.process_status;
pr_output : string;
pr_time : float;
}
......@@ -93,9 +94,17 @@ let print_prover_answer fmt = function
| Failure s -> fprintf fmt "Failure: %s" s
| HighFailure -> fprintf fmt "HighFailure"
let print_prover_result fmt {pr_answer=ans; pr_output=out; pr_time=t} =
let print_prover_status fmt = function
| Unix.WSTOPPED n -> fprintf fmt "stopped by signal %d" n
| Unix.WSIGNALED n -> fprintf fmt "killed by signal %d" n
| Unix.WEXITED n -> fprintf fmt "exited with status %d" n
let print_prover_result fmt
{pr_answer=ans; pr_status=status; pr_output=out; pr_time=t} =
fprintf fmt "%a (%.2fs)" print_prover_answer ans t;
if ans == HighFailure then fprintf fmt "@\nProver output:@\n%s@." out
if ans == HighFailure then
fprintf fmt "@\nProver exit status: %a@\nProver output:@\n%s@."
print_prover_status status out
let rec grep out l = match l with
| [] ->
......@@ -186,6 +195,7 @@ let call_on_file ~command ?(timelimit=0) ?(memlimit=0)
| _ -> ans
in
{ pr_answer = ans;
pr_status = ret;
pr_output = out;
pr_time = time }
......
......@@ -37,11 +37,13 @@ type prover_answer =
type prover_result = {
pr_answer : prover_answer;
(* The answer of the prover on the given task *)
(** The answer of the prover on the given task *)
pr_status : Unix.process_status;
(** The process exit status *)
pr_output : string;
(* The output of the prover currently stderr and stdout *)
(** The output of the prover currently stderr and stdout *)
pr_time : float;
(* The time taken by the prover *)
(** The time taken by the prover *)
}
val print_prover_answer : Format.formatter -> prover_answer -> unit
......
......@@ -741,6 +741,7 @@ let load_result r =
Call_provers.pr_answer = answer;
Call_provers.pr_time = time;
Call_provers.pr_output = "";
Call_provers.pr_status = Unix.WEXITED 0
}
| "undone" -> Undone Interrupted
| "unedited" -> Undone Unedited
......
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