Commit b62a67fb authored by Sylvain Dailler's avatar Sylvain Dailler

Moved print_request in itp_server. needed to print an error.

Removed duplicated code.
Handling of unrecoverable exception in treat_request so that server dont
get stuck.
parent 57ac46f7
......@@ -19,19 +19,7 @@ module Protocol_why3ide = struct
let print_request_debug r =
Debug.dprintf debug_proto "[request]";
match r with
| Command_req s -> Debug.dprintf debug_proto "command \"%s\"" s
| Prove_req (prover, _rl) -> Debug.dprintf debug_proto "prove with %s" prover
| Transform_req (tr, _args) -> Debug.dprintf debug_proto "transformation :%s" tr
| Strategy_req st -> Debug.dprintf debug_proto "strategy %s" st
| Open_req f -> Debug.dprintf debug_proto "open file %s" f
| Set_max_tasks_req i -> Debug.dprintf debug_proto "set max tasks %i" i
| Get_task -> Debug.dprintf debug_proto "get task"
| Get_Session_Tree_req -> Debug.dprintf debug_proto "get session tree"
| Save_req -> Debug.dprintf debug_proto "save"
| Reload_req -> Debug.dprintf debug_proto "reload"
| Replay_req -> Debug.dprintf debug_proto "replay"
| Exit_req -> Debug.dprintf debug_proto "exit"
Debug.dprintf debug_proto "%a" print_request r
let print_msg_debug m = match m with
| Proof_error (_ids, s) -> Debug.dprintf debug_proto "proof error %s" s
......@@ -43,6 +31,7 @@ module Protocol_why3ide = struct
| Help _s -> Debug.dprintf debug_proto "help"
| Information s -> Debug.dprintf debug_proto "info %s" s
| Task_Monitor _ -> Debug.dprintf debug_proto "task montor"
| Error s -> Debug.dprintf debug_proto "%s" s
let print_notify_debug n =
Debug.dprintf debug_proto "[notification]";
......@@ -764,15 +753,21 @@ let add_to_msg_zone s =
let treat_message_notification msg = match msg with
(* TODO: do something ! *)
| Proof_error (_id, s) -> add_to_msg_zone s
| Transf_error (_id, s) -> add_to_msg_zone s
| Strat_error (_id, s) -> add_to_msg_zone s
| Proof_error (_id, s) -> add_to_msg_zone s
| Transf_error (_id, s) -> add_to_msg_zone s
| Strat_error (_id, s) -> add_to_msg_zone s
| Replay_Info s -> add_to_msg_zone s
| Query_Info (_id, s) -> add_to_msg_zone s
| Query_Error (_id, s) -> add_to_msg_zone s
| Query_Info (_id, s) -> add_to_msg_zone s
| Query_Error (_id, s) -> add_to_msg_zone s
| Help s -> add_to_msg_zone s
| Information s -> add_to_msg_zone s
| Task_Monitor (t, s, r) -> update_monitor t s r
(* TODO do not print it *)
| Error s ->
if Debug.test_flag debug then
add_to_msg_zone s
else
add_to_msg_zone "Request failed."
let treat_notification n = match n with
| Node_change (id, info) ->
......
......@@ -232,13 +232,6 @@ module P = Print_tree.PMake(PSession)
let print_session fmt c =
P.print fmt { PSession.tcont = c; PSession.tkind = PSession.Session }
(*********)
......
open Call_provers
open Format
(* Information that the IDE may want to have *)
type prover = string
......@@ -47,6 +48,7 @@ type message_notification =
| Help of string
| Information of string
| Task_Monitor of int * int * int
| Error of string
type notification =
| Node_change of node_ID * node_info
......@@ -73,6 +75,21 @@ type request_type =
| Replay_req
| Exit_req
let print_request fmt r =
match r with
| Command_req s -> fprintf fmt "command \"%s\"" s
| Prove_req (prover, _rl) -> fprintf fmt "prove with %s" prover
| Transform_req (tr, _args) -> fprintf fmt "transformation :%s" tr
| Strategy_req st -> fprintf fmt "strategy %s" st
| Open_req f -> fprintf fmt "open file %s" f
| Set_max_tasks_req i -> fprintf fmt "set max tasks %i" i
| Get_task -> fprintf fmt "get task"
| Get_Session_Tree_req -> fprintf fmt "get session tree"
| Save_req -> fprintf fmt "save"
| Reload_req -> fprintf fmt "reload"
| Replay_req -> fprintf fmt "replay"
| Exit_req -> fprintf fmt "exit"
type ide_request = request_type * node_ID
open Session_itp
......@@ -96,7 +113,7 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
(************************)
let files = Queue.create ()
let opt_parser = ref None
(* TODO never used let _opt_parser = ref None *)
(* Files are passed with request Open *)
let config, base_config, env =
......@@ -491,7 +508,9 @@ exception Bad_prover_name of prover
(* ----------------- treat_request -------------------- *)
let rec treat_request (r,nid) = match r with
let rec treat_request (r,nid) =
try (
match r with
| Prove_req (p,limit) -> schedule_proof_attempt nid (get_prover p) limit
| Transform_req (t, args) -> apply_transform nid t args
| Strategy_req st -> run_strategy_on_task nid st
......@@ -528,7 +547,11 @@ exception Bad_prover_name of prover
end
| Set_max_tasks_req i -> C.set_max_tasks i
| Exit_req -> exit 0 (* TODO *)
)
with e -> P.notify (Message (Error (Pp.string_of
(fun fmt (r,nid,e) -> Format.fprintf fmt
"There was an unrecoverable error during treatment of request:\n %a\non node: %d\nwith exception: %a"
print_request (Obj.magic r) nid Exn_printer.exn_printer e ) (r, nid, e))))
let treat_requests () : bool =
List.iter treat_request (P.get_requests ());
......
......@@ -44,8 +44,12 @@ type message_notification =
| Query_Info of node_ID * string
| Query_Error of node_ID * string
| Help of string
(* General information *)
| Information of string
(* Number of task scheduled, running, etc *)
| Task_Monitor of int * int * int
(* An error happened that could not be identified in server *)
| Error of string
type notification =
| Node_change of node_ID * node_info
......@@ -82,6 +86,8 @@ type request_type =
| Replay_req
| Exit_req
val print_request: Format.formatter -> request_type -> unit
(* TODO: change to request_type * node_ID list ? *)
type ide_request = request_type * node_ID
......
......@@ -450,57 +450,6 @@ Strategies
(********* Callbacks tools *******)
(* Return the prover corresponding to given name. name is of the form
| name
| name, version
| name, altern
| name, version, altern *)
let return_prover name config =
let fp = Whyconf.parse_filter_prover name in
(** all provers that have the name/version/altern name *)
let provers = Whyconf.filter_provers config fp in
if Whyconf.Mprover.is_empty provers then begin
(*Format.eprintf "Prover corresponding to %s has not been found@." name;*)
None
end else
Some (snd (Whyconf.Mprover.choose provers))
(* Parses the Other command. If it fails to parse it, it answers None otherwise
it returns the config of the prover together with the ressource_limit *)
let parse_prover_name config name args :
(Whyconf.config_prover * Call_provers.resource_limit) option =
let main = Whyconf.get_main config in
match (return_prover name config) with
| None -> None
| Some prover_config ->
begin
if (List.length args > 2) then None else
match args with
| [] ->
let default_limit = Call_provers.{limit_time = Whyconf.timelimit main;
limit_mem = Whyconf.memlimit main;
limit_steps = 0} in
Some (prover_config, default_limit)
| [timeout] -> Some (prover_config,
Call_provers.{empty_limit with
limit_time = int_of_string timeout})
| [timeout; oom ] ->
Some (prover_config, Call_provers.{limit_time = int_of_string timeout;
limit_mem = int_of_string oom;
limit_steps = 0})
| _ -> (*Format.eprintf "Parse_prover_name. Should not happen. Please report@."; *) None
end
(********************)
(* Terminal history *)
(********************)
......
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