Commit f04a5a8c authored by MARCHE Claude's avatar MARCHE Claude

delayed initialization of ITP server

parent 3c425b07
......@@ -251,6 +251,7 @@ val set_family : config -> string -> Rc.family -> config
(** Common command line options *)
module Args : sig
val initialize :
?extra_help : (Format.formatter -> unit -> unit) ->
(string * Arg.spec * string) list ->
......@@ -265,4 +266,5 @@ module Args : sig
(string -> unit) -> string -> unit
val exit_with_usage : (string * Arg.spec * string) list -> string -> 'a
end
......@@ -77,8 +77,6 @@ module S = struct
()
end
module Server = Itp_server.Make (S) (Protocol_why3ide)
(************************)
(* parsing command line *)
(************************)
......@@ -104,8 +102,9 @@ let usage_str = sprintf
(Filename.basename Sys.argv.(0))
let gconfig = try
let config,base_config = Server.get_configs () in
Whyconf.Args.parse spec (fun f -> Queue.add f files) usage_str;
= Server.get_configs () in
let config,base_config, env =
Whyconf.Args.initialize spec (fun f -> Queue.add f files) usage_str;
if Queue.is_empty files then
Whyconf.Args.exit_with_usage spec usage_str;
Gconfig.load_config config base_config;
......@@ -115,6 +114,10 @@ let gconfig = try
eprintf "%a@." Exn_printer.exn_printer e;
exit 1
module Server = Itp_server.Make (S) (Protocol_why3ide)
let () = Server.init_controller config base_config env
let () =
Debug.dprintf debug "[GUI] Init the GTK interface...@?";
ignore (GtkMain.Main.init ());
......
......@@ -33,29 +33,29 @@ let interp_request args =
let print_message_notification fmt n =
match n with
| Error s -> ()
| Open_File_Error s -> ()
| Proof_error(nid,s) -> ()
| Transf_error(nid,s) -> ()
| Strat_error(nid,s) -> ()
| Replay_Info(s) -> ()
| Error _s -> ()
| Open_File_Error _s -> ()
| Proof_error(_nid,_s) -> ()
| Transf_error(_nid,_s) -> ()
| Strat_error(_nid,_s) -> ()
| Replay_Info(_s) -> ()
| Query_Info(nid,s) -> fprintf fmt "kind=\"query_info\", node=\"%d\", text=\"%s\"" nid s
| Query_Error(nid,s) -> fprintf fmt "kind=\"query_error\", node=\"%d\", text=\"%s\"" nid s
| Help s -> fprintf fmt "kind=\"help\", text=\"%s\"" s
| Information s -> fprintf fmt "kind=\"information\", text=\"%s\"" s
| Task_Monitor(a,b,c) -> ()
| Task_Monitor(_a,_b,_c) -> ()
let print_notification fmt n =
match n with
| Node_change(nid,info) -> ()
| New_node(nid,nid',nodetype,info) -> ()
| Remove(nid) -> ()
| Initialized(ginfo) -> ()
| Node_change(_nid,_info) -> ()
| New_node(_nid,_nid',_nodetype,_info) -> ()
| Remove(_nid) -> ()
| Initialized(_ginfo) -> ()
| Saved -> ()
| Message n -> fprintf fmt "{ notification=\"message=\"; %a }"
print_message_notification n
| Dead s -> ()
| Task(nid,task) -> ()
| Dead _s -> ()
| Task(_nid,_task) -> ()
let handle_script s args =
match s with
......
......@@ -76,32 +76,13 @@ let clear_proof_state c =
Htn.clear c.proof_state.tn_state;
Hpn.clear c.proof_state.pn_state
exception LoadDriverFailure of Whyconf.config_prover * exn
let create_controller env provers =
let c = {
let create_controller env =
{
controller_session = Session_itp.dummy_session;
proof_state = init_proof_state ();
controller_env = env;
controller_provers = Whyconf.Hprover.create 7;
}
in
(* load provers drivers *)
Whyconf.Mprover.iter
(fun _ p ->
try
let d = Driver.load_driver env p.Whyconf.driver [] in
Whyconf.Hprover.add c.controller_provers p.Whyconf.prover (p,d)
with e -> raise (LoadDriverFailure(p,e))
(*
let p = p.Whyconf.prover in
eprintf "Failed to load driver for %s %s: %a@."
p.Whyconf.prover_name p.Whyconf.prover_version
Exn_printer.exn_printer e
*)
)
provers;
c
}
let init_controller s c =
clear_proof_state (c);
......
......@@ -78,10 +78,8 @@ type controller = private
controller_provers : (Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
}
exception LoadDriverFailure of Whyconf.config_prover * exn
val create_controller:
Env.env -> Whyconf.config_prover Whyconf.Mprover.t -> controller
(** creates a controller with an empty session *)
val create_controller: Env.env -> controller
(** creates a controller with no prover and an empty session *)
val init_controller: Session_itp.session -> controller -> unit
(** adds a session to a controller *)
......
......@@ -431,18 +431,23 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
let debug = Debug.register_flag "itp_server" ~desc:"ITP server"
(************************)
(* parsing command line *)
(************************)
type server_data =
{ config : Whyconf.config;
task_driver : Driver.driver;
provers : Whyconf.config_prover Whyconf.Mprover.t;
cont : Controller_itp.controller;
}
(* Files are passed with request Open *)
let config, base_config, env =
let c, b, e = Whyconf.Args.init () in
c, b, e
let server_data = ref None
let get_configs () = config, base_config
let d () =
match !server_data with
| None ->
Format.eprintf "[ITP server] not yet initialized@.";
exit 1
| Some x -> x
let task_driver =
let task_driver config env =
try
let main = Whyconf.get_main config in
let d = Filename.concat (Whyconf.datadir main)
......@@ -452,58 +457,66 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
Debug.dprintf debug "[ITP server] driver for task printing loaded@.";
d
with e ->
Format.eprintf "Fatal error while loading itp driver: %a@." Exn_printer.exn_printer e;
exit 1
let provers : Whyconf.config_prover Whyconf.Mprover.t =
Whyconf.get_provers config
Format.eprintf "Fatal error while loading itp driver: %a@." Exn_printer.exn_printer e;
exit 1
let get_prover_list (config: Whyconf.config) =
Mstr.fold (fun x _ acc -> x :: acc) (Whyconf.get_prover_shortcuts config) []
let prover_list: prover list = get_prover_list config
let transformation_list: transformation list =
List.map fst (list_transforms ())
let strategies_list: strategy list =
let l = strategies env config loaded_strategies in
List.map (fun (a,_,_,_) -> a) l
let infos =
{
provers = prover_list;
transformations = transformation_list;
strategies = strategies_list;
commands =
List.map (fun (c,_,_) -> c) commands
}
(* Create_controller creates a dummy controller *)
let cont =
try
create_controller env provers
with LoadDriverFailure (p,e') as e ->
P.notify (Message (Error "To implement: could not load driver"));
Format.eprintf "[ITP server] error loading driver for prover %a: %a@."
Whyconf.print_prover p.Whyconf.prover
Exn_printer.exn_printer e';
raise e (* TODO *)
let init_server config env =
let provers = Whyconf.get_provers config in
let c = create_controller env in
let task_driver = task_driver config env in
Whyconf.Mprover.iter
(fun _ p ->
try
let d = Driver.load_driver c.controller_env p.Whyconf.driver [] in
Whyconf.Hprover.add c.controller_provers p.Whyconf.prover (p,d)
with e ->
Format.eprintf
"[ITP server] error loading driver for prover %a: %a@."
Whyconf.print_prover p.Whyconf.prover
Exn_printer.exn_printer e)
provers;
server_data := Some
{ config = config;
task_driver = task_driver;
provers = provers;
cont = c }
(* ------------ init controller ------------ *)
(* Init cont on file or directory. It is called only when an
Open_session_req is requested *)
let init_cont f =
let d = d () in
let prover_list = get_prover_list d.config in
let transformation_list = List.map fst (list_transforms ()) in
let strategies_list =
let l = strategies d.cont.controller_env d.config loaded_strategies in
List.map (fun (a,_,_,_) -> a) l
in
let infos =
{
provers = prover_list;
transformations = transformation_list;
strategies = strategies_list;
commands =
List.map (fun (c,_,_) -> c) commands
}
in
try (
if (Sys.file_exists f) then
begin
if (Sys.is_directory f) then
begin
cont_from_session_dir cont f;
cont_from_session_dir d.cont f;
P.notify (Initialized infos)
end
else
begin
cont_from_file cont f;
cont_from_file d.cont f;
P.notify (Initialized infos)
end
end
......@@ -530,17 +543,18 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
| APa _ -> NProofAttempt
let get_node_name (node: any) =
let d = d () in
match node with
| AFile file ->
file.file_name
| ATh th ->
(theory_name th).Ident.id_string
| ATn tn ->
get_transf_name cont.controller_session tn
get_transf_name d.cont.controller_session tn
| APn pn ->
(get_proof_name cont.controller_session pn).Ident.id_string
(get_proof_name d.cont.controller_session pn).Ident.id_string
| APa pa ->
let pa = get_proof_attempt_node cont.controller_session pa in
let pa = get_proof_attempt_node d.cont.controller_session pa in
Pp.string_of Whyconf.print_prover pa.prover
(*
......@@ -617,7 +631,8 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
let get_prover p =
match return_prover p config with
let d = d () in
match return_prover p d.config with
| None -> raise (Bad_prover_name p)
| Some c -> c
......@@ -650,9 +665,10 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
node_ID -> any -> unit *)
let iter_subtree_proof_attempt_from_goal
(f: parent:node_ID -> any -> unit) parent id =
let d = d () in
Whyconf.Hprover.iter
(fun _pa panid -> f ~parent (APa panid))
(get_proof_attempt_ids cont.controller_session id)
(get_proof_attempt_ids d.cont.controller_session id)
let rec iter_subtree_from_goal
(f: parent:node_ID -> any -> unit) parent id =
......
......@@ -105,7 +105,9 @@ end
module Make (S:Controller_itp.Scheduler) (P:Protocol) : sig
(*
val get_configs: unit -> Whyconf.config * Whyconf.config
*)
(* Nothing ! *)
......
open Format
open Stdlib
open Session_itp
exception NotADirectory of string
......
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