proofs monitoring and cancellation

doc/manpages.tex

@@ -293,6 +293,9 @@ the actions of the various menus and buttons of the interface.
 \item[Clean] Removes any unsuccessful proof attempt for which there is
   another successful proof attempt for the same goal
 
+\item[Interrupt] Cancels all the proof attempts currently scheduled
+  but not yet started.
+
 \end{description}
 
 \subsection{Menus}

src/ide/gmain.ml

@@ -229,6 +229,23 @@ let cleaning_box =
   GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
   ~packing:cleaning_frame#add ()
 
+let monitor_frame =
+  GBin.frame ~label:"Monitor"
+    ~packing:(tools_window_vbox#pack ~expand:false) ()
+
+let monitor_box =
+  GPack.vbox ~homogeneous:false ~packing:monitor_frame#add ()
+
+let monitor_waiting =
+  GMisc.label ~text:"  Waiting: 0" ~packing:monitor_box#add ()
+
+let monitor_scheduled =
+  GMisc.label ~text:"Scheduled: 0" ~packing:monitor_box#add ()
+
+let monitor_running =
+  GMisc.label ~text:"  Running: 0" ~packing:monitor_box#add ()
+
+
 
 (* horizontal paned *)
 
@@ -318,6 +335,7 @@ let image_of_result ~obsolete result =
     | Session.Undone -> !image_undone
     | Session.Scheduled -> !image_scheduled
     | Session.Running -> !image_running
+    | Session.Interrupted -> assert false
     | Session.InternalFailure _ -> !image_failure
     | Session.Done r -> match r.Call_provers.pr_answer with
         | Call_provers.Valid ->
@@ -361,6 +379,11 @@ module M = Session.Make
        let (_ : GMain.Timeout.id) = GMain.Timeout.add ~ms ~callback:f in
        ()
 
+     let notify_timer_state t s r =
+       monitor_waiting#set_text ("Waiting: " ^ (string_of_int t));
+       monitor_scheduled#set_text ("Scheduled: " ^ (string_of_int s));
+       monitor_running#set_text ("Running: " ^ (string_of_int r));
+
    end)
 
 let set_row_status row b =
@@ -1377,16 +1400,6 @@ let () =
     b#connect#pressed ~callback:replay_obsolete_proofs
   in ()
 
-(*
-let () =
-  let b = GButton.button ~packing:tools_box#add ~label:"Cancel" () in
-  b#misc#set_tooltip_markup "Mark all proofs below the current selection as <b>obsolete</b>";
-  let i = GMisc.image ~pixbuf:(!image_cancel) () in
-  let () = b#set_image i#coerce in
-  let (_ : GtkSignal.id) =
-    b#connect#pressed ~callback:cancel_proofs
-  in ()
-*)
 
 (*************)
 (* removing  *)
@@ -1477,6 +1490,15 @@ let () =
     b#connect#pressed ~callback:clean_selection
   in ()
 
+let () =
+  let b = GButton.button ~packing:monitor_box#add ~label:"Interrupt" () in
+  b#misc#set_tooltip_markup "Cancels all scheduled proof attempts";
+  let i = GMisc.image ~pixbuf:(!image_cancel) () in
+  let () = b#set_image i#coerce in
+  let (_ : GtkSignal.id) =
+    b#connect#pressed ~callback:M.cancel_scheduled_proofs 
+  in ()
+
 
 (***************)
 (* Bind events *)
@@ -1514,6 +1536,7 @@ let select_row r =
             | Session.Done r -> r.Call_provers.pr_output
             | Session.Scheduled-> "proof scheduled by not running yet"
             | Session.Running -> "prover currently running"
+            | Session.Interrupted -> assert false
             | Session.InternalFailure e ->
               let b = Buffer.create 37 in
               bprintf b "%a" Exn_printer.exn_printer e;

src/ide/replay.ml

@@ -119,6 +119,8 @@ module M = Session.Make
          | None -> timeout_handler := Some(float ms /. 1000.0 ,f);
          | Some _ -> failwith "Replay.timeout: already one handler installed"
 
+     let notify_timer_state _ _ _ = ()
+
    end)
 
 

src/ide/session.ml

@@ -96,6 +96,7 @@ let lookup_transformation env =
 type proof_attempt_status =
   | Undone
   | Scheduled (** external proof attempt is scheduled *)
+  | Interrupted
   | Running (** external proof attempt is in progress *)
   | Done of Call_provers.prover_result (** external proof done *)
   | InternalFailure of exn (** external proof aborted by internal error *)
@@ -113,6 +114,9 @@ module type OBSERVER = sig
 
   val timeout: ms:int -> (unit -> bool) -> unit
   val idle: (unit -> bool) -> unit
+
+  val notify_timer_state : int -> int -> int -> unit
+
 end
 
 module Make(O : OBSERVER) = struct
@@ -277,7 +281,7 @@ let save_result fmt r =
 
 let save_status fmt s =
   match s with
-    | Undone | Scheduled | Running ->
+    | Undone | Scheduled | Running | Interrupted ->
         fprintf fmt "<undone/>@\n"
     | InternalFailure msg ->
         fprintf fmt "<internalfailure reason=\"%s\"/>@\n"
@@ -390,6 +394,13 @@ let set_proof_state ~obsolete a res =
 (*************************)
 
 
+type action =
+  | Action_proof_attempt of bool * int * int * in_channel option * string * Driver.driver *
+    (proof_attempt_status -> unit) * Task.task
+  | Action_delayed of (unit -> unit)
+
+let actions_queue = Queue.create ()
+
 (* timeout handler *)
 
 type timeout_action =
@@ -436,24 +447,26 @@ let timeout_handler () =
   let continue =
     match l with
       | [] ->
-(*
+(**)
           eprintf "Info: timeout_handler stopped@.";
-*)
+(**)
           false
       | _ -> true
   in
+  O.notify_timer_state
+    (Queue.length actions_queue)
+    (Queue.length proof_attempts_queue) (List.length l);
   timeout_handler_activated := continue;
   timeout_handler_running := false;
   continue
 
-
 let run_timeout_handler () =
   if !timeout_handler_activated then () else
     begin
       timeout_handler_activated := true;
-(*
+(**)
       eprintf "Info: timeout_handler started@.";
-*)
+(**)
       O.timeout ~ms:100 timeout_handler
     end
 
@@ -464,13 +477,6 @@ let schedule_any_timeout callback =
 (* idle handler *)
 
 
-type action =
-  | Action_proof_attempt of bool * int * int * in_channel option * string * Driver.driver *
-    (proof_attempt_status -> unit) * Task.task
-  | Action_delayed of (unit -> unit)
-
-let actions_queue = Queue.create ()
-
 let idle_handler_activated = ref false
 
 let idle_handler () =
@@ -500,9 +506,9 @@ let idle_handler () =
     true
   with Queue.Empty ->
     idle_handler_activated := false;
-(*
+(**)
     eprintf "Info: idle_handler stopped@.";
-*)
+(**)
     false
     | e ->
       Format.eprintf "@[Exception raise in Session.idle_handler:@ %a@.@]"
@@ -515,16 +521,41 @@ let run_idle_handler () =
   if !idle_handler_activated then () else
     begin
       idle_handler_activated := true;
-(*
+(**)
       eprintf "Info: idle_handler started@.";
-*)
+(**)
       O.idle idle_handler
     end
 
 (* main scheduling functions *)
 
+let cancel_scheduled_proofs () =
+  let new_queue = Queue.create () in
+  try
+    while true do
+      match Queue.pop actions_queue with
+        | Action_proof_attempt(_debug,_timelimit,_memlimit,_old,_command,
+                               _driver,callback,_goal) ->
+            callback Interrupted
+        | Action_delayed _ as a->
+            Queue.push a new_queue
+    done
+  with Queue.Empty ->
+    Queue.transfer new_queue actions_queue;
+    try
+      while true do
+        let (callback,_) = Queue.pop proof_attempts_queue in
+        callback Interrupted
+      done
+    with
+      | Queue.Empty -> ()
+
+
 let schedule_proof_attempt ~debug ~timelimit ~memlimit ?old
     ~command ~driver ~callback goal =
+(**)
+  eprintf "Scheduling a new proof attempt@.";
+(**)
   Queue.push
     (Action_proof_attempt(debug,timelimit,memlimit,old,command,driver,
                         callback,goal))
@@ -1484,8 +1515,9 @@ let save_session () =
 
 let redo_external_proof ~timelimit g a =
   (* check that the state is not Scheduled or Running *)
-  let running = match a.proof_state with
-    | Scheduled | Running -> true
+  let previous_result,previous_obs = a.proof_state,a.proof_obsolete in
+  let running = match previous_result with
+    | Scheduled | Running | Interrupted -> true
     | Done _ | Undone | InternalFailure _ -> false
   in
   if running then ()
@@ -1495,6 +1527,10 @@ let redo_external_proof ~timelimit g a =
       | Undetected_prover _ -> ()
       | Detected_prover p ->
           let callback result =
+            match result with
+              | Interrupted ->
+                  set_proof_state ~obsolete:previous_obs a previous_result
+              | _ ->
                   set_proof_state ~obsolete:false a result;
           in
           let old = if a.edited_as = "" then None else
@@ -1660,7 +1696,7 @@ let same_result r1 r2 =
 let check_external_proof g a =
   (* check that the state is not Scheduled or Running *)
   let running = match a.proof_state with
-    | Scheduled | Running -> true
+    | Scheduled | Running | Interrupted -> true
     | Done _ | Undone | InternalFailure _ -> false
   in
   if running then ()
@@ -1676,7 +1712,7 @@ let check_external_proof g a =
             let p_name = p.prover_name ^ " " ^ p.prover_version in
             let callback result =
               match result with
-                | Scheduled | Running -> ()
+                | Scheduled | Running | Interrupted -> ()
                 | Undone -> assert false
                 | InternalFailure msg ->
                     push_report g p_name (CallFailed msg);
@@ -1849,7 +1885,7 @@ let ft_of_pa a =
 let edit_proof ~default_editor ~project_dir a =
   (* check that the state is not Scheduled or Running *)
   let running = match a.proof_state with
-    | Scheduled | Running -> true
+    | Scheduled | Running | Interrupted -> true
     | Undone | Done _ | InternalFailure _ -> false
   in
   if running then ()

src/ide/session.mli

@@ -57,6 +57,7 @@ val lookup_transformation : Env.env -> string -> transformation_data
 type proof_attempt_status = private
     | Undone
     | Scheduled (** external proof attempt is scheduled *)
+    | Interrupted
     | Running (** external proof attempt is in progress *)
     | Done of Call_provers.prover_result (** external proof done *)
     | InternalFailure of exn (** external proof aborted by internal error *)
@@ -89,6 +90,11 @@ module type OBSERVER = sig
         there is nothing else to do. When the given function returns
         true, it must be rescheduled *)
 
+  val notify_timer_state : int -> int -> int -> unit
+    (** this function is called when timer state changes.
+        The first arg is the number of tasks waiting.
+        The second arg is the number of scheduled proof tasks.
+        The third arg is the number of running proof tasks *)
 end
 
 (** {2 Main functor} *)
@@ -228,7 +234,16 @@ module Make(O: OBSERVER) : sig
 
   val run_prover : context_unproved_goals_only:bool ->
     timelimit:int -> prover_data -> any -> unit
-    (** [run_prover p a] runs prover [p] on all goals under [a] *)
+    (** [run_prover p a] runs prover [p] on all goals under [a]
+        the proof attempts are only scheduled for running, and they
+        will be started asynchronously when processors are available
+    *)
+
+  val cancel_scheduled_proofs : unit -> unit
+    (** cancels all currently scheduled proof attempts.
+        note that the already running proof attempts are not
+        stopped, the corresponding processes must terminate
+        by their own. *)
 
   val transform : context_unproved_goals_only:bool ->
     transformation_data -> any -> unit