Attention une mise à jour du serveur va être effectuée le vendredi 16 avril entre 12h et 12h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit b137be24 authored by MARCHE Claude's avatar MARCHE Claude

[replayer] replay now fails if new goals are added in the session

grants a long-standing feature wish by Andrei
parent 34d3b31e
......@@ -884,7 +884,7 @@ let sched =
else
S.create_session project_dir
in
let env,(_:bool) =
let env,(_:bool),(_:bool) =
M.update_session ~allow_obsolete:true session gconfig.env
gconfig.Gconfig.config
in
......@@ -1921,7 +1921,7 @@ let reload () =
gconfig.env <- Env.create_env loadpath;
(** reload the session *)
let old_session = (env_session()).S.session in
let new_env_session,(_:bool) =
let new_env_session,(_:bool),(_:bool) =
M.update_session ~allow_obsolete:true old_session gconfig.env
gconfig.Gconfig.config
in
......
......@@ -1761,6 +1761,7 @@ end
(**********************************)
let found_obsolete = ref false
let found_missed_goals = ref false
let merge_proof ~keygen obsolete to_goal _ from_proof =
let obsolete = obsolete || from_proof.proof_obsolete in
......@@ -2006,12 +2007,14 @@ and merge_trans ~keygen ~theories env to_goal _ from_transf =
let associated =
dprintf debug "[Info] associate_subgoals, shape_version = %d@\n"
env.session.session_shape_version;
AssoGoals.associate from_transf.transf_goals to_transf.transf_goals in
AssoGoals.associate from_transf.transf_goals to_transf.transf_goals
in
List.iter (function
| (to_goal, Some (from_goal, obsolete)) ->
merge_any_goal ~keygen ~theories env obsolete from_goal to_goal
| (_, None) -> ()
) associated
| (to_goal, Some (from_goal, obsolete)) ->
merge_any_goal ~keygen ~theories env obsolete from_goal to_goal
| (_, None) ->
found_missed_goals := true)
associated
with Exit -> ()
(** convert the ident from the old task to the ident at the same
......@@ -2071,6 +2074,7 @@ let merge_theory
if release then release_sub_tasks to_goal
with
| Not_found when allow_obsolete ->
found_missed_goals := true;
if release then release_sub_tasks to_goal
| Not_found -> raise OutdatedSession
) to_th.theory_goals
......@@ -2141,6 +2145,7 @@ let update_session
}
in
found_obsolete := false;
found_missed_goals := false;
let files =
PHstr.fold (fun _ old_file acc ->
dprintf debug "[Load] file '%s'@\n" old_file.file_name;
......@@ -2175,7 +2180,7 @@ let update_session
in
assert (new_env_session.session.session_shape_version
= Termcode.current_shape_version);
new_env_session, obsolete
new_env_session, obsolete, !found_missed_goals
(** Copy/Paste *)
......
......@@ -229,7 +229,7 @@ val update_session :
?release:bool (* default false *) ->
keygen:'a keygen ->
allow_obsolete:bool -> 'b session ->
Env.env -> Whyconf.config -> 'a env_session * bool
Env.env -> Whyconf.config -> 'a env_session * bool * bool
(** reload the given session with the given environnement :
- the files are reloaded
- apply again the transformation
......@@ -241,6 +241,8 @@ val update_session :
otherwise the exception {!OutdatedSession} is raised.
If the session was obsolete is indicated by
the second result.
If the merge generated new unpaired goals is indicated by
the third result.
raises [Failure msg] if the database file cannot be read correctly
......
......@@ -336,7 +336,7 @@ let schedule_delayed_action t callback =
let update_session ?release ~allow_obsolete old_session env whyconf =
O.reset ();
let (env_session,_) as res =
let (env_session,_,_) as res =
update_session ?release
~keygen:O.create ~allow_obsolete old_session env whyconf in
dprintf debug "Init_session@\n";
......
......@@ -116,7 +116,7 @@ module Make(O: OBSERVER) : sig
allow_obsolete:bool ->
'key session ->
Env.env -> Whyconf.config ->
O.key env_session * bool
O.key env_session * bool * bool
(**
Same as {!Session.update_session} except initialization is done.
*)
......
......@@ -326,7 +326,7 @@ let same_result r1 r2 =
| Call_provers.Failure _, Call_provers.Failure _-> true
| _ -> false
let add_to_check_no_smoke config found_obs env_session sched =
let add_to_check_no_smoke config some_merge_miss found_obs env_session sched =
let session = env_session.S.session in
let callback report =
Debug.dprintf debug "@.";
......@@ -347,7 +347,7 @@ let add_to_check_no_smoke config found_obs env_session sched =
S.save_session config session;
Debug.dprintf debug " done@." in
printf " %d/%d " n m;
if report = [] then
if report = [] && not some_merge_miss then
begin
printf "(replay OK%s%s)@."
(if found_obs then ", obsolete session" else "")
......@@ -360,7 +360,8 @@ let add_to_check_no_smoke config found_obs env_session sched =
else
let report = List.rev report in
begin
printf "(replay failed)@.";
printf "(replay failed%s)@."
(if some_merge_miss then ", with some merge miss" else "");
List.iter print_report report;
eprintf "Replay failed.@.";
if !opt_force then save ();
......@@ -400,10 +401,13 @@ let add_to_check_smoke env_session sched =
in
M.check_all ~release:true ~callback env_session sched
let add_to_check config found_obs =
let add_to_check config some_merge_miss found_obs =
match !opt_smoke with
| SD_None -> add_to_check_no_smoke config found_obs;
| _ -> assert (not found_obs); add_to_check_smoke
| SD_None -> add_to_check_no_smoke config some_merge_miss found_obs;
| _ ->
assert (not some_merge_miss);
assert (not found_obs);
add_to_check_smoke
let transform_smoke env_session =
let trans tr_name s =
......@@ -447,13 +451,12 @@ let () =
try
Debug.dprintf debug "Opening session...@?";
O.verbose := Debug.test_flag debug;
let env_session,found_obs =
let env_session,found_obs,some_merge_miss =
let session = S.read_session project_dir in
M.update_session ~allow_obsolete:true session env config
in
Debug.dprintf debug " done.@.";
if !opt_obsolete_only && not found_obs
(* useless since too early: && not found_uninstalled_prover *)
then
begin
eprintf "Session is not obsolete, hence not replayed@.";
......@@ -466,7 +469,8 @@ let () =
M.init (Whyconf.running_provers_max (Whyconf.get_main config))
in
if found_obs then eprintf "[Warning] session is obsolete@.";
add_to_check config found_obs env_session sched;
if some_merge_miss then eprintf "[Warning] some goals were missed during merge@.";
add_to_check config some_merge_miss found_obs env_session sched;
main_loop ();
eprintf "main replayer loop exited unexpectedly@.";
exit 1
......
......@@ -114,7 +114,7 @@ let get_to_prover pk session config =
exception NoAlt
let run_one ~action env config filters pk fname =
let env_session,_ =
let env_session,_,_ =
read_update_session ~allow_obsolete:!opt_force_obsolete env config fname in
let to_prover = get_to_prover pk env_session.session config in
let s = Stack.create () in
......
......@@ -49,9 +49,9 @@ val read_env_spec : unit -> Env.env * Whyconf.config * bool
(** read_simple_spec also *)
val read_update_session :
allow_obsolete:bool ->
Why3.Env.env ->
Why3.Whyconf.config -> string -> unit Why3.Session.env_session * bool
allow_obsolete:bool -> Why3.Env.env ->
Why3.Whyconf.config -> string ->
unit Why3.Session.env_session * bool * bool
(** {2 Spec for filtering } *)
type filter_prover
......
......@@ -53,7 +53,7 @@ let keygen ?parent:_ _ = ()
let fname_printer = Ident.create_ident_printer []
let run_one env config filters dir fname =
let env_session,_ =
let env_session,_,_ =
read_update_session ~allow_obsolete:!opt_force_obsolete env config fname in
iter_session (fun file ->
let fname = Filename.basename file.file_name in
......
......@@ -58,7 +58,7 @@ let rec interactive to_remove =
| _ -> interactive to_remove
let run_one env config filters fname =
let env_session,_ =
let env_session,_,_ =
read_update_session ~allow_obsolete:!opt_force_obsolete env config fname in
session_iter_proof_attempt_by_filter filters
(fun pr ->
......
......@@ -194,15 +194,17 @@ let is_successful env = (** means all goals proved*)
let run_one sched env config filters interactive_provers fname =
let env_session, out_of_sync =
let env_session, out_of_sync, missed =
read_update_session ~allow_obsolete:(!opt_outofsync <> Outofsync_none)
env config fname in
if out_of_sync then
dprintf verbose "@[From@ file@ %s:out of sync@]@." fname;
dprintf verbose "@[From@ file@ %s: out of sync@]@." fname;
if missed then
dprintf verbose "@[From@ file@ %s: merge missed new goals@]@." fname;
let todo = Todo.create () (fun () _ -> ())
(fun () ->
if !opt_save <> Save_none &&
(not out_of_sync
(not (out_of_sync || missed)
|| !opt_outofsync = Outofsync_usual
|| (!opt_outofsync = Outofsync_success
&& is_successful env_session ))
......
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