From a892b84a8ab5f6c6b772a475c3404f5d4f2455bb Mon Sep 17 00:00:00 2001 From: Claude Marche Date: Fri, 14 Apr 2017 17:21:46 +0200 Subject: [PATCH] ITP: simple attempt to implement 'interrupt'. IMPORTANT ISSUE: running processes are not killed --- src/ide/why3ide.ml | 2 +- src/session/controller_itp.ml | 17 ++++++++++++++++- src/session/controller_itp.mli | 4 ++++ src/session/itp_communication.ml | 1 + src/session/itp_communication.mli | 1 + src/session/itp_server.ml | 3 +++ src/session/json_util.ml | 3 +++ src/session/server_utils.ml | 2 ++ src/session/server_utils.mli | 1 + 9 files changed, 32 insertions(+), 2 deletions(-) diff --git a/src/ide/why3ide.ml b/src/ide/why3ide.ml index adada4b95..d0d23f5bd 100644 --- a/src/ide/why3ide.ml +++ b/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 diff --git a/src/session/controller_itp.ml b/src/session/controller_itp.ml index db84ad5d1..0e47a2e25 100644 --- a/src/session/controller_itp.ml +++ b/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)); diff --git a/src/session/controller_itp.mli b/src/session/controller_itp.mli index 475d9f03e..4d6b5c324 100644 --- a/src/session/controller_itp.mli +++ b/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 -> diff --git a/src/session/itp_communication.ml b/src/session/itp_communication.ml index aa497cdc7..1abd25f8b 100644 --- a/src/session/itp_communication.ml +++ b/src/session/itp_communication.ml @@ -96,3 +96,4 @@ type ide_request = | Reload_req | Replay_req | Exit_req + | Interrupt_req diff --git a/src/session/itp_communication.mli b/src/session/itp_communication.mli index 30ee29ffe..973682539 100644 --- a/src/session/itp_communication.mli +++ b/src/session/itp_communication.mli @@ -103,3 +103,4 @@ type ide_request = | Reload_req | Replay_req | Exit_req + | Interrupt_req diff --git a/src/session/itp_server.ml b/src/session/itp_server.ml index 197bb1c3d..a3737ae04 100644 --- a/src/session/itp_server.ml +++ b/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) -> diff --git a/src/session/json_util.ml b/src/session/json_util.ml index 96ff87e54..daaa1ebc9 100644 --- a/src/session/json_util.ml +++ b/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 diff --git a/src/session/server_utils.ml b/src/session/server_utils.ml index b6d33c57d..5bbba47c6 100644 --- a/src/session/server_utils.ml +++ b/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\ diff --git a/src/session/server_utils.mli b/src/session/server_utils.mli index 03aa204f0..373fe1281 100644 --- a/src/session/server_utils.mli +++ b/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 -- GitLab