Commit 5fc52562 authored by MARCHE Claude's avatar MARCHE Claude

replay aborts if session data is outdated

parent 13378fb6
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/check-builtin/real/why3session.xml">
<why3session name="check-builtin/real/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.2pl1"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.13.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../real.why" verified="true" expanded="true">
<theory name="Test" verified="true" expanded="true">
<goal name="G1" sum="809c4674f0b6c8c26230b31c88c93205" proved="true" expanded="true">
<goal name="G1" sum="832ddb9ca6d4d32f25e03098a3607b6b" proved="true" expanded="true" shape="ainfix =ainfix *c5.5c10.c55.">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="yices" timelimit="10" edited="" obsolete="false">
<proof prover="yices" timelimit="10" edited="" obsolete="true">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<proof prover="spass" timelimit="10" edited="" obsolete="true">
<result status="timeout" time="10.07"/>
</proof>
</goal>
<goal name="G2" sum="bdcf97e1ee5d72c09c49e8205dc2b03d" proved="true" expanded="true">
<goal name="G2" sum="efe077a578905ccd7321f78fa8952077" proved="true" expanded="true" shape="ainfix =ainfix /c9.c3.c3.">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.03"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<proof prover="spass" timelimit="10" edited="" obsolete="true">
<result status="timeout" time="10.08"/>
</proof>
</goal>
<goal name="G3" sum="6df8ed98cc9864be991675ea6ab11da1" proved="true" expanded="true">
<goal name="G3" sum="1885fdced1e38f18cc908dd034c5266e" proved="true" expanded="true" shape="ainfix =ainvc5.c0.2">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<proof prover="spass" timelimit="10" edited="" obsolete="true">
<result status="timeout" time="10.06"/>
</proof>
</goal>
......
......@@ -10,9 +10,9 @@ DATE=`date --utc +%Y-%m-%d`
SUBJECT="Why3 nightly bench:"
notify() {
mail -s "$SUBJECT" why3-commits@lists.gforge.inria.fr < $REPORT
# mail -s "$SUBJECT" why3-commits@lists.gforge.inria.fr < $REPORT
# mail -s "$SUBJECT" Claude.Marche@inria.fr < $REPORT
# cat $REPORT
cat $REPORT
exit 0
}
......
......@@ -575,8 +575,8 @@ let () =
let () =
try
eprintf "[Info] Opening session...@\n@[<v 2> ";
M.open_session ~env:gconfig.env
(* ~provers:gconfig.provers *)
M.open_session ~allow_obsolete:true
~env:gconfig.env
~config:gconfig.Gconfig.config
~init ~notify project_dir;
M.maximum_running_proofs := gconfig.max_running_processes;
......@@ -1208,7 +1208,7 @@ let reload () =
try
erase_color_loc source_view;
current_file := "";
M.reload_all ()
M.reload_all true
with
| e ->
let e = match e with
......
......@@ -313,7 +313,8 @@ let print_report (g,p,r) =
let () =
try
eprintf "Opening session...@?";
M.open_session ~env ~config ~init ~notify project_dir;
M.open_session ~allow_obsolete:false
~env ~config ~init ~notify project_dir;
M.maximum_running_proofs :=
Whyconf.running_provers_max (Whyconf.get_main config);
eprintf " done@.";
......@@ -335,11 +336,18 @@ let () =
M.check_all ~callback;
try main_loop ()
with Exit -> eprintf "main replayer exited unexpectedly@."
with e when not (Debug.test_flag Debug.stack_trace) ->
eprintf "Error while opening session with database '%s' : %a@." project_dir
Exn_printer.exn_printer e;
eprintf "Aborting...@.";
exit 1
with
| M.OutdatedSession ->
eprintf "The session database '%s' is outdated, cannot replay@."
project_dir;
eprintf "Aborting...@.";
exit 1
| e when not (Debug.test_flag Debug.stack_trace) ->
eprintf "Error while opening session with database '%s' : %a@."
project_dir
Exn_printer.exn_printer e;
eprintf "Aborting...@.";
exit 1
(*
......
......@@ -1107,7 +1107,8 @@ let reload_proof obsolete goal pid old_a =
in
!notify_fun (Goal a.proof_goal)
let rec reload_any_goal parent gid gname sum shape t old_goal goal_obsolete =
let rec reload_any_goal parent gid gname sum shape t
old_goal goal_obsolete =
let info = get_explanation gid (Task.task_goal_fmla t) in
let exp = match old_goal with None -> true | Some g -> g.goal_expanded in
let goal = raw_add_goal parent gname info sum shape (Some t) exp in
......@@ -1123,7 +1124,7 @@ let rec reload_any_goal parent gid gname sum shape t old_goal goal_obsolete =
goal
and reload_trans _goal_obsolete goal _ tr =
and reload_trans _goal_obsolete goal _ tr =
let trname = tr.transf.transformation_name in
let gname = goal.goal_name in
eprintf "[Reload] transformation %s for goal %s @\n" trname gname;
......@@ -1143,9 +1144,10 @@ and reload_trans _goal_obsolete goal _ tr =
in
apply_transformation ~callback tr.transf (get_task goal)
exception OutdatedSession
(* reloads the task [t] in theory mth (named tname) *)
let reload_root_goal mth tname old_goals t : goal =
let reload_root_goal ~allow_obsolete mth tname old_goals t : goal =
let id = (Task.task_goal t).Decl.pr_name in
let gname = id.Ident.id_string in
let sum = task_checksum t in
......@@ -1157,11 +1159,14 @@ let reload_root_goal mth tname old_goals t : goal =
with Not_found -> (None,false)
in
if goal_obsolete then
eprintf "Goal %s.%s has changed@." tname gname;
begin
eprintf "[Reload] Goal %s.%s has changed@." tname gname;
if not allow_obsolete then raise OutdatedSession
end;
reload_any_goal (Parent_theory mth) id gname sum "" t old_goal goal_obsolete
(* reloads a theory *)
let reload_theory mfile old_theories (_,tname,th) =
let reload_theory ~allow_obsolete mfile old_theories (_,tname,th) =
eprintf "[Reload] theory '%s'@\n"tname;
let tasks = List.rev (Task.split_theory th None None) in
let old_goals, old_exp =
......@@ -1178,7 +1183,7 @@ let reload_theory mfile old_theories (_,tname,th) =
!notify_fun (Theory mth);
let new_goals = List.fold_left
(fun acc t ->
let g = reload_root_goal mth tname goalsmap t in
let g = reload_root_goal ~allow_obsolete mth tname goalsmap t in
g::acc)
[] tasks
in
......@@ -1188,7 +1193,7 @@ let reload_theory mfile old_theories (_,tname,th) =
(* reloads a file *)
let reload_file mf theories =
let reload_file ~allow_obsolete mf theories =
let new_mf = raw_add_file mf.file_name mf.file_expanded in
let old_theories = List.fold_left
(fun acc t -> Util.Mstr.add t.theory_name t acc)
......@@ -1197,7 +1202,7 @@ let reload_file mf theories =
in
!notify_fun (File new_mf);
let mths = List.fold_left
(fun acc th -> reload_theory new_mf old_theories th :: acc)
(fun acc th -> reload_theory ~allow_obsolete new_mf old_theories th :: acc)
[] theories
in
new_mf.theories <- List.rev mths;
......@@ -1205,7 +1210,7 @@ let reload_file mf theories =
(* reloads all files *)
let reload_all () =
let reload_all allow_obsolete =
let files = !all_files in
let all_theories =
List.map (fun mf ->
......@@ -1215,7 +1220,7 @@ let reload_all () =
in
all_files := [];
O.reset ();
List.iter (fun (mf,ths) -> reload_file mf ths) all_theories
List.iter (fun (mf,ths) -> reload_file ~allow_obsolete mf ths) all_theories
(****************************)
(* session opening *)
......@@ -1407,7 +1412,7 @@ let load_session ~env xml =
let db_filename = "why3session.xml"
let open_session ~env ~config ~init ~notify dir =
let open_session ~allow_obsolete ~env ~config ~init ~notify dir =
match !current_env with
| None ->
init_fun := init; notify_fun := notify;
......@@ -1418,7 +1423,7 @@ let open_session ~env ~config ~init ~notify dir =
begin try
let xml = Xml.from_file (Filename.concat dir db_filename) in
load_session ~env xml;
reload_all ()
reload_all allow_obsolete
with
| Sys_error _ ->
(* xml does not exist yet *)
......
......@@ -169,11 +169,11 @@ module Make(O: OBSERVER) : sig
(** {2 Save and load a state} *)
exception OutdatedSession
val open_session :
allow_obsolete:bool ->
env:Env.env ->
(*
provers:prover_data Util.Mstr.t ->
*)
config:Whyconf.config ->
init:(O.key -> any -> unit) ->
notify:(any -> unit) ->
......@@ -190,6 +190,8 @@ module Make(O: OBSERVER) : sig
the [init] function is a function that will be called at each
creation of element of the state
raises [OutdatedSession] if [allow_obsolete] is false and any obsolete
data for a goal is found in the session database
*)
val get_provers : unit -> prover_data Util.Mstr.t
......@@ -257,11 +259,15 @@ module Make(O: OBSERVER) : sig
which are triples (goal name, prover, report)
*)
val reload_all: unit -> unit
val reload_all: bool -> unit
(** 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
is raised
raises [OutdatedSession] if [allow_obsolete] is false and any obsolete
data for a goal is found in the session database
*)
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