ITP: simple attempt to implement 'interrupt'. IMPORTANT ISSUE: running processes are not killed

src/ide/why3ide.ml

@@ -686,7 +686,7 @@ let image_of_pa_status ~obsolete pa =
   match pa with
   | Controller_itp.Unedited -> !image_scheduled (* TODO !image_unedited *)
   | Controller_itp.JustEdited -> !image_scheduled (* TODO !image_edited *)
-  | Controller_itp.Interrupted -> !image_scheduled (* TODO !image_interrrupted *)
+  | Controller_itp.Interrupted -> !image_undone
   | Controller_itp.Scheduled -> !image_scheduled
   | Controller_itp.Running -> !image_running
   | Controller_itp.InternalFailure _e -> !image_failure

src/session/controller_itp.ml

@@ -506,6 +506,20 @@ let timeout_handler () =
   !observer scheduled (waiting_or_running - running) running;
   true
 
+let interrupt () =
+  while not (Queue.is_empty prover_tasks_in_progress) do
+    let (_ses,_id,_pr,callback,_started,_call) =
+      Queue.pop prover_tasks_in_progress in
+    (* TODO: apply some Call_provers.interrupt_call call *)
+    callback Interrupted
+  done;
+  number_of_running_provers := 0;
+  while not (Queue.is_empty scheduled_proof_attempts) do
+    let (_c,_id,_pr,_limit,callback) = Queue.pop scheduled_proof_attempts in
+    callback Interrupted
+  done;
+  !observer 0 0 0
+
 let run_timeout_handler () =
   if not !timeout_handler_running then
     begin
@@ -593,7 +607,8 @@ let run_strategy_on_goal
            | Done { Call_provers.pr_answer = Call_provers.Valid } ->
               (* proof succeeded, nothing more to do *)
               callback STShalt
-           | Interrupted | InternalFailure _
+           | Interrupted | InternalFailure _ ->
+              callback STShalt
            | Done _ ->
               (* proof did not succeed, goto to next step *)
               callback (STSgoto (g,pc+1));

src/session/controller_itp.mli

@@ -159,6 +159,10 @@ val register_observer : (int -> int -> int -> unit) -> unit
     tasks, scheduled tasks, and running taks, each time these numbers
     change *)
 
+val interrupt : unit -> unit
+(** discards all scheduled proof attempts or transformations, including
+    the one already running *)
+
 val schedule_proof_attempt :
   controller ->
   proofNodeID ->

src/session/itp_communication.ml

@@ -96,3 +96,4 @@ type ide_request =
   | Reload_req
   | Replay_req
   | Exit_req
+  | Interrupt_req

src/session/itp_communication.mli

@@ -103,3 +103,4 @@ type ide_request =
   | Reload_req
   | Replay_req
   | Exit_req
+  | Interrupt_req

src/session/itp_server.ml

@@ -294,6 +294,7 @@ let print_request fmt r =
   | Reload_req                      -> fprintf fmt "reload"
   | Replay_req                      -> fprintf fmt "replay"
   | Exit_req                        -> fprintf fmt "exit"
+  | Interrupt_req                   -> fprintf fmt "interrupt"
 
 let print_msg fmt m =
   match m with
@@ -1020,6 +1021,7 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
         save_file name text;
     | Get_task nid                 -> send_task nid
     | Replay_req                   -> replay_session (); resend_the_tree ()
+    | Interrupt_req                -> C.interrupt ()
     | Command_req (nid, cmd)       ->
       begin
         let snid = get_proof_node_id nid in
@@ -1028,6 +1030,7 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
         | Query s                 -> P.notify (Message (Query_Info (nid, s)))
         | Prove (p, limit)        -> schedule_proof_attempt nid p limit
         | Strategies st           -> run_strategy_on_task nid st
+        | Interrupt               -> C.interrupt ()
         | Help_message s          -> P.notify (Message (Help s))
         | QError s                -> P.notify (Message (Query_Error (nid, s)))
         | Other (s, _args)        ->

src/session/json_util.ml

@@ -129,6 +129,7 @@ let convert_request_constructor (r: ide_request) =
   | Reload_req                -> String "Reload_req"
   | Replay_req                -> String "Replay_req"
   | Exit_req                  -> String "Exit_req"
+  | Interrupt_req             -> String "Interrupt_req"
 
 let print_request_to_json (r: ide_request): Json_base.value =
   let cc = convert_request_constructor in
@@ -192,6 +193,8 @@ let print_request_to_json (r: ide_request): Json_base.value =
       Obj ["ide_request", cc r]
   | Exit_req ->
       Obj ["ide_request", cc r]
+  | Interrupt_req ->
+      Obj ["ide_request", cc r]
 
 let convert_constructor_message (m: message_notification) =
   match m with

src/session/server_utils.ml

@@ -232,6 +232,7 @@ type command =
   | Transform    of string * Trans.gentrans * string list
   | Prove        of Whyconf.config_prover * Call_provers.resource_limit
   | Strategies   of string
+  | Interrupt
   | Help_message of string
   | Query        of string
   | QError       of string
@@ -250,6 +251,7 @@ let interp_others commands config cmd args =
             | _ -> "1"
           in
           Strategies s
+      | "interrupt" -> Interrupt
       | "help" ->
           let text = Pp.sprintf
                           "Please type a command among the following (automatic completion available)@\n\

src/session/server_utils.mli

@@ -43,6 +43,7 @@ type command =
   | Transform    of string * Trans.gentrans * string list
   | Prove        of Whyconf.config_prover * Call_provers.resource_limit
   | Strategies   of string
+  | Interrupt
   | Help_message of string
   | Query        of string
   | QError       of string