Commit c67866e4 authored by MARCHE Claude's avatar MARCHE Claude

replayer saves the session when it is outdated and successful

parent 43ec9976
......@@ -575,10 +575,12 @@ let () =
let () =
try
eprintf "[Info] Opening session...@\n@[<v 2> ";
M.open_session ~allow_obsolete:true
~env:gconfig.env
~config:gconfig.Gconfig.config
~init ~notify project_dir;
let (_:bool) =
M.open_session ~allow_obsolete:true
~env:gconfig.env
~config:gconfig.Gconfig.config
~init ~notify project_dir
in
M.maximum_running_proofs := gconfig.max_running_processes;
eprintf "@]@\n[Info] Opening session: done@."
with e ->
......@@ -1208,7 +1210,8 @@ let reload () =
try
erase_color_loc source_view;
current_file := "";
M.reload_all true
let (_:bool) = M.reload_all true in
()
with
| e ->
let e = match e with
......
......@@ -313,8 +313,12 @@ let print_report (g,p,r) =
let () =
try
eprintf "Opening session...@?";
M.open_session ~allow_obsolete:false
~env ~config ~init ~notify project_dir;
let found_obs =
M.open_session ~allow_obsolete:true
~env ~config ~init ~notify project_dir
in
if found_obs then
eprintf "[Warning] session is obsolete@.";
M.maximum_running_proofs :=
Whyconf.running_provers_max (Whyconf.get_main config);
eprintf " done@.";
......@@ -322,15 +326,28 @@ let () =
let files,n,m =
List.fold_left file_statistics ([],0,0) (M.get_all_files ())
in
printf " %d/%d@." n m ;
match report with
| [] ->
if found_obs then
if n=m then
printf " %d/%d (replay OK, all proved: obsolete session updated)@." n m
else
printf " %d/%d (replay OK, but not all proved: obsolete session NOT updated)@." n m
else
printf " %d/%d@." n m ;
if !opt_stats && n<m then print_statistics files;
eprintf "Everything OK.@.";
eprintf "Everything replayed OK.@.";
if found_obs && n=m then
begin
eprintf "Updating obsolete session...@?";
M.save_session ();
eprintf " done@."
end;
exit 0
| _ ->
printf " %d/%d (replay failed)@." n m ;
List.iter print_report report;
eprintf "Check failed.@.";
eprintf "Replay failed.@.";
exit 1
in
M.check_all ~callback;
......
......@@ -1138,6 +1138,7 @@ and reload_trans _goal_obsolete goal _ tr =
apply_transformation ~callback tr.transf (get_task goal)
exception OutdatedSession
let found_obsolete = ref false
(* reloads the task [t] in theory mth (named tname) *)
let reload_root_goal ~allow_obsolete mth tname old_goals t : goal =
......@@ -1154,7 +1155,10 @@ let reload_root_goal ~allow_obsolete mth tname old_goals t : goal =
if goal_obsolete then
begin
eprintf "[Reload] Goal %s.%s has changed@." tname gname;
if not allow_obsolete then raise OutdatedSession
if allow_obsolete then
found_obsolete := true
else
raise OutdatedSession
end;
reload_any_goal (Parent_theory mth) id gname sum "" t old_goal goal_obsolete
......@@ -1213,7 +1217,9 @@ let reload_all allow_obsolete =
in
all_files := [];
O.reset ();
List.iter (fun (mf,ths) -> reload_file ~allow_obsolete mf ths) all_theories
found_obsolete := false;
List.iter (fun (mf,ths) -> reload_file ~allow_obsolete mf ths) all_theories;
!found_obsolete
(****************************)
(* session opening *)
......@@ -1418,12 +1424,11 @@ let open_session ~allow_obsolete ~env ~config ~init ~notify dir =
load_session ~env xml;
reload_all allow_obsolete
with
| Sys_error _ ->
| Sys_error msg ->
(* xml does not exist yet *)
()
failwith ("Open session: sys error " ^ msg)
| Xml.Parse_error s ->
Format.eprintf "XML database corrupted, ignored (%s)@." s;
()
failwith ("Open session: XML database corrupted (%s)@." ^ s)
end
| _ ->
eprintf "Session.open_session: session already opened@.";
......
......@@ -177,7 +177,7 @@ module Make(O: OBSERVER) : sig
config:Whyconf.config ->
init:(O.key -> any -> unit) ->
notify:(any -> unit) ->
string -> unit
string -> bool
(** starts a new proof session, using directory given as argument
this reloads the previous session database if any.
......@@ -192,6 +192,12 @@ module Make(O: OBSERVER) : sig
raises [OutdatedSession] if [allow_obsolete] is false and any obsolete
data for a goal is found in the session database
raises [Failure msg] if the database file cannot be read correctly
returns true if some obsolete goal was found (and
[allow_obsolete] is true), false otherwise
*)
val get_provers : unit -> prover_data Util.Mstr.t
......@@ -259,7 +265,7 @@ module Make(O: OBSERVER) : sig
which are triples (goal name, prover, report)
*)
val reload_all: bool -> unit
val reload_all: bool -> bool
(** reloads all the files
If for one of the file, the parsing or typing fails, then
the complete old session state is kept, and an exception
......@@ -267,7 +273,10 @@ module Make(O: OBSERVER) : sig
raises [OutdatedSession] if [allow_obsolete] is false and any obsolete
data for a goal is found in the session database
returns true if some obsolete goal was found (and
[allow_obsolete] is true), false otherwise
*)
val remove_proof_attempt : proof_attempt -> unit
......
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