allow the use of more than 1 task in parallel

Added a monitor in the IDE

src/ide/why3ide.ml

@@ -6,6 +6,8 @@ open Stdlib
 open Session_itp
 open Controller_itp
 
+external reset_gc : unit -> unit = "ml_reset_gc"
+
 let debug = Debug.lookup_flag "ide_info"
 
 (************************)
@@ -211,8 +213,16 @@ let task_view =
 
 let vbox2222 = GPack.vbox ~packing:vpan222#add  ()
 
-let command_entry =
-  GEdit.entry ~packing:(vbox2222#pack ?from:None ?expand:None ?fill:None ?padding:None) ()
+let hbox22221 =
+  GPack.hbox
+    ~packing:(vbox2222#pack ?from:None ?expand:None ?fill:None ?padding:None) ()
+
+let command_entry = GEdit.entry ~packing:hbox22221#add ()
+
+let monitor =
+  GMisc.label
+    ~text:"0/0/0"
+    ~packing:(hbox22221#pack ?from:None ?expand:None ?fill:None ?padding:None) ()
 
 let message_zone =
   let sv = GBin.scrolled_window
@@ -222,6 +232,27 @@ let message_zone =
   GText.view ~editable:false ~cursor_visible:false
     ~packing:sv#add ()
 
+(**** Monitor *****)
+
+let fan n =
+  match n mod 4 with
+    | 0 -> "|"
+    | 1 | -3 -> "\\"
+    | 2 | -2 -> "-"
+    | 3 | -1 -> "/"
+    | _ -> assert false
+
+let update_monitor =
+  let c = ref 0 in
+  fun t s r ->
+  reset_gc ();
+  incr c;
+  let r =
+    if r=0 then "0" else
+      (string_of_int r) ^ " " ^ (fan (!c / 4))
+  in
+  monitor#set_text ((string_of_int t) ^ "/" ^ (string_of_int s) ^ "/" ^ r)
+
 (****************************)
 (* command entry completion *)
 (****************************)
@@ -333,6 +364,12 @@ end
 
 module C = Controller_itp.Make(S)
 
+let () =
+  let n = gconfig.session_nb_processes in
+  Debug.dprintf debug "[IDE] setting max proof tasks to %d@." n;
+  C.set_max_tasks n;
+  C.register_observer update_monitor
+
 let (_ : GtkSignal.id) =
   replay_menu_item#connect#activate
     ~callback:(fun () ->
@@ -512,8 +549,8 @@ let run_strategy_on_task s =
           C.run_strategy_on_goal cont id st ~callback_pa ~callback_tr ~callback
     | _ -> printf "Strategy '%s' not found@." s
      end
-  | _ -> ()
-
+  | _ -> (
+)
 
 let clear_command_entry () = command_entry#set_text ""
 

src/session/controller_itp.ml

@@ -198,11 +198,6 @@ let print_session fmt c =
 
 
 
-module type Scheduler = sig
-  val timeout: ms:int -> (unit -> bool) -> unit
-  val idle: prio:int -> (unit -> bool) -> unit
-end
-
 let read_file env ?format fn =
   let theories = Env.read_file Env.base_language env ?format fn in
   let ltheories =
@@ -251,6 +246,14 @@ let add_file c ?format fname =
   let theories = read_file c.controller_env ?format fname in
   add_file_section ~use_shapes:false c.controller_session fname theories format
 
+
+
+module type Scheduler = sig
+  val timeout: ms:int -> (unit -> bool) -> unit
+  val idle: prio:int -> (unit -> bool) -> unit
+end
+
+
 module Make(S : Scheduler) = struct
 
 let scheduled_proof_attempts = Queue.create ()
@@ -261,8 +264,17 @@ let timeout_handler_running = ref false
 
 let max_number_of_running_provers = ref 1
 
+let set_max_tasks n =
+  max_number_of_running_provers := n;
+  Prove_client.set_max_running_provers n
+
+
 let number_of_running_provers = ref 0
 
+let observer = ref (fun _ _ _ -> ())
+
+let register_observer = (:=) observer
+
 module Hprover = Whyconf.Hprover
 
 (*
@@ -321,20 +333,26 @@ let timeout_handler () =
   (* if the number of prover tasks is less than 3 times the maximum
      number of running provers, then we heuristically decide to add
      more tasks *)
-  try
-    for _i = Queue.length prover_tasks_in_progress
-        to 3 * !max_number_of_running_provers do
-      let (c,id,pr,limit,callback) = Queue.pop scheduled_proof_attempts in
-      try
-        build_prover_call c id pr limit callback
-      with e when not (Debug.test_flag Debug.stack_trace) ->
-        Format.eprintf
-          "@[Exception raised in Controller_itp.build_prover_call:@ %a@.@]"
-          Exn_printer.exn_printer e;
-        callback (InternalFailure e)
-    done;
-    true
-  with Queue.Empty -> true
+  begin
+    try
+      for _i = Queue.length prover_tasks_in_progress
+          to 3 * !max_number_of_running_provers do
+        let (c,id,pr,limit,callback) = Queue.pop scheduled_proof_attempts in
+        try
+          build_prover_call c id pr limit callback
+        with e when not (Debug.test_flag Debug.stack_trace) ->
+          Format.eprintf
+            "@[Exception raised in Controller_itp.build_prover_call:@ %a@.@]"
+            Exn_printer.exn_printer e;
+          callback (InternalFailure e)
+      done
+  with Queue.Empty -> ()
+  end;
+  let scheduled = Queue.length scheduled_proof_attempts in
+  let waiting_or_running = Queue.length prover_tasks_in_progress in
+  let running = !number_of_running_provers in
+  !observer scheduled (waiting_or_running - running) running;
+  true
 
 let run_timeout_handler () =
   if not !timeout_handler_running then

src/session/controller_itp.mli

@@ -145,6 +145,15 @@ val add_file : controller -> ?format:Env.fformat -> string -> unit
 
 module Make(S : Scheduler) : sig
 
+val set_max_tasks : int -> unit
+(** sets the maximum number of proof tasks that can be running at the
+    same time. Initially set to 1. *)
+
+val register_observer : (int -> int -> int -> unit) -> unit
+(** records a hook that will be called with the number of waiting
+    tasks, scheduled tasks, and running taks, each time these numbers
+    change *)
+
 val schedule_proof_attempt :
   controller ->
   proofNodeID ->