Commit 65a92cec authored by MARCHE Claude's avatar MARCHE Claude

replayer finally does something

parent 876d26e1
......@@ -567,7 +567,8 @@ let replay_obsolete_proofs () =
List.iter
(fun row ->
let a = get_any row in
M.replay ~context_unproved_goals_only:!context_unproved_goals_only a)
M.replay ~obsolete_only:true
~context_unproved_goals_only:!context_unproved_goals_only a)
goals_view#selection#get_selected_rows
......
......@@ -119,7 +119,7 @@ let main_loop () =
begin
let ms =
match !timeout_handler with
| None -> 0.1
| None -> raise Exit
| Some(ms,_) -> ms
in
usleep (ms -. time)
......@@ -223,8 +223,14 @@ let main () =
M.maximum_running_proofs :=
Whyconf.running_provers_max (Whyconf.get_main config);
eprintf " done@.";
(* for each file f *) let _ = M.replay (* f *) in
main_loop ()
let files = M.get_all_files () in
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;
try main_loop ()
with Exit -> eprintf "Everything done@."
with e ->
eprintf "Error while opening session with database '%s'@." project_dir;
eprintf "Aborting...@.";
......
......@@ -1217,40 +1217,40 @@ let proof_successful a =
| Done { Call_provers.pr_answer = Call_provers.Valid } -> true
| _ -> false
let rec replay_on_goal_or_children ~context_unproved_goals_only g =
let rec replay_on_goal_or_children ~obsolete_only ~context_unproved_goals_only g =
Hashtbl.iter
(fun _ a ->
if a.proof_obsolete then
if not obsolete_only || a.proof_obsolete then
if not context_unproved_goals_only || proof_successful a
then redo_external_proof g a)
g.external_proofs;
Hashtbl.iter
(fun _ t ->
List.iter
(replay_on_goal_or_children ~context_unproved_goals_only)
(replay_on_goal_or_children ~obsolete_only ~context_unproved_goals_only)
t.subgoals)
g.transformations
let replay ~context_unproved_goals_only a =
let replay ~obsolete_only ~context_unproved_goals_only a =
match a with
| Goal g ->
replay_on_goal_or_children ~context_unproved_goals_only g
replay_on_goal_or_children ~obsolete_only ~context_unproved_goals_only g
| Theory th ->
List.iter
(replay_on_goal_or_children ~context_unproved_goals_only)
(replay_on_goal_or_children ~obsolete_only ~context_unproved_goals_only)
th.goals
| File file ->
List.iter
(fun th ->
List.iter
(replay_on_goal_or_children ~context_unproved_goals_only)
(replay_on_goal_or_children ~obsolete_only ~context_unproved_goals_only)
th.goals)
file.theories
| Proof_attempt a ->
replay_on_goal_or_children ~context_unproved_goals_only a.proof_goal
replay_on_goal_or_children ~obsolete_only ~context_unproved_goals_only a.proof_goal
| Transformation tr ->
List.iter
(replay_on_goal_or_children ~context_unproved_goals_only)
(replay_on_goal_or_children ~obsolete_only ~context_unproved_goals_only)
tr.subgoals
......
......@@ -208,8 +208,13 @@ module Make(O: OBSERVER) : sig
val edit_proof :
default_editor:string -> project_dir:string -> proof_attempt -> unit
val replay : context_unproved_goals_only:bool -> any -> unit
(** [replay a] reruns all valid but obsolete proofs under [a] *)
val replay :
obsolete_only:bool ->
context_unproved_goals_only:bool -> any -> unit
(** [replay a] reruns proofs under [a]
if obsolete_only is set then does not rerun non-obsolete proofs
if context_unproved_goals_only is set then reruns only proofs with result was 'valid'
*)
(*
TODO
......
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