Commit cbad94c7 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Merge branch 'itp' into itp_new_why3session

Conflicts:
	src/session/itp_server.ml
	src/session/server_utils.mli
parents 07533ceb 7dda1c7d
......@@ -139,6 +139,9 @@ val call_on_file :
printer_mapping : Printer.printer_mapping ->
?inplace : bool ->
string -> prover_call
(* inplace=true is used to make a save of the file on which the prover was
called. It is renamed as %f.save if the command [actualcommand] fails *)
val call_on_buffer :
command : string ->
......@@ -156,7 +159,11 @@ val call_on_buffer :
@param res_parser : prover result parser
@param filename : the suffix of the proof task's file, if the prover
doesn't accept stdin. *)
doesn't accept stdin.
@param inplace : it is used to make a save of the file on which the
prover was called. It is renamed as %f.save if inplace=true and the command
[actualcommand] fails *)
type prover_update =
| NoUpdates
......
......@@ -182,7 +182,16 @@ let env, gconfig = try
exit 1
(* Initialization of config, provers, task_driver and controller in the server *)
let () = Server.init_server gconfig.config env
let () =
let dir =
try
Server_utils.get_session_dir ~allow_mkdir:true files
with Invalid_argument s ->
Format.eprintf "Error: %s@." s;
Whyconf.Args.exit_with_usage spec usage_str
in
Server.init_server gconfig.config env dir;
Queue.iter (fun f -> send_request (Add_file_req f)) files
let () =
Debug.dprintf debug "[GUI] Init the GTK interface...@?";
......@@ -1576,9 +1585,6 @@ let (_ : GMenu.image_menu_item) =
let () =
S.timeout ~ms:100 (fun () -> List.iter treat_notification (get_notified ()); true);
let f = Queue.pop files in
send_request (Open_session_req f);
Queue.iter (fun f -> send_request (Add_file_req f)) files;
(* temporary *)
vpan222#set_position 500;
goals_view#expand_all ();
......
......@@ -139,10 +139,13 @@ let () =
let config, _base_config, env =
Whyconf.Args.initialize spec (fun f -> Queue.add f files) usage_str
in
if Queue.is_empty files then
Whyconf.Args.exit_with_usage spec usage_str;
let f = Queue.pop files in
P.push_request (Open_session_req f);
let dir =
try
Server_utils.get_session_dir ~allow_mkdir:true files
with Invalid_argument s ->
Format.eprintf "Error: %s@." s;
Whyconf.Args.exit_with_usage spec usage_str
in
S.init_server config env dir;
Queue.iter (fun f -> P.push_request (Add_file_req f)) files;
S.init_server config env;
Wserver.main_loop None 6789 handler stdin_handler
......@@ -72,28 +72,45 @@ let init_proof_state () = {
type controller =
{ mutable controller_session: Session_itp.session;
proof_state: proof_state;
controller_config : Whyconf.config;
controller_env: Env.env;
controller_provers:
(Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
}
(*
let clear_proof_state c =
Stdlib.Hstr.clear c.proof_state.file_state;
Hid.clear c.proof_state.th_state;
Htn.clear c.proof_state.tn_state;
Hpn.clear c.proof_state.pn_state
let create_controller env =
{
controller_session = Session_itp.dummy_session;
proof_state = init_proof_state ();
controller_env = env;
controller_provers = Whyconf.Hprover.create 7;
}
let init_controller s c =
clear_proof_state (c);
c.controller_session <- s
*)
let create_controller config env ses =
let c =
{
controller_session = ses;
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 set_session cont ses = cont.controller_session <- ses
let tn_proved c tid = Htn.find_def c.proof_state.tn_state false tid
let pn_proved c pid = Hpn.find_def c.proof_state.pn_state false pid
......@@ -372,8 +389,7 @@ let merge_file (old_ses : session) (c : controller) ~use_shapes _ file =
in
merge_file_section
c.controller_session ~use_shapes ~old_ses ~old_theories
~env:c.controller_env file_name new_theories format;
reload_session_proof_state c
~env:c.controller_env file_name new_theories format
let reload_files (c : controller) ~use_shapes =
let old_ses = c.controller_session in
......@@ -382,7 +398,8 @@ let reload_files (c : controller) ~use_shapes =
try
Stdlib.Hstr.iter
(fun f -> merge_file old_ses c ~use_shapes f)
(get_files old_ses)
(get_files old_ses);
reload_session_proof_state c
with e ->
c.controller_session <- old_ses;
raise e
......@@ -448,7 +465,7 @@ let register_observer = (:=) observer
module Hprover = Whyconf.Hprover
let build_prover_call c id pr limit callback =
let build_prover_call ~cntexample c id pr limit callback =
let (config_pr,driver) = Hprover.find c.controller_provers pr in
let command =
Whyconf.get_complete_command
......@@ -457,7 +474,7 @@ let build_prover_call c id pr limit callback =
let task = Session_itp.get_task c.controller_session id in
let table = Session_itp.get_table c.controller_session id in
let call =
Driver.prove_task ?old:None ~cntexample:true ~inplace:false ~command
Driver.prove_task ?old:None ~cntexample:cntexample ~inplace:false ~command
~limit ?name_table:table driver task
in
let pa = (c.controller_session,id,pr,callback,false,call) in
......@@ -499,9 +516,9 @@ let timeout_handler () =
try
for _i = Queue.length prover_tasks_in_progress
to 3 * !max_number_of_running_provers do
let (c,id,pr,limit,callback) = Queue.pop scheduled_proof_attempts in
let (c,id,pr,limit,callback,cntexample) = Queue.pop scheduled_proof_attempts in
try
build_prover_call c id pr limit callback
build_prover_call ~cntexample c id pr limit callback
with e when not (Debug.test_flag Debug.stack_trace) ->
(*Format.eprintf
"@[Exception raised in Controller_itp.build_prover_call:@ %a@.@]"
......@@ -525,7 +542,7 @@ let interrupt () =
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
let (_c,_id,_pr,_limit,callback,_cntexample) = Queue.pop scheduled_proof_attempts in
callback Interrupted
done;
!observer 0 0 0
......@@ -537,21 +554,21 @@ let run_timeout_handler () =
S.timeout ~ms:125 timeout_handler;
end
let schedule_proof_attempt_r c id pr ~limit ~callback =
let schedule_proof_attempt_r c id pr ~counterexmp ~limit ~callback =
let panid =
graft_proof_attempt c.controller_session id pr ~limit
in
Queue.add (c,id,pr,limit,callback panid) scheduled_proof_attempts;
Queue.add (c,id,pr,limit,callback panid,counterexmp) scheduled_proof_attempts;
callback panid Scheduled;
run_timeout_handler ()
let schedule_proof_attempt c id pr ~limit ~callback ~notification =
let schedule_proof_attempt c id pr ~counterexmp ~limit ~callback ~notification =
let callback panid s = callback panid s;
(match s with
| Scheduled | Done _ -> update_goal_node notification c id
| _ -> ())
in
schedule_proof_attempt_r c id pr ~limit ~callback
schedule_proof_attempt_r c id pr ~counterexmp ~limit ~callback
let schedule_transformation_r c id name args ~callback =
let apply_trans () =
......@@ -593,7 +610,7 @@ let schedule_transformation c id name args ~callback ~notification =
open Strategy
let run_strategy_on_goal
c id strat ~callback_pa ~callback_tr ~callback ~notification =
c id strat ~counterexmp ~callback_pa ~callback_tr ~callback ~notification =
let rec exec_strategy pc strat g =
if pc < 0 || pc >= Array.length strat then
callback STShalt
......@@ -621,7 +638,7 @@ let run_strategy_on_goal
let limit = { Call_provers.empty_limit with
Call_provers.limit_time = timelimit;
limit_mem = memlimit} in
schedule_proof_attempt c g p ~limit ~callback ~notification
schedule_proof_attempt c g p ~counterexmp ~limit ~callback ~notification
| Itransform(trname,pcsuccess) ->
let callback ntr =
callback_tr ntr;
......@@ -708,7 +725,7 @@ let rec copy_paste ~notification ~callback_pa ~callback_tr c from_any to_any =
raise BadCopyPaste
| APn from_pn, APn to_pn ->
let from_pa_list = get_proof_attempts s from_pn in
List.iter (fun x -> schedule_pa_with_same_arguments c x to_pn
List.iter (fun x -> schedule_pa_with_same_arguments c x to_pn ~counterexmp:false
~callback:callback_pa ~notification) from_pa_list;
let from_tr_list = get_transformations s from_pn in
let callback x st = callback_tr st;
......@@ -751,7 +768,7 @@ let replay_proof_attempt c pr limit (parid: proofNodeID) id ~callback ~notificat
if not (Hprover.mem c.controller_provers pr) then
callback id (Uninstalled pr)
else
schedule_proof_attempt c parid pr ~limit ~callback ~notification
schedule_proof_attempt c parid pr ~counterexmp:false ~limit ~callback ~notification
type report =
| Result of Call_provers.prover_result * Call_provers.prover_result
......
......@@ -68,15 +68,17 @@ type proof_state
type controller = private
{ mutable controller_session : Session_itp.session;
proof_state : proof_state;
controller_config : Whyconf.config;
controller_env : Env.env;
controller_provers : (Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
}
val create_controller: Env.env -> controller
(** creates a controller with no prover and an empty session *)
val create_controller: Whyconf.config -> Env.env -> Session_itp.session -> controller
(** creates a controller for the given 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 *)
(* TEMPORARY *)
val set_session : controller -> Session_itp.session -> unit
(** Used to find if a proof/trans node or theory is proved or not *)
val tn_proved: controller -> Session_itp.transID -> bool
......@@ -180,6 +182,7 @@ val schedule_proof_attempt :
controller ->
proofNodeID ->
Whyconf.prover ->
counterexmp:bool ->
limit:Call_provers.resource_limit ->
callback:(proofAttemptID -> proof_attempt_status -> unit) ->
notification:notifier -> unit
......@@ -206,6 +209,7 @@ val run_strategy_on_goal :
controller ->
proofNodeID ->
Strategy.t ->
counterexmp:bool ->
callback_pa:(proofAttemptID -> proof_attempt_status -> unit) ->
callback_tr:(transformation_status -> unit) ->
callback:(strategy_status -> unit) ->
......
......@@ -92,7 +92,9 @@ type ide_request =
| Prove_req of node_ID * prover * Call_provers.resource_limit
| Transform_req of node_ID * transformation * string list
| Strategy_req of node_ID * strategy
(*
| Open_session_req of string
*)
| Add_file_req of string
| Set_max_tasks_req of int
| Get_file_contents of string
......@@ -118,7 +120,8 @@ let modify_session (r: ide_request) =
| Add_file_req _ | Remove_subtree _ | Copy_paste _ | Copy_detached _
| Replay_req | Clean_req | Mark_obsolete_req _ -> true
| Open_session_req _ | Set_max_tasks_req _ | Get_file_contents _
(*| Open_session_req _ *)
| Set_max_tasks_req _ | Get_file_contents _
| Get_task _ | Save_file_req _ | Get_first_unproven_node _
| Get_Session_Tree_req | Save_req | Reload_req | Exit_req
| Interrupt_req -> false
......@@ -98,7 +98,9 @@ type ide_request =
| Prove_req of node_ID * prover * Call_provers.resource_limit
| Transform_req of node_ID * transformation * string list
| Strategy_req of node_ID * strategy
(*
| Open_session_req of string
*)
| Add_file_req of string
| Set_max_tasks_req of int
| Get_file_contents of string
......
......@@ -247,7 +247,9 @@ let print_request fmt r =
| Prove_req (_nid, prover, _rl) -> fprintf fmt "prove with %s" prover
| Transform_req (_nid, tr, _args) -> fprintf fmt "transformation :%s" tr
| Strategy_req (_nid, st) -> fprintf fmt "strategy %s" st
(*
| Open_session_req f -> fprintf fmt "open session file %s" f
*)
| Add_file_req f -> fprintf fmt "open file %s" f
| Set_max_tasks_req i -> fprintf fmt "set max tasks %i" i
| Get_file_contents _f -> fprintf fmt "get file contents"
......@@ -323,7 +325,7 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
module C = Controller_itp.Make(S)
let debug = Debug.register_flag "itp_server" ~desc:"ITP server"
let debug = Debug.register_flag "itp_server" ~desc:"ITP server"
(****************)
......@@ -365,8 +367,7 @@ let () =
]
type server_data =
{ config : Whyconf.config;
task_driver : Driver.driver;
{ task_driver : Driver.driver;
cont : Controller_itp.controller;
}
......@@ -510,26 +511,6 @@ let get_locations t =
let get_prover_list (config: Whyconf.config) =
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 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;
cont = c }
(* ----------------------------------- ------------------------------------- *)
let get_node_type (node: any) =
......@@ -679,7 +660,7 @@ let get_locations t =
let get_prover p =
let d = get_server_data () in
match return_prover p d.config with
match return_prover p d.cont.controller_config with
| None -> raise (Bad_prover_name p)
| Some c -> c
......@@ -849,16 +830,22 @@ let get_locations t =
P.notify (Message (Open_File_Error ("File already in session: " ^ fn)))
(* ------------ init controller ------------ *)
(* ------------ init server ------------ *)
(* Init cont on file or directory. It is called only when an
Open_session_req is requested *)
let init_cont f =
let init_server config env f =
Debug.dprintf debug "[ITP server] loading session %s@." f;
let ses,use_shapes = Session_itp.load_session f in
Debug.dprintf debug "[ITP server] creating controller@.";
let c = create_controller config env ses in
let task_driver = task_driver config env in
server_data := Some
{ task_driver = task_driver;
cont = c };
let d = get_server_data () in
let prover_list = get_prover_list d.config in
let prover_list = get_prover_list 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
let l = strategies d.cont.controller_env config loaded_strategies in
List.map (fun (a,_,_,_) -> a) l
in
let infos =
......@@ -870,20 +857,15 @@ let get_locations t =
Hstr.fold (fun c _ acc -> c :: acc) commands_table []
}
in
match cont_from_session ~notify:P.notify d.cont f with
| Some false ->
begin
add_file_to_session d.cont f;
P.notify (Initialized infos);
true
end
| Some true ->
P.notify (Initialized infos);
true
| None ->
(* Even if it fails we want to load source files *)
load_files_session ();
false
Debug.dprintf debug "[ITP server] sending initialization infos@.";
P.notify (Initialized infos);
Debug.dprintf debug "[ITP server] reloading source files@.";
let b = reload_files d.cont ~use_shapes in
if b then
init_and_send_the_tree ()
else
load_files_session ()
(* ----------------- Schedule proof attempt -------------------- *)
......@@ -919,12 +901,12 @@ let get_locations t =
| _ -> ()
with Not_found -> ()
let schedule_proof_attempt nid (p: Whyconf.config_prover) limit =
let schedule_proof_attempt ~counterexmp nid (p: Whyconf.config_prover) limit =
let d = get_server_data () in
let prover = p.Whyconf.prover in
let callback = callback_update_tree_proof d.cont in
let unproven_goals = unproven_goals_below_id d.cont (any_from_node_ID nid) in
List.iter (fun id -> C.schedule_proof_attempt d.cont id prover
List.iter (fun id -> C.schedule_proof_attempt d.cont id prover ~counterexmp
~limit ~callback ~notification:(notify_change_proved d.cont))
unproven_goals
......@@ -964,10 +946,10 @@ let get_locations t =
let debug_strat = Debug.register_flag "strategy_exec" ~desc:"Trace strategies execution"
let run_strategy_on_task nid s =
let run_strategy_on_task ~counterexmp nid s =
let d = get_server_data () in
let unproven_goals = unproven_goals_below_id d.cont (any_from_node_ID nid) in
let l = strategies d.cont.controller_env d.config loaded_strategies in
let l = strategies d.cont.controller_env d.cont.controller_config loaded_strategies in
let st = List.filter (fun (_,c,_,_) -> c=s) l in
match st with
| [(n,_,_,st)] ->
......@@ -978,7 +960,8 @@ let get_locations t =
let callback_pa = callback_update_tree_proof d.cont in
let callback_tr st = callback_update_tree_transform st in
List.iter (fun id ->
C.run_strategy_on_goal d.cont id st ~callback_pa ~callback_tr ~callback ~notification:(notify_change_proved d.cont))
C.run_strategy_on_goal d.cont id st ~counterexmp
~callback_pa ~callback_tr ~callback ~notification:(notify_change_proved d.cont))
unproven_goals
| _ -> Debug.dprintf debug_strat "[strategy_exec] strategy '%s' not found@." s
......@@ -1072,6 +1055,7 @@ let get_locations t =
let rec treat_request r =
let d = get_server_data () in
let config = d.cont.controller_config in
try (
match r with
| Prove_req (nid,p,limit) ->
......@@ -1080,10 +1064,14 @@ let get_locations t =
in
begin match p with
| None -> ()
| Some p -> schedule_proof_attempt nid p limit
| Some p ->
let counterexmp = Whyconf.cntexample (Whyconf.get_main config) in
schedule_proof_attempt ~counterexmp nid p limit
end
| Transform_req (nid, t, args) -> apply_transform nid t args
| Strategy_req (nid, st) -> run_strategy_on_task nid st
| Strategy_req (nid, st) ->
let counterexmp = Whyconf.cntexample (Whyconf.get_main config) in
run_strategy_on_task ~counterexmp nid st
| Clean_req -> clean_session ()
| Save_req -> save_session ()
| Reload_req -> reload_session ()
......@@ -1129,11 +1117,15 @@ let get_locations t =
| Command_req (nid, cmd) ->
begin
let snid = get_proof_node_id nid in
match (interp commands_table d.config d.cont snid cmd) with
match (interp commands_table d.cont.controller_config d.cont snid cmd) with
| Transform (s, _t, args) -> treat_request (Transform_req (nid, s, args))
| 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
| Prove (p, limit) ->
let counterexmp = Whyconf.cntexample (Whyconf.get_main config) in
schedule_proof_attempt ~counterexmp nid p limit
| Strategies st ->
let counterexmp = Whyconf.cntexample (Whyconf.get_main config) in
run_strategy_on_task ~counterexmp nid st
| Help_message s -> P.notify (Message (Help s))
| QError s -> P.notify (Message (Query_Error (nid, s)))
| Other (s, _args) ->
......@@ -1144,12 +1136,14 @@ let get_locations t =
let f = Sysutil.relativize_filename
(Session_itp.get_dir d.cont.controller_session) f in
read_and_send f
(*
| Open_session_req file_or_dir_name ->
let b = init_cont file_or_dir_name in
if b then
reload_session ()
else
() (* Eventually print debug here *)
*)
| Set_max_tasks_req i -> C.set_max_tasks i
| Exit_req -> exit 0
)
......
......@@ -15,12 +15,7 @@ end
module Make (S:Controller_itp.Scheduler) (P:Protocol) : sig
(*
val get_configs: unit -> Whyconf.config * Whyconf.config
*)
(* Initialize server_data *)
val init_server: Whyconf.config -> Env.env -> unit
(* Nothing ! *)
(* Initialize server with the given config, env and filename for the session *)
val init_server: Whyconf.config -> Env.env -> string -> unit
end
......@@ -121,7 +121,9 @@ let convert_request_constructor (r: ide_request) =
| Prove_req _ -> String "Prove_req"
| Transform_req _ -> String "Transform_req"
| Strategy_req _ -> String "Strategy_req"
(*
| Open_session_req _ -> String "Open_session_req"
*)
| Add_file_req _ -> String "Add_file_req"
| Save_file_req _ -> String "Save_file_req"
| Set_max_tasks_req _ -> String "Set_max_tasks_req"
......@@ -162,9 +164,11 @@ let print_request_to_json (r: ide_request): Json_base.json =
convert_record ["ide_request", cc r;
"node_ID", Int nid;
"strategy", String str]
(*
| Open_session_req f ->
convert_record ["ide_request", cc r;
"file", String f]
*)
| Add_file_req f ->
convert_record ["ide_request", cc r;
"file", String f]
......@@ -434,10 +438,11 @@ let parse_request (constr: string) j =
let str = get_string (get_field j "strategy") in
Strategy_req (nid, str)
(*
| "Open_session_req" ->
let f = get_string (get_field j "file") in
Open_session_req f
*)
| "Add_file_req" ->
let f = get_string (get_field j "file") in
Add_file_req f
......
......@@ -4,38 +4,46 @@
(* TODO: all occurences of Format.eprintf in this file should be
replaced by proper server notifications *)
open Session_itp
open Itp_communication
exception NotADirectory of string
exception BadFileName of string
let default_session_filename = "why3session.xml"
let get_project_dir fname =
if not (Sys.file_exists fname) then raise Not_found;
let d =
if Sys.is_directory fname then fname
else if Filename.basename fname = default_session_filename then begin
(*
Debug.dprintf debug "Info: found db file '%s'@." fname;
*)
Filename.dirname fname
end
let has_extension f =
try
let _ = Filename.chop_extension f in true
with Invalid_argument _ -> false
let get_session_dir ~allow_mkdir files =
if Queue.is_empty files then invalid_arg "no files given";
let first = Queue.pop files in