Commit f856d94a authored by MARCHE Claude's avatar MARCHE Claude

reloading in IDE

parent d89815f1
......@@ -11,7 +11,7 @@ version_bad = "0.92"
version_bad = "0.91"
version_bad = "0.9"
version_bad = "0.8"
command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f"
command = "@LOCALBIN@why3-cpulimit %t %m -s %e -proof %f"
driver = "drivers/alt_ergo_trunk.drv"
[ATP alt-ergo]
......
......@@ -202,6 +202,7 @@ let iconname_prover = "wizard32"
let iconname_transf = "configure32"
let iconname_editor = "edit32"
let iconname_replay = "refresh32"
let iconname_reload = "movefile32"
let iconname_remove = "deletefile32"
let iconname_cleaning = "trashb32"
......@@ -227,6 +228,7 @@ let image_prover = ref !image_default
let image_transf = ref !image_default
let image_editor = ref !image_default
let image_replay = ref !image_default
let image_reload = ref !image_default
let image_remove = ref !image_default
let image_cleaning = ref !image_default
......@@ -253,6 +255,7 @@ let resize_images size =
image_transf := image ~size iconname_transf;
image_editor := image ~size iconname_editor;
image_replay := image ~size iconname_replay;
image_reload := image ~size iconname_reload;
image_remove := image ~size iconname_remove;
image_cleaning := image ~size iconname_cleaning;
()
......
......@@ -72,6 +72,7 @@ val image_prover : GdkPixbuf.pixbuf ref
val image_transf : GdkPixbuf.pixbuf ref
val image_editor : GdkPixbuf.pixbuf ref
val image_replay : GdkPixbuf.pixbuf ref
val image_reload : GdkPixbuf.pixbuf ref
val image_remove : GdkPixbuf.pixbuf ref
val image_cleaning : GdkPixbuf.pixbuf ref
......
......@@ -367,12 +367,15 @@ module M = Session.Make
| Some r -> Some r#iter
in
let iter = goals_model#append ?parent () in
goals_model#set ~row:iter ~column:index_column (-1);
goals_model#get_row_reference (goals_model#get_path iter)
let remove row =
let (_:bool) = goals_model#remove row#iter in ()
let reset () = goals_model#clear ()
let idle f =
let (_ : GMain.Idle.id) = GMain.Idle.add f in ()
......@@ -408,47 +411,57 @@ let set_proof_state ~obsolete a =
let model_index = Hashtbl.create 17
let get_any row =
try
let get_any row =
try
let row = goals_model#get_iter row in
let idx = goals_model#get ~row ~column:index_column in
Hashtbl.find model_index idx
with Not_found -> invalid_arg "Gmain.get_index"
let init =
let cpt = ref 0 in
let notify any =
match any with
| M.Goal g ->
set_row_status (M.goal_key g) (M.goal_proved g)
| M.Theory th ->
set_row_status (M.theory_key th) (M.verified th)
| M.File file ->
set_row_status file.M.file_key file.M.file_verified
| M.Proof_attempt a ->
set_proof_state ~obsolete:a.M.proof_obsolete a
| M.Transformation tr ->
set_row_status tr.M.transf_key tr.M.transf_proved
let init =
let cpt = ref (-1) in
fun row any ->
incr cpt;
Hashtbl.add model_index !cpt any;
goals_model#set ~row:row#iter ~column:index_column !cpt;
goals_model#set ~row:row#iter ~column:icon_column
let ind = goals_model#get ~row:row#iter ~column:index_column in
if ind < 0 then
begin
incr cpt;
Hashtbl.add model_index !cpt any;
goals_model#set ~row:row#iter ~column:index_column !cpt
end
else
begin
Hashtbl.replace model_index ind any;
end;
goals_model#set ~row:row#iter ~column:icon_column
(match any with
| M.Goal _ -> !image_file
| M.Theory _
| M.Theory _
| M.File _ -> !image_directory
| M.Proof_attempt _ -> !image_prover
| M.Transformation _ -> !image_transf);
goals_model#set ~row:row#iter ~column:name_column
goals_model#set ~row:row#iter ~column:name_column
(match any with
| M.Goal g -> M.goal_expl g
| M.Theory th -> M.theory_name th
| M.File f -> Filename.basename f.M.file_name
| M.Proof_attempt a -> let p = a.M.prover in
p.Session.prover_name ^ " " ^ p.Session.prover_version
| M.Transformation tr -> Session.transformation_id tr.M.transf)
| M.Transformation tr -> Session.transformation_id tr.M.transf);
notify any
let notify any =
match any with
| M.Goal g ->
set_row_status (M.goal_key g) (M.goal_proved g)
| M.Theory th ->
set_row_status (M.theory_key th) (M.verified th)
| M.File file ->
set_row_status file.M.file_key file.M.file_verified
| M.Proof_attempt a ->
set_proof_state ~obsolete:false a
| M.Transformation tr ->
set_row_status tr.M.transf_key tr.M.transf_proved
(********************)
......@@ -490,7 +503,7 @@ let () =
let () =
try
eprintf "Opening session...@?";
M.open_session ~env:gconfig.env ~provers:gconfig.provers
M.open_session ~env:gconfig.env ~provers:gconfig.provers
~init ~notify project_dir;
M.maximum_running_proofs := gconfig.max_running_processes;
eprintf " done@."
......@@ -567,7 +580,7 @@ let replay_obsolete_proofs () =
List.iter
(fun row ->
let a = get_any row in
M.replay ~obsolete_only:true
M.replay ~obsolete_only:true
~context_unproved_goals_only:!context_unproved_goals_only a)
goals_view#selection#get_selected_rows
......@@ -685,14 +698,14 @@ let exit_function () =
match l with
| [] -> ()
| f :: _ ->
eprintf "first element is a '%s' with %d sub-elements@."
eprintf "first element is a '%s' with %d sub-elements@."
f.Xml.name (List.length f.Xml.elements);
with e -> eprintf "test reloading failed with exception %s@."
(Printexc.to_string e)
end;
let ret = Sys.command "xmllint --noout --dtdvalid share/why3session.dtd essai.xml" in
if ret = 0 then eprintf "DTD validation succeeded, good!@.";
if ret = 0 then eprintf "DTD validation succeeded, good!@.";
*)
M.save_session ();
GMain.quit ()
......@@ -911,7 +924,7 @@ let () =
let () = b#set_image i#coerce in
let (_ : GtkSignal.id) =
b#connect#pressed ~callback:inline_selected_goals
in
in
()
......@@ -1091,13 +1104,13 @@ let select_row p =
match a with
| M.Goal g ->
let callback = function
| [t] ->
| [t] ->
let task_text = Pp.string_of Pretty.print_task t in
task_view#source_buffer#set_text task_text;
task_view#scroll_to_mark `INSERT;
scroll_to_source_goal g
| _ -> assert false
in
in
M.apply_transformation ~callback intro_transformation (M.get_task g)
| M.Theory th ->
......@@ -1177,6 +1190,18 @@ let () =
b#connect#pressed ~callback:replay_obsolete_proofs
in ()
let () =
let b = GButton.button ~packing:tools_box#add ~label:"Reload" () in
b#misc#set_tooltip_markup "Reloads the files";
let i = GMisc.image ~pixbuf:(!image_reload) () in
let () = b#set_image i#coerce in
let (_ : GtkSignal.id) =
b#connect#pressed ~callback:(fun () ->
current_file := "";
M.reload_all gconfig.provers)
in ()
(*************)
(* removing *)
(*************)
......
......@@ -56,7 +56,7 @@ let loadpath = (Whyconf.loadpath (Whyconf.get_main config))
let env = Lexer.create_env loadpath
let provers = Whyconf.get_provers config
let provers = Whyconf.get_provers config
let provers =
Util.Mstr.fold (Session.get_prover_data env) provers Util.Mstr.empty
......@@ -71,13 +71,15 @@ module M = Session.Make
(struct
type key = int
let create ?parent () =
let create ?parent () =
match parent with
| None -> 0
| Some n -> n+1
let remove _row = ()
let reset () = ()
let idle f =
match !idle_handler with
| None -> idle_handler := Some f;
......@@ -115,16 +117,16 @@ let main_loop () =
else
(* attempt to run the idle handler *)
match !idle_handler with
| None ->
begin
let ms =
| None ->
begin
let ms =
match !timeout_handler with
| None -> raise Exit
| Some(ms,_) -> ms
in
usleep (ms -. time)
end
| Some f ->
| Some f ->
let b = f () in
if b then () else
begin
......@@ -136,8 +138,8 @@ open Format
let model_index = Hashtbl.create 257
let init =
let cpt = ref 0 in
let init =
let cpt = ref 0 in
fun _row any ->
incr cpt;
Hashtbl.add model_index !cpt any;
......@@ -152,7 +154,7 @@ let init =
in
printf "Item '%s' loaded@." name
let string_of_result result =
let string_of_result result =
match result with
| Session.Undone -> "undone"
| Session.Scheduled -> "scheduled"
......@@ -166,7 +168,7 @@ let string_of_result result =
| Call_provers.Failure _ -> "failure"
| Call_provers.HighFailure -> "high failure"
let print_result fmt res =
let print_result fmt res =
let t = match res with
| Session.Done { Call_provers.pr_time = time } ->
Format.sprintf "(%.2f)" time
......@@ -186,8 +188,8 @@ let notify any =
file.M.file_verified
| M.Proof_attempt a ->
let p = a.M.prover in
printf "Proof with '%s %s' gives %a@."
p.Session.prover_name p.Session.prover_version
printf "Proof with '%s %s' gives %a@."
p.Session.prover_name p.Session.prover_version
print_result a.M.proof_state
| M.Transformation tr ->
printf "Transformation '%s' proved: %b@."
......@@ -220,12 +222,12 @@ let main () =
try
eprintf "Opening session...@?";
M.open_session ~env ~provers ~init ~notify project_dir;
M.maximum_running_proofs :=
M.maximum_running_proofs :=
Whyconf.running_provers_max (Whyconf.get_main config);
eprintf " done@.";
let files = M.get_all_files () in
List.iter
(fun f ->
List.iter
(fun f ->
eprintf "Replaying file '%s'@." f.M.file_name;
M.replay ~obsolete_only:false
~context_unproved_goals_only:false (M.File f)) files;
......
......@@ -25,7 +25,7 @@ open Format
(* provers *)
(***************************)
type prover_data =
type prover_data =
{ prover_id : string;
prover_name : string;
prover_version : string;
......@@ -50,7 +50,7 @@ let get_prover_data env id pr acc =
acc
with e ->
eprintf "Failed to load driver %s for prover %s (%a). prover disabled@."
pr.Whyconf.driver
pr.Whyconf.driver
pr.Whyconf.name
Exn_printer.exn_printer e
;
......@@ -64,7 +64,7 @@ type trans =
| Trans_one of Task.task Trans.trans
| Trans_list of Task.task Trans.tlist
type transformation_data =
type transformation_data =
{ transformation_name : string;
transformation : trans;
}
......@@ -82,7 +82,7 @@ let lookup_trans env name =
let lookup_transformation env =
let h = Hashtbl.create 13 in
fun name ->
try
try
Hashtbl.find h name
with Not_found ->
let t = {transformation_name = name;
......@@ -109,6 +109,7 @@ module type OBSERVER = sig
type key
val create: ?parent:key -> unit -> key
val remove: key -> unit
val reset: unit -> unit
val timeout: ms:int -> (unit -> bool) -> unit
val idle: (unit -> bool) -> unit
......@@ -138,7 +139,7 @@ and goal =
goal_expl : string option;
parent : goal_parent;
mutable task: Task.task option;
checksum : string;
mutable checksum : string;
goal_key : O.key;
mutable proved : bool;
external_proofs: (string, proof_attempt) Hashtbl.t;
......@@ -181,25 +182,25 @@ let theory_key t = t.theory_key
let verified t = t.verified
let goals t = t.goals
let get_theory t =
match t.theory with
| None ->
let get_theory t =
match t.theory with
| None ->
eprintf "Session: theory not yet reimported, this should not happen@.";
assert false
| Some t -> t
let goal_name g = g.goal_name
let goal_expl g =
match g.goal_expl with
let goal_expl g =
match g.goal_expl with
| None -> g.goal_name
| Some s -> s
let goal_key g = g.goal_key
let goal_proved g = g.proved
let transformations g = g.transformations
let get_task g =
match g.task with
| None ->
let get_task g =
match g.task with
| None ->
begin
match g.parent with
| Parent_theory _th ->
......@@ -213,7 +214,7 @@ let get_task g =
let all_files : file list ref = ref []
let get_all_files () = !all_files
(************************)
(* saving state on disk *)
(************************)
......@@ -232,14 +233,14 @@ let save_result fmt r =
let save_status fmt s =
match s with
| Undone | Scheduled | Running ->
fprintf fmt "<undone/>@\n"
| InternalFailure msg ->
fprintf fmt "<internalfailure reason=\"%s\"/>@\n"
fprintf fmt "<undone/>@\n"
| InternalFailure msg ->
fprintf fmt "<internalfailure reason=\"%s\"/>@\n"
(Printexc.to_string msg)
| Done r -> save_result fmt r
let save_proof_attempt fmt _key a =
fprintf fmt "@\n@[<v 1><proof prover=\"%s\" edited=\"%s\">"
fprintf fmt "@\n@[<v 1><proof prover=\"%s\" edited=\"%s\">"
a.prover.prover_id
a.edited_as;
save_status fmt a.proof_state;
......@@ -250,20 +251,20 @@ let opt lab fmt = function
| Some s -> fprintf fmt "%s=\"%s\" " lab s
let rec save_goal fmt g =
fprintf fmt "@\n@[<v 1><goal name=\"%s\" %aproved=\"%b\">"
g.goal_name (opt "expl") g.goal_expl g.proved;
fprintf fmt "@\n@[<v 1><goal name=\"%s\" %asum=\"%s\" proved=\"%b\">"
g.goal_name (opt "expl") g.goal_expl g.checksum g.proved;
Hashtbl.iter (save_proof_attempt fmt) g.external_proofs;
Hashtbl.iter (save_trans fmt) g.transformations;
fprintf fmt "@]@\n</goal>"
and save_trans fmt _ t =
fprintf fmt "@\n@[<v 1><transf name=\"%s\" proved=\"%b\">"
fprintf fmt "@\n@[<v 1><transf name=\"%s\" proved=\"%b\">"
t.transf.transformation_name t.transf_proved;
List.iter (save_goal fmt) t.subgoals;
fprintf fmt "@]@\n</transf>"
let save_theory fmt t =
fprintf fmt "@\n@[<v 1><theory name=\"%s\" verified=\"%b\">"
fprintf fmt "@\n@[<v 1><theory name=\"%s\" verified=\"%b\">"
t.theory_name t.verified;
List.iter (save_goal fmt) t.goals;
fprintf fmt "@]@\n</theory>"
......@@ -272,7 +273,7 @@ let save_file fmt f =
fprintf fmt "@\n@[<v 1><file name=\"%s\" verified=\"%b\">" f.file_name f.file_verified;
List.iter (save_theory fmt) f.theories;
fprintf fmt "@]@\n</file>"
let save fname =
let ch = open_out fname in
let fmt = formatter_of_out_channel ch in
......@@ -348,7 +349,7 @@ let set_proof_state ~obsolete a res =
(*************************)
(* Scheduler *)
(*************************)
(*************************)
(* timeout handler *)
......@@ -581,25 +582,24 @@ let raw_add_external_proof ~obsolete ~edit g p result =
edited_as = edit;
}
in
Hashtbl.add g.external_proofs p.prover_name a;
Hashtbl.add g.external_proofs p.prover_id a;
let any = Proof_attempt a in
!init_fun key any;
!notify_fun any;
(* !notify_fun (Goal g) ? *)
a
(* [raw_add_goal parent name expl t] adds a goal to the given parent
(* [raw_add_goal parent name expl sum t] adds a goal to the given parent
DOES NOT record the new goal in its parent, thus this should not be exported
*)
let raw_add_goal parent name expl topt =
let raw_add_goal parent name expl sum topt =
let parent_key = match parent with
| Parent_theory mth -> mth.theory_key
| Parent_transf mtr -> mtr.transf_key
in
let key = O.create ~parent:parent_key () in
let sum = match topt with
| None -> ""
| None -> sum
| Some t -> task_checksum t
in
let goal = { goal_name = name;
......@@ -664,7 +664,7 @@ let add_theory mfile name th =
let id = (Task.task_goal t).Decl.pr_name in
let name = id.Ident.id_string in
let expl = get_explanation id (Task.task_goal_fmla t) in
let goal = raw_add_goal (Parent_theory mth) name expl (Some t) in
let goal = raw_add_goal (Parent_theory mth) name expl "" (Some t) in
goal :: acc)
[]
tasks
......@@ -691,8 +691,8 @@ let project_dir = ref ""
let read_file fn =
let fn = Filename.concat !project_dir fn in
let env = match !current_env with
| None -> assert false | Some e -> e
let env = match !current_env with
| None -> assert false | Some e -> e
in
let theories = Env.read_file env fn in
let theories =
......@@ -732,48 +732,38 @@ let file_exists fn =
(* reload a file *)
(**********************************)
let rec reimport_any_goal _parent gid _gname t goal __goal_obsolete =
let _info = get_explanation gid (Task.task_goal_fmla t) in
let reload_proof ~provers obsolete goal pid old_a =
try
let p = Util.Mstr.find pid provers in
let old_res = old_a.proof_state in
let obsolete = obsolete or old_a.proof_obsolete in
eprintf "proof_obsolete : %b@." obsolete;
let _a =
raw_add_external_proof ~obsolete ~edit:old_a.edited_as goal p old_res
in
((* something TODO ?*))
with Not_found ->
eprintf
"Warning: prover %s appears in database but is not installed.@."
pid
let rec reload_any_goal ~provers parent gid gname sum t old_goal goal_obsolete =
let info = get_explanation gid (Task.task_goal_fmla t) in
let goal = raw_add_goal parent gname info sum (Some t) in
goal.task <- Some t;
begin
match old_goal with
| None -> ()
| Some g ->
Hashtbl.iter (reload_proof ~provers goal_obsolete goal) g.external_proofs;
Hashtbl.iter (reload_trans ~provers goal_obsolete goal) g.transformations
end;
goal
and reload_trans ~provers:_ _goal_obsolete _goal _tr_id _tr =
()
(*
let goal = raw_add_goal parent gname info t in
let proved = ref false in
let external_proofs = Db.external_proofs db_goal in
Db.Hprover.iter
(fun pid a ->
let pname = Db.prover_name pid in
try
let p = Util.Mstr.find pname gconfig.provers in
let s,t,o,edit = Db.status_and_time a in
if goal_obsolete && not o then Db.set_obsolete a;
let obsolete = goal_obsolete or o in
let s = match s with
| Db.Undone -> Call_provers.HighFailure
| Db.Done r ->
if r = Call_provers.Valid then
if not obsolete then proved := true;
r
in
let r = { Call_provers.pr_answer = s;
Call_provers.pr_output = "";
Call_provers.pr_time = t;
}
in
let (_pa : Model.proof_attempt) =
Helpers.add_external_proof_row ~obsolete ~edit goal p a
(Gscheduler.Done r)
in
((* something TODO ?*))
with Not_found ->
eprintf
"Warning: prover %s appears in database but is not installed.@."
pname
)
external_proofs;
let transformations = Db.transformations db_goal in
Db.Htransf.iter
(fun tr_id tr ->
let trname = Db.transf_name tr_id in
eprintf "Reimporting transformation %s for goal %s @." trname gname;
let trans = trans_of_name trname in
......@@ -867,93 +857,83 @@ let rec reimport_any_goal _parent gid _gname t goal __goal_obsolete =
*)
let reimport_root_goal mth tname goals t : goal =
(* re-imports database informations of a goal in theory mth (named tname)
goals is a table, indexed by names of DB goals formerly known to be
a in theory mth. returns true whenever the task t is known to be
proved *)
(* reloads the task [t] in theory mth (named tname) *)
let reload_root_goal ~provers mth tname old_goals t : goal =
let id = (Task.task_goal t).Decl.pr_name in
let gname = id.Ident.id_string
in
let gname = id.Ident.id_string in
let sum = task_checksum t in
let goal, goal_obsolete =
try
let dbg = Util.Mstr.find gname goals in
let db_sum = dbg.checksum in
let goal_obsolete = sum <> db_sum in
if goal_obsolete then
begin
eprintf "Goal %s.%s has changed@." tname gname;
(*
Db.change_checksum dbg sum
*)
end;
dbg,goal_obsolete
with Not_found ->
assert false (* TODO *)
(*
let dbg = Db.add_goal mth.Model.theory_db gname sum in
dbg,false