Commit 59574d2c authored by Andrei Paskevich's avatar Andrei Paskevich

why3replayer: release tasks as soon as they are checked

parent 6b8c6a97
......@@ -714,17 +714,24 @@ let check_goal_and_children eS eT todo g =
goal_iter_proof_attempt (check_external_proof eS eT todo) g
*)
let rec goal_iter_proof_attempt_with_release ~release f g =
let iter g = goal_iter_proof_attempt_with_release ~release f g in
PHprover.iter (fun _ a -> f a) g.goal_external_proofs;
PHstr.iter (fun _ t -> List.iter iter t.transf_goals) g.goal_transformations;
Mmetas_args.iter (fun _ t -> iter t.metas_goal) g.goal_metas;
if release then release_task g
let check_all ?(release=false) eS eT ~callback =
dprintf debug "[Sched] check all@.%a@." print_session eS.session;
let todo = Todo.create [] push_report callback in
let todo = Todo.create [] push_report callback in
Todo.start todo;
let check_top_goal g =
goal_iter_proof_attempt (check_external_proof eS eT todo) g;
if release then release_sub_tasks g
let check a = check_external_proof eS eT todo a in
goal_iter_proof_attempt_with_release ~release check g
in
PHstr.iter (fun _ file ->
List.iter (fun t ->
List.iter check_top_goal t.theory_goals)
List.iter (fun t ->
List.iter check_top_goal t.theory_goals)
file.file_theories)
eS.session.session_files;
Todo.stop todo
......
......@@ -363,7 +363,7 @@ let add_to_check_no_smoke config found_obs env_session sched =
exit 1
end
in
M.check_all ~callback env_session sched
M.check_all ~release:true ~callback env_session sched
let add_to_check_smoke env_session sched =
let callback report =
......@@ -387,7 +387,7 @@ let add_to_check_smoke env_session sched =
exit 1
end
in
M.check_all ~callback env_session sched
M.check_all ~release:true ~callback env_session sched
let add_to_check config found_obs =
match !opt_smoke with
......
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