Commit a7a21770 authored by MARCHE Claude's avatar MARCHE Claude

ITP, make why3webserver work again

parent fa117c16
......@@ -28,12 +28,13 @@ open Format
let interp_request args =
match args with
| "list-provers" -> (Command_req "list-provers", root_node)
| "list-provers" -> (Command_req (root_node,"list-provers"))
| _ -> invalid_arg "Why3web.interp_request"
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) -> ()
......@@ -54,7 +55,6 @@ let print_notification fmt n =
| Message n -> fprintf fmt "{ notification=\"message=\"; %a }"
print_message_notification n
| Dead s -> ()
| Proof_update(nid,status) -> ()
| Task(nid,task) -> ()
let handle_script s args =
......@@ -69,7 +69,8 @@ let handle_script s args =
end
| "getNotifications" ->
let n = P.get_notifications () in
if n <> [] then Pp.sprintf "getNotifications: %a@." (Pp.print_list Pp.space print_notification) n
(* if n <> [] then *)
Pp.sprintf "getNotifications: %a@." (Pp.print_list Pp.space print_notification) n
| _ -> "bad request"
let plist fmt l =
......@@ -130,8 +131,8 @@ let usage_str = sprintf
let () =
Whyconf.Args.parse spec (fun f -> Queue.add f files) usage_str;
if Queue.is_empty files then
Whyconf.Args.exit_with_usage spec usage_str;
Queue.iter (fun f -> P.push_request (Itp_server.Open_req f, Itp_server.root_node)) files;
Wserver.main_loop None 6789 handler stdin_handler
Whyconf.Args.parse spec (fun f -> Queue.add f files) usage_str;
if Queue.is_empty files then
Whyconf.Args.exit_with_usage spec usage_str;
Queue.iter (fun f -> P.push_request (Itp_server.Open_session_req f)) files;
Wserver.main_loop None 6789 handler stdin_handler
......@@ -429,7 +429,7 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
module C = Controller_itp.Make(S)
let _debug = Debug.register_flag "itp_server"
let debug = Debug.register_flag "itp_server" ~desc:"ITP server"
(************************)
(* parsing command line *)
......@@ -443,11 +443,17 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
let get_configs () = config, base_config
let task_driver =
let main = Whyconf.get_main config in
let d = Filename.concat (Whyconf.datadir main)
(Filename.concat "drivers" "why3_itp.drv")
in
Driver.load_driver env d []
try
let main = Whyconf.get_main config in
let d = Filename.concat (Whyconf.datadir main)
(Filename.concat "drivers" "why3_itp.drv")
in
let d = Driver.load_driver env d [] in
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
......@@ -475,9 +481,12 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
let cont =
try
create_controller env provers
with LoadDriverFailure (p, e) -> P.notify (Message (
Error "To implement: could not load driver"));
raise (LoadDriverFailure (p, e)) (* TODO *)
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 *)
(* ------------ init controller ------------ *)
......
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