Commit d656be19 authored by François Bobot's avatar François Bobot

some debug

parent 54cd6e48
...@@ -391,7 +391,7 @@ let () = ...@@ -391,7 +391,7 @@ let () =
Pp.Ansi.set_column 0 Pp.Ansi.set_column 0
!nb_done !nb_scheduled !nb_valid !nb_done !nb_scheduled !nb_valid
end; end;
Debug.dprintf Scheduler.debug "%s.%s %a %i with %s : %a@." Debug.dprintf debug "%s.%s %a %i with %s : %a@."
file prob Pretty.print_pr (task_goal task) i tool file prob Pretty.print_pr (task_goal task) i tool
Scheduler.print_pas res; Scheduler.print_pas res;
in in
......
...@@ -183,13 +183,13 @@ let event_handler () = ...@@ -183,13 +183,13 @@ let event_handler () =
in in
incr scheduled_proofs; incr scheduled_proofs;
print_debug_nb_running (); print_debug_nb_running ();
Debug.dprintf debug
"%a is sent to driver;@."
(fun fmt g -> Pretty.print_pr fmt (Task.task_goal g)) goal;
Mutex.unlock queue_lock; Mutex.unlock queue_lock;
Thread.yield (); Thread.yield ();
(* build the prover task from goal in [a] *) (* build the prover task from goal in [a] *)
try try
Debug.dprintf debug
"%a is sent to driver;@."
(fun fmt g -> Pretty.print_pr fmt (Task.task_goal g)) goal;
let call_prover : unit -> unit -> Call_provers.prover_result = let call_prover : unit -> unit -> Call_provers.prover_result =
(* (*
if debug then if debug then
......
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