Commit c2dc9cb2 authored by MARCHE Claude's avatar MARCHE Claude

partial reloading of files

parent 1f4102c3
Copyright (C) 2010 Copyright (C) 2010-2011
François Bobot François Bobot
Jean-Christophe Filliâtre Jean-Christophe Filliâtre
Claude Marché Claude Marché
......
...@@ -180,7 +180,8 @@ let image ?size f = ...@@ -180,7 +180,8 @@ let image ?size f =
| Some s -> | Some s ->
GdkPixbuf.from_file_at_size ~width:s ~height:s n GdkPixbuf.from_file_at_size ~width:s ~height:s n
let iconname_default = "pausehalf32" let iconname_default = "undone32"
let iconname_undone = "undone32"
let iconname_scheduled = "pausehalf32" let iconname_scheduled = "pausehalf32"
let iconname_running = "play32" let iconname_running = "play32"
let iconname_valid = "accept32" let iconname_valid = "accept32"
...@@ -205,6 +206,7 @@ let iconname_remove = "deletefile32" ...@@ -205,6 +206,7 @@ let iconname_remove = "deletefile32"
let iconname_cleaning = "trashb32" let iconname_cleaning = "trashb32"
let image_default = ref (image ~size:20 iconname_default) let image_default = ref (image ~size:20 iconname_default)
let image_undone = ref !image_default
let image_scheduled = ref !image_default let image_scheduled = ref !image_default
let image_running = ref !image_default let image_running = ref !image_default
let image_valid = ref !image_default let image_valid = ref !image_default
...@@ -230,6 +232,7 @@ let image_cleaning = ref !image_default ...@@ -230,6 +232,7 @@ let image_cleaning = ref !image_default
let resize_images size = let resize_images size =
image_default := image ~size iconname_default; image_default := image ~size iconname_default;
image_undone := image ~size iconname_undone;
image_scheduled := image ~size iconname_scheduled; image_scheduled := image ~size iconname_scheduled;
image_running := image ~size iconname_running; image_running := image ~size iconname_running;
image_valid := image ~size iconname_valid; image_valid := image ~size iconname_valid;
...@@ -278,7 +281,7 @@ let show_legend_window () = ...@@ -278,7 +281,7 @@ let show_legend_window () =
ib image_prover; ib image_prover;
i " External prover\n"; i " External prover\n";
ib image_transf; ib image_transf;
i " Split transformation\n"; i " Transformation\n";
it "Status column\n"; it "Status column\n";
ib image_scheduled; ib image_scheduled;
i " Scheduled external proof attempt\n"; i " Scheduled external proof attempt\n";
...@@ -306,13 +309,13 @@ let show_legend_window () = ...@@ -306,13 +309,13 @@ let show_legend_window () =
let show_about_window () = let show_about_window () =
let about_dialog = let about_dialog =
GWindow.about_dialog GWindow.about_dialog
~name:"Why" ~name:"Why3"
~authors:["François Bobot"; ~authors:["François Bobot";
"Jean-Christophe Filliâtre"; "Jean-Christophe Filliâtre";
"Claude Marché"; "Claude Marché";
"Andrei Paskevich" "Andrei Paskevich"
] ]
~copyright:"Copyright 2010 Univ Paris-Sud, CNRS, INRIA" ~copyright:"Copyright 2010-2011 Univ Paris-Sud, CNRS, INRIA"
~license:"GNU Lesser General Public License" ~license:"GNU Lesser General Public License"
~website:"https://gforge.inria.fr/projects/why3" ~website:"https://gforge.inria.fr/projects/why3"
~website_label:"Project web site" ~website_label:"Project web site"
......
...@@ -76,6 +76,7 @@ val image_remove : GdkPixbuf.pixbuf ref ...@@ -76,6 +76,7 @@ val image_remove : GdkPixbuf.pixbuf ref
val image_cleaning : GdkPixbuf.pixbuf ref val image_cleaning : GdkPixbuf.pixbuf ref
(* status icons *) (* status icons *)
val image_undone : GdkPixbuf.pixbuf ref
val image_scheduled : GdkPixbuf.pixbuf ref val image_scheduled : GdkPixbuf.pixbuf ref
val image_running : GdkPixbuf.pixbuf ref val image_running : GdkPixbuf.pixbuf ref
val image_valid : GdkPixbuf.pixbuf ref val image_valid : GdkPixbuf.pixbuf ref
......
...@@ -338,7 +338,7 @@ let clear model = model#clear () ...@@ -338,7 +338,7 @@ let clear model = model#clear ()
let image_of_result ~obsolete result = let image_of_result ~obsolete result =
match result with match result with
| Session.Undone -> !image_scheduled (* TODO *) | Session.Undone -> !image_undone
| Session.Scheduled -> !image_scheduled | Session.Scheduled -> !image_scheduled
| Session.Running -> !image_running | Session.Running -> !image_running
| Session.InternalFailure _ -> !image_failure | Session.InternalFailure _ -> !image_failure
...@@ -424,14 +424,8 @@ let init = ...@@ -424,14 +424,8 @@ let init =
| M.Transformation _ -> !image_transf); | M.Transformation _ -> !image_transf);
goals_model#set ~row ~column:name_column goals_model#set ~row ~column:name_column
(match any with (match any with
| M.Goal g -> | M.Goal g -> M.goal_expl g
(match g.M.goal_expl with | M.Theory th -> M.theory_name th
| None -> g.M.goal_name
| Some s -> s)
| M.Theory th -> th.M.theory_name
(*
th.M.theory.Theory.th_name.Ident.id_string
*)
| M.File f -> Filename.basename f.M.file_name | M.File f -> Filename.basename f.M.file_name
| M.Proof_attempt a -> let p = a.M.prover in | M.Proof_attempt a -> let p = a.M.prover in
p.Session.prover_name ^ " " ^ p.Session.prover_version p.Session.prover_name ^ " " ^ p.Session.prover_version
...@@ -440,9 +434,9 @@ let init = ...@@ -440,9 +434,9 @@ let init =
let notify any = let notify any =
match any with match any with
| M.Goal g -> | M.Goal g ->
set_row_status g.M.goal_key g.M.proved set_row_status (M.goal_key g) (M.goal_proved g)
| M.Theory th -> | M.Theory th ->
set_row_status th.M.theory_key th.M.verified set_row_status (M.theory_key th) (M.verified th)
| M.File file -> | M.File file ->
set_row_status file.M.file_key file.M.file_verified set_row_status file.M.file_key file.M.file_verified
| M.Proof_attempt a -> | M.Proof_attempt a ->
...@@ -488,22 +482,18 @@ let () = ...@@ -488,22 +482,18 @@ let () =
let () = let () =
let dbfname = Filename.concat project_dir "project.xml" in
try try
eprintf "Opening session...@?"; eprintf "Opening session...@?";
M.open_session ~env:gconfig.env ~provers:gconfig.provers M.open_session ~env:gconfig.env ~provers:gconfig.provers
~init ~notify dbfname; ~init ~notify project_dir;
M.maximum_running_proofs := gconfig.max_running_processes; M.maximum_running_proofs := gconfig.max_running_processes;
eprintf " done@." eprintf " done@."
with e -> with e ->
eprintf "Error while opening session with database '%s'@." dbfname; eprintf "Error while opening session with database '%s'@." project_dir;
eprintf "Aborting...@."; eprintf "Aborting...@.";
raise e raise e
let read_file fn =
let fn = Filename.concat project_dir fn in
Env.read_file gconfig.env fn
...@@ -541,7 +531,7 @@ let () = ...@@ -541,7 +531,7 @@ let () =
eprintf "Info: file %s already in database@." fn eprintf "Info: file %s already in database@." fn
else else
try try
M.add_file fn (read_file fn) M.add_file fn
with e -> with e ->
eprintf "@[Error while reading file@ '%s':@ %a@.@]" fn eprintf "@[Error while reading file@ '%s':@ %a@.@]" fn
Exn_printer.exn_printer e; Exn_printer.exn_printer e;
...@@ -629,7 +619,7 @@ let select_file () = ...@@ -629,7 +619,7 @@ let select_file () =
let f = Sysutil.relativize_filename project_dir f in let f = Sysutil.relativize_filename project_dir f in
eprintf "Adding file '%s'@." f; eprintf "Adding file '%s'@." f;
try try
M.add_file f (read_file f) M.add_file f
with e -> with e ->
fprintf str_formatter fprintf str_formatter
"@[Error while reading file@ '%s':@ %a@]" f "@[Error while reading file@ '%s':@ %a@]" f
...@@ -719,24 +709,24 @@ let (_ : GMenu.image_menu_item) = ...@@ -719,24 +709,24 @@ let (_ : GMenu.image_menu_item) =
let rec collapse_proved_goal g = let rec collapse_proved_goal g =
if g.M.proved then if M.goal_proved g then
begin begin
let row = g.M.goal_key in let row = M.goal_key g in
goals_view#collapse_row (goals_model#get_path row); goals_view#collapse_row (goals_model#get_path row);
end end
else else
Hashtbl.iter Hashtbl.iter
(fun _ t -> List.iter collapse_proved_goal t.M.subgoals) (fun _ t -> List.iter collapse_proved_goal t.M.subgoals)
g.M.transformations (M.transformations g)
let collapse_verified_theory th = let collapse_verified_theory th =
if th.M.verified then if M.verified th then
begin begin
let row = th.M.theory_key in let row = M.theory_key th in
goals_view#collapse_row (goals_model#get_path row); goals_view#collapse_row (goals_model#get_path row);
end end
else else
List.iter collapse_proved_goal th.M.goals List.iter collapse_proved_goal (M.goals th)
let collapse_verified_file f = let collapse_verified_file f =
if f.M.file_verified then if f.M.file_verified then
......
...@@ -151,7 +151,7 @@ and transf = ...@@ -151,7 +151,7 @@ and transf =
and theory = and theory =
{ theory_name : string; { theory_name : string;
theory : Theory.theory option; mutable theory : Theory.theory option;
theory_key : O.key; theory_key : O.key;
theory_parent : file; theory_parent : file;
mutable goals : goal list; mutable goals : goal list;
...@@ -172,6 +172,11 @@ type any = ...@@ -172,6 +172,11 @@ type any =
| Proof_attempt of proof_attempt | Proof_attempt of proof_attempt
| Transformation of transf | Transformation of transf
let theory_name t = t.theory_name
let theory_key t = t.theory_key
let verified t = t.verified
let goals t = t.goals
let get_theory t = let get_theory t =
match t.theory with match t.theory with
| None -> | None ->
...@@ -179,6 +184,15 @@ let get_theory t = ...@@ -179,6 +184,15 @@ let get_theory t =
assert false assert false
| Some t -> t | Some t -> t
let goal_name g = g.goal_name
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 = let get_task g =
match g.task with match g.task with
| None -> | None ->
...@@ -256,11 +270,6 @@ let save fname = ...@@ -256,11 +270,6 @@ let save fname =
fprintf fmt "@."; fprintf fmt "@.";
close_out ch close_out ch
let test_save () = save "essai.xml"
let test_load () = Xml.from_file "essai.xml"
(************************) (************************)
(* actions *) (* actions *)
(************************) (************************)
...@@ -314,38 +323,14 @@ and check_transf_proved t = ...@@ -314,38 +323,14 @@ and check_transf_proved t =
check_goal_proved t.parent_goal check_goal_proved t.parent_goal
end end
let set_file_verified f =
f.file_verified <- true;
!notify_fun (File f)
let set_theory_proved ~propagate t =
t.verified <- true;
!notify_fun (Theory t);
let f = t.theory_parent in
if propagate then
if List.for_all (fun t ->
t.verified) f.theories
then set_file_verified f
let rec set_proved ~propagate g =
g.proved <- true;
!notify_fun (Goal g);
if propagate then
match g.parent with
| Parent_theory t ->
if List.for_all (fun g -> g.proved) t.goals then
set_theory_proved ~propagate t
| Parent_transf t ->
if List.for_all (fun g -> g.proved) t.subgoals then
begin
set_proved ~propagate t.parent_goal;
end
let set_proof_state ~obsolete a res = let set_proof_state ~obsolete a res =
a.proof_state <- res; a.proof_state <- res;
a.proof_obsolete <- obsolete; a.proof_obsolete <- obsolete;
!notify_fun (Proof_attempt a) !notify_fun (Proof_attempt a);
match res with
| Done _ ->
check_goal_proved a.proof_goal
| _ -> ()
(*************************) (*************************)
(* Scheduler *) (* Scheduler *)
...@@ -645,7 +630,7 @@ let add_theory mfile name th = ...@@ -645,7 +630,7 @@ let add_theory mfile name th =
tasks tasks
in in
mth.goals <- List.rev goals; mth.goals <- List.rev goals;
if goals = [] then set_theory_proved ~propagate:false mth; check_theory_proved mth;
mth mth
let raw_add_file f = let raw_add_file f =
...@@ -661,7 +646,15 @@ let raw_add_file f = ...@@ -661,7 +646,15 @@ let raw_add_file f =
!notify_fun any; !notify_fun any;
mfile mfile
let add_file f theories = let current_env = ref None
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
in
let theories = Env.read_file env fn in
let theories = let theories =
Theory.Mnm.fold Theory.Mnm.fold
(fun name th acc -> (fun name th acc ->
...@@ -670,10 +663,12 @@ let add_file f theories = ...@@ -670,10 +663,12 @@ let add_file f theories =
| _ -> (Loc.dummy_position,name,th)::acc) | _ -> (Loc.dummy_position,name,th)::acc)
theories [] theories []
in in
let theories = List.sort List.sort
(fun (l1,_,_) (l2,_,_) -> Loc.compare l1 l2) (fun (l1,_,_) (l2,_,_) -> Loc.compare l1 l2)
theories theories
in
let add_file f =
let theories = read_file f in
let mfile = raw_add_file f in let mfile = raw_add_file f in
let mths = let mths =
List.fold_left List.fold_left
...@@ -683,7 +678,7 @@ let add_file f theories = ...@@ -683,7 +678,7 @@ let add_file f theories =
[] theories [] theories
in in
mfile.theories <- List.rev mths; mfile.theories <- List.rev mths;
if theories = [] then set_file_verified mfile check_file_verified mfile
let file_exists fn = let file_exists fn =
...@@ -855,57 +850,63 @@ let reimport_root_goal mth tname goals t : Model.goal * bool = ...@@ -855,57 +850,63 @@ let reimport_root_goal mth tname goals t : Model.goal * bool =
in in
reimport_any_goal (Model.Theory mth) id gname t db_goal goal_obsolete reimport_any_goal (Model.Theory mth) id gname t db_goal goal_obsolete
(* reimports all files *) *)
let files_in_db = Db.files ()
let () = (* reloads a file *)
List.iter
(fun (f,fn) ->
eprintf "Reimporting file '%s'@." fn;
let mfile = Helpers.add_file_row fn f in
try
let theories = read_file fn in
let ths = Db.theories f in
let (mths,file_proved) =
List.fold_left
(fun (acc,file_proved) (_,tname,th) ->
eprintf "Reimporting theory '%s'@."tname;
let db_th =
try
Util.Mstr.find tname ths
with Not_found -> Db.add_theory f tname
in
let mth = Helpers.add_theory_row mfile th db_th in
let goals = Db.goals db_th in
let tasks = List.rev (Task.split_theory th None None) in
let goals,proved = List.fold_left
(fun (acc,proved) t ->
let (g,p) = reimport_root_goal mth tname goals t in
(g::acc,proved && p))
([],true) tasks
in
mth.Model.goals <- List.rev goals;
(* TODO: what to do with remaining tasks in Db ???
for the moment they remain in the db, but they are not shown
*)
if proved then Helpers.set_theory_proved ~propagate:false mth;
(mth::acc,file_proved && proved))
([],true) theories
in
(* TODO: detecter d'eventuelles vieilles theories, qui seraient donc
dans [ths] mais pas dans [theories]
*)
mfile.Model.theories <- List.rev mths;
if file_proved then Helpers.set_file_verified mfile
with e ->
eprintf "@[Error while reading file@ '%s':@ %a@.@]" fn
Exn_printer.exn_printer e;
exit 1
)
files_in_db
let reload_file mf =
eprintf "[Reload] file '%s'@." mf.file_name;
try
let theories = read_file mf.file_name in
let old_theories = List.fold_left
(fun acc t -> Util.Mstr.add t.theory_name t acc)
Util.Mstr.empty
mf.theories
in
let mths =
List.fold_left
(fun acc (_,tname,th) ->
eprintf "[Reload] theory '%s'@."tname;
let mth =
try
let mth = Util.Mstr.find tname old_theories in
mth.theory <- Some th;
mth
with Not_found ->
raw_add_theory mf (Some th) tname
in
(*
let goals = Db.goals db_th in
let tasks = List.rev (Task.split_theory th None None) in
let goals,proved = List.fold_left
(fun (acc,proved) t ->
let (g,p) = reimport_root_goal mth tname goals t in
(g::acc,proved && p))
([],true) tasks
in
mth.Model.goals <- List.rev goals;
*) *)
(* TODO: what to do with remaining old theories?
for the moment they remain in the session
*)
check_theory_proved mth;
mth::acc
)
[] theories
in
(* TODO: detecter d'eventuelles vieilles theories, qui seraient donc
dans [old_theories] mais pas dans [theories]
*)
mf.theories <- List.rev mths;
check_file_verified mf
with e ->
eprintf "@[Error while reading file@ '%s':@ %a@.@]" mf.file_name
Exn_printer.exn_printer e;
exit 1
(* reloads all files *)
let reload_all () = List.iter reload_file !all_files
(****************************) (****************************)
(* session opening *) (* session opening *)
...@@ -1058,18 +1059,17 @@ let load_session ~env ~provers xml = ...@@ -1058,18 +1059,17 @@ let load_session ~env ~provers xml =
eprintf "Session.load_session: unexpected element '%s'@." s; eprintf "Session.load_session: unexpected element '%s'@." s;
assert false assert false
let db_file = ref None let db_filename = "why3session.xml"
let open_session ~env ~provers ~init ~notify file = let open_session ~env ~provers ~init ~notify dir =
match !db_file with match !current_env with
| None -> | None ->
init_fun := init; notify_fun := notify; init_fun := init; notify_fun := notify;
db_file := Some file; project_dir := dir; current_env := Some env;
begin try begin try
let xml = Xml.from_file file in let xml = Xml.from_file (Filename.concat dir db_filename) in
load_session ~env ~provers xml; load_session ~env ~provers xml;
(* TODO reload the files *) reload_all ()
()
with with
| Sys_error _ -> | Sys_error _ ->
(* xml does not exist yet *) (* xml does not exist yet *)
...@@ -1083,8 +1083,8 @@ let open_session ~env ~provers ~init ~notify file = ...@@ -1083,8 +1083,8 @@ let open_session ~env ~provers ~init ~notify file =
assert false assert false
let save_session () = let save_session () =
match !db_file with match !current_env with
| Some f -> save f | Some _ -> save (Filename.concat !project_dir db_filename)
| None -> | None ->
eprintf "Session.save_session: no session opened@."; eprintf "Session.save_session: no session opened@.";
assert false assert false
...@@ -1105,11 +1105,6 @@ let redo_external_proof g a = ...@@ -1105,11 +1105,6 @@ let redo_external_proof g a =
let p = a.prover in let p = a.prover in
let callback result = let callback result =
set_proof_state ~obsolete:false a result; set_proof_state ~obsolete:false a result;
match result with
| Done r ->
if r.Call_provers.pr_answer = Call_provers.Valid then
set_proved ~propagate:true a.proof_goal
| _ -> ()
in in
let old = if a.edited_as = "" then None else let old = if a.edited_as = "" then None else
begin begin
...@@ -1364,11 +1359,10 @@ let edit_proof ~default_editor ~project_dir a = ...@@ -1364,11 +1359,10 @@ let edit_proof ~default_editor ~project_dir a =
file file
| f -> f | f -> f
in in
let old_status = a.proof_state in
let callback res = let callback res =
match res with match res with
| Done _ -> | Done _ ->
set_proof_state ~obsolete:false a old_status set_proof_state ~obsolete:false a Undone
| _ -> | _ ->
set_proof_state ~obsolete:false a res set_proof_state ~obsolete:false a res
in in
......
...@@ -20,6 +20,7 @@ ...@@ -20,6 +20,7 @@
open Why open Why
(** {Prover's data} *)
type prover_data = private type prover_data = private
{ prover_id : string; { prover_id : string;
prover_name : string; prover_name : string;
...@@ -29,18 +30,24 @@ type prover_data = private ...@@ -29,18 +30,24 @@ type prover_data = private
driver : Driver.driver; driver : Driver.driver;
mutable editor : string; mutable editor : string;
} }
(** record of necessary data for a given external prover *)
val get_prover_data : val get_prover_data :
Env.env -> Util.Mstr.key -> Whyconf.config_prover -> Env.env -> Util.Mstr.key -> Whyconf.config_prover ->
prover_data Util.Mstr.t -> prover_data Util.Mstr.t prover_data Util.Mstr.t -> prover_data Util.Mstr.t
(** loads all provers from the current configuration *)
(* transformations *) (** {Transformation's data} *)
type transformation_data type transformation_data
(** record data for transformations *)
val transformation_id : transformation_data -> string val transformation_id : transformation_data -> string
(** Why3 name of a transformation *)
val lookup_transformation : Env.env -> string -> transformation_data val lookup_transformation : Env.env -> string -> transformation_data
(** returns a transformation from its Why3 name *)
(** {Proof attempts} *)
type proof_attempt_status = private type proof_attempt_status = private
| Undone | Undone
| Scheduled (** external proof attempt is scheduled *) | Scheduled (** external proof attempt is scheduled *)
...@@ -48,24 +55,55 @@ type proof_attempt_status = private ...@@ -48,24 +55,55 @@ type proof_attempt_status = private
| Done of Call_provers.prover_result (** external proof done *) | Done of Call_provers.prover_result (** external proof done *)
| InternalFailure of exn (** external proof aborted by internal error *) | InternalFailure of exn (** external proof aborted by internal error *)
(** {Observers signature} *)
module type OBSERVER = sig module type OBSERVER = sig
type key type key
(** type key allowing to uniquely identify an element of
of session: a goal, a transformation, a proof attempt,
a theory or a file. See type [any] below *)
val create: ?parent:key -> unit -> key val create: ?parent:key -> unit -> key
(** returns a fresh key, a new child of the given parent if any *)
val remove: key -> unit val remove: key -> unit
(** removes a key *)
val timeout: ms:int -> (unit -> bool) -> unit val timeout: ms:int -> (unit -> bool) -> unit
(** a handler for functions that must be called after a given time
elapsed, in milliseconds. When the given function returns
true, it must be rescheduled *)
val idle: (unit -> bool) -> unit val idle: (unit -> bool) -> unit
(** a handler for a delayed function, that can be called when
there is nothing else to do. When the given function returns
true, it must be rescheduled *)
end end
(** {Main functor} *)
module Make(O: OBSERVER) : sig module Make(O: OBSERVER) : sig
(*****************************) (** {static state of a session} *)
(* *)
(* static state of a session *) type goal
(* *) (** a goal *)