Commit d0e3d342 authored by Andrei Paskevich's avatar Andrei Paskevich

remove '~debug' option from driver routines

parent 55fc17a9
......@@ -897,7 +897,7 @@ let whytac s gl =
let command = cp.command in
if debug then Format.printf "@[%a@]@\n---@." Pretty.print_task !task;
if debug then Format.printf "@[%a@]@\n---@." (Driver.print_task drv) !task;
let res = Driver.prove_task ~debug ~command ~timelimit drv !task () in
let res = Driver.prove_task ~command ~timelimit drv !task () in
match res.pr_answer with
| Valid -> Tactics.admit_as_an_axiom gl
| Invalid -> error "Invalid"
......
......@@ -76,8 +76,11 @@ let call_prover debug command opt_cout buffer =
if debug then eprintf "Call_provers: prover output:@\n%s@." out;
ret, out, time
let call_on_buffer ?(debug=false) ~command ?(timelimit=0) ?(memlimit=0)
~regexps ~exitcodes ~filename buffer () =
let debug = Debug.register_flag "call_prover"
let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0)
~regexps ~exitcodes ~filename buffer () =
let debug = Debug.test_flag debug in
let on_stdin = ref true in
let on_timelimit = ref false in
let cmd_regexp = Str.regexp "%\\(.\\)" in
......
......@@ -51,8 +51,10 @@ val print_prover_result : Format.formatter -> prover_result -> unit
The output of the prover is printed if and only if the answer is
a [HighFailure] *)
val debug : Debug.flag
(** debug flag for the calling procedure (option "--debug call_prover") *)
val call_on_buffer :
?debug : bool ->
command : string ->
?timelimit : int ->
?memlimit : int ->
......
......@@ -199,12 +199,12 @@ let get_filename drv input_file theory_name goal_name =
let file_of_task drv input_file theory_name task =
get_filename drv input_file theory_name (task_goal task).pr_name.id_string
let call_on_buffer ?debug ~command ?timelimit ?memlimit drv buffer =
let call_on_buffer ~command ?timelimit ?memlimit drv buffer =
let regexps = drv.drv_regexps in
let exitcodes = drv.drv_exitcodes in
let filename = get_filename drv "" "" "" in
Call_provers.call_on_buffer
?debug ~command ?timelimit ?memlimit ~regexps ~exitcodes ~filename buffer
~command ?timelimit ?memlimit ~regexps ~exitcodes ~filename buffer
(** print'n'prove *)
......@@ -239,7 +239,9 @@ let update_task drv task =
in
add_tdecl task goal
let print_task ?(debug=false) drv fmt task =
let print_task drv fmt task =
(* TODO: wrong debug flag, should use one in Trans *)
let debug = Debug.test_flag Call_provers.debug in
let p = match drv.drv_printer with
| None -> raise NoPrinter
| Some p -> p
......@@ -259,11 +261,11 @@ let print_task ?(debug=false) drv fmt task =
let task = List.fold_left apply task transl in
fprintf fmt "@[%a@]@?" printer task
let prove_task ?debug ~command ?timelimit ?memlimit drv task =
let prove_task ~command ?timelimit ?memlimit drv task =
let buf = Buffer.create 1024 in
let fmt = formatter_of_buffer buf in
print_task ?debug drv fmt task; pp_print_flush fmt ();
call_on_buffer ?debug ~command ?timelimit ?memlimit drv buf
print_task drv fmt task; pp_print_flush fmt ();
call_on_buffer ~command ?timelimit ?memlimit drv buf
(* exception report *)
......
......@@ -35,18 +35,15 @@ val load_driver : Env.env -> string -> driver
val file_of_task : driver -> string -> string -> Task.task -> string
val call_on_buffer :
?debug : bool ->
command : string ->
?timelimit : int ->
?memlimit : int ->
driver -> Buffer.t -> unit -> Call_provers.prover_result
val print_task :
?debug : bool ->
driver -> Format.formatter -> Task.task -> unit
val prove_task :
?debug : bool ->
command : string ->
?timelimit : int ->
?memlimit : int ->
......
......@@ -94,7 +94,7 @@ let event_handler () =
if false && debug then
Format.eprintf "Task for prover: %a@."
(Driver.print_task driver) goal;
Driver.prove_task ~debug ~command ~timelimit ~memlimit driver goal
Driver.prove_task ~command ~timelimit ~memlimit driver goal
in
let (_ : Thread.t) = Thread.create
(fun () ->
......
......@@ -337,13 +337,13 @@ let do_task drv fname tname (th : Why.Theory.theory) (task : Task.task) =
match !opt_output, !opt_command with
| None, Some command ->
let res =
Driver.prove_task ~debug ~command ~timelimit ~memlimit drv task ()
Driver.prove_task ~command ~timelimit ~memlimit drv task ()
in
printf "%s %s %s : %a@." fname tname
(task_goal task).Decl.pr_name.Ident.id_string
Call_provers.print_prover_result res
| None, None ->
Driver.print_task ~debug drv std_formatter task
Driver.print_task drv std_formatter task
| Some dir, _ ->
let fname = Filename.basename fname in
let fname =
......@@ -356,7 +356,7 @@ let do_task drv fname tname (th : Why.Theory.theory) (task : Task.task) =
let name = Ident.string_unique !fname_printer (String.sub dest 0 i) in
let ext = String.sub dest i (String.length dest - i) in
let cout = open_out (Filename.concat dir (name ^ ext)) in
Driver.print_task ~debug drv (formatter_of_out_channel cout) task;
Driver.print_task drv (formatter_of_out_channel cout) task;
close_out cout
let do_tasks env drv fname tname th trans task =
......
......@@ -1140,7 +1140,7 @@ let try_prover ~(async:(unit->unit)->unit)
if false && debug then
Format.eprintf "Task for prover: %a@."
(Why.Driver.print_task driver) g.task;
Why.Driver.prove_task ~debug ~command ~timelimit ~memlimit driver g.task
Why.Driver.prove_task ~command ~timelimit ~memlimit driver g.task
with
| e ->
try
......
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