Commit 9b6e2bd6 authored by MARCHE Claude's avatar MARCHE Claude

create_controller now immediately load the drivers for provers

parent 66e0b6e4
......@@ -85,13 +85,29 @@ let clear_proof_state c =
Hpn.clear c.proof_state.pn_state
let create_controller config env =
{
controller_session = Session_itp.dummy_session;
proof_state = init_proof_state ();
controller_config = config;
controller_env = env;
controller_provers = Whyconf.Hprover.create 7;
}
let c =
{
controller_session = Session_itp.dummy_session;
proof_state = init_proof_state ();
controller_config = config;
controller_env = env;
controller_provers = Whyconf.Hprover.create 7;
}
in
let provers = Whyconf.get_provers config in
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 ->
Format.eprintf
"[Controller_itp] error while loading driver for prover %a: %a@."
Whyconf.print_prover p.Whyconf.prover
Exn_printer.exn_printer e)
provers;
c
let init_controller s c =
clear_proof_state c;
......
......@@ -74,7 +74,8 @@ type controller = private
}
val create_controller: Whyconf.config -> Env.env -> controller
(** creates a controller with no prover and an empty session *)
(** creates a controller with an empty session.
The config and env is used to load the drivers for the provers. *)
val init_controller: Session_itp.session -> controller -> unit
(** adds a session to a controller *)
......
......@@ -510,20 +510,8 @@ let get_locations t =
Mstr.fold (fun x _ acc -> x :: acc) (Whyconf.get_prover_shortcuts config) []
let init_server config env =
let provers = Whyconf.get_provers config in
let c = create_controller config 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
{ task_driver = task_driver;
cont = c }
......
......@@ -349,18 +349,6 @@ let () =
try
Debug.dprintf debug "Opening session...@?";
let cont = Controller_itp.create_controller config env in
let provers = Whyconf.get_provers config in
Whyconf.Mprover.iter
(fun _ p ->
try
let d = Driver.load_driver cont.Controller_itp.controller_env p.Whyconf.driver [] in
Whyconf.Hprover.add cont.Controller_itp.controller_provers p.Whyconf.prover (p,d)
with e ->
Format.eprintf
"error loading driver for prover %a: %a@."
Whyconf.print_prover p.Whyconf.prover
Exn_printer.exn_printer e)
provers;
let ses,use_shapes = S.load_session project_dir in
Controller_itp.init_controller ses cont;
(* update the session *)
......
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