Skip to content

GitLab

why3
why3
Commit c6dc4315 authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

Again, fixed mistakes related to the timelimit used 

when replaying proofs.
parent 66f56097
Hide whitespace changes
Inline Side-by-side
Showing with 79 additions and 81 deletions
src/driver/call_provers.ml
View file @ c6dc4315
......@@ -86,6 +86,8 @@ let print_prover_answer fmt = function
| Valid -> fprintf fmt "Valid"
| Invalid -> fprintf fmt "Invalid"
| Timeout -> fprintf fmt "Timeout"
| Unknown "" -> fprintf fmt "Unknown"
| Failure "" -> fprintf fmt "Failure"
| Unknown s -> fprintf fmt "Unknown: %s" s
| Failure s -> fprintf fmt "Failure: %s" s
| HighFailure -> fprintf fmt "HighFailure"
......
src/ide/replay.ml
View file @ c6dc4315
......@@ -210,19 +210,22 @@ end
module M = Session_scheduler.Make(O)
let print_result fmt
{Call_provers.pr_answer=ans; Call_provers.pr_output=out;
Call_provers.pr_time=_t} =
(*
{ Call_provers.pr_answer=ans;
Call_provers.pr_output=out;
Call_provers.pr_time=t } =
fprintf fmt "%a (%.1fs)" Call_provers.print_prover_answer ans t;
*)
(*
fprintf fmt "%a" Call_provers.print_prover_answer ans;
if ans == Call_provers.HighFailure then
fprintf fmt "@\nProver output:@\n%s@." out
*)
match ans with
| Call_provers.HighFailure ->
fprintf fmt "@\nProver output:@\n%s@." out
| _ -> ()
(*
fprintf fmt "[limit=%s@\nProver output:@\n%s@." out
*)
let main_loop = O.main_loop
(*
let model_index = Hashtbl.create 257
*)
let project_dir =
try
......@@ -262,14 +265,14 @@ let print_statistics files =
List.iter print_file (List.rev files)
let print_report (g,p,r) =
let print_report (g,p,t,r) =
printf " goal '%s', prover '%a': " g.Ident.id_string Whyconf.print_prover p;
match r with
| M.Result(new_res,old_res) ->
(* begin match !opt_smoke with *)
(* | Session.SD_None -> *)
printf "%a instead of %a@."
print_result new_res print_result old_res
printf "%a instead of %a (timelimit=%d)@."
print_result new_res print_result old_res t
(* | _ -> *)
(* printf "Smoke detected!!!@." *)
(* end *)
......@@ -298,9 +301,14 @@ let add_to_check_no_smoke config found_obs env_session sched =
S.PHstr.fold file_statistics
session.S.session_files ([],0,0)
in
let report = List.filter (function
| (_,_,M.Result(new_res,old_res)) ->not (same_result new_res old_res)
| _ -> true) report in
let report =
List.filter
(function
| (_,_,_,M.Result(new_res,old_res)) ->
not (same_result new_res old_res)
| _ -> true)
report
in
if report = [] then begin
if found_obs then
if n=m then
......@@ -338,12 +346,15 @@ session NOT updated)@." n m
let add_to_check_smoke env_session sched =
let callback report =
eprintf "@.";
let report = List.filter (function
| (_,_,M.Result({Call_provers.pr_answer = Call_provers.Valid} ,_))
-> true
| (_,_,M.No_former_result({Call_provers.pr_answer = Call_provers.Valid}))
-> true
| _ -> false) report in
let report =
List.filter
(function
| (_,_,_,M.Result({Call_provers.pr_answer = Call_provers.Valid} ,_))
-> true
| (_,_,_,M.No_former_result({Call_provers.pr_answer = Call_provers.Valid}))
-> true
| _ -> false) report
in
if report = [] then begin
eprintf "No smoke detected.@.";
exit 0
......@@ -376,26 +387,15 @@ let run_as_bench env_session =
M.init (Whyconf.running_provers_max (Whyconf.get_main config))
in
eprintf "Provers:@ ";
let provers =
let provers =
Whyconf.Mprover.fold
(fun _ p acc ->
(fun _ p acc ->
if p.Whyconf.interactive then acc else
begin
eprintf "%a@ " Whyconf.print_prover p.Whyconf.prover;
p.Whyconf.prover :: acc
end)
(Whyconf.get_provers env_session.Session.whyconf) []
(*
Session.PHprover.fold
(fun _ p acc ->
match p with
| None -> acc
| Some p ->
let p = p.Session.prover_config.Whyconf.prover in
eprintf "prover: %a@." Whyconf.print_prover p;
p :: acc)
env_session.Session.loaded_provers []
*)
in
eprintf "@.";
let callback () =
......@@ -405,8 +405,8 @@ let run_as_bench env_session =
exit 0
in
M.play_all env_session sched ~callback ~timelimit:2 provers;
main_loop ();
eprintf "main replayer (in bench mode) exited unexpectedly@.";
main_loop ();
eprintf "main replayer (in bench mode) exited unexpectedly@.";
exit 1
let () =
......@@ -433,8 +433,8 @@ let () =
(* M.smoke_detector := !opt_smoke; *)
eprintf " done.";
add_to_check config found_obs env_session sched;
main_loop ();
eprintf "main replayer exited unexpectedly@.";
main_loop ();
eprintf "main replayer exited unexpectedly@.";
exit 1
with
| S.OutdatedSession ->
......
src/session/session_scheduler.ml
View file @ c6dc4315
......@@ -272,7 +272,7 @@ let cancel_scheduled_proofs t =
callback (Undone Interrupted)
done
with
| Queue.Empty ->
| Queue.Empty ->
O.notify_timer_state 0 0 (List.length t.running_proofs)
......@@ -334,6 +334,15 @@ let rec find_loadable_prover eS prover =
end
| Some npc -> Some (prover,npc)
let adapt_timelimit a =
match a.proof_state with
| Done { Call_provers.pr_answer = Call_provers.Valid ;
Call_provers.pr_time = t } ->
let time = max a.proof_timelimit (1 + truncate (2.0 *. t)) in
set_timelimit time a;
time
| _ -> a.proof_timelimit
let run_external_proof eS eT ?callback a =
(** Perhaps this test, a.proof_archived, should be done somewhere else *)
......@@ -343,11 +352,11 @@ let run_external_proof eS eT ?callback a =
(* info_window `ERROR "Proof already in progress" *)
let ap = a.proof_prover in
match find_loadable_prover eS a.proof_prover with
| None ->
| None ->
Debug.dprintf debug
"[Info] Can't redo an external proof since the prover %a is not loaded@."
Whyconf.print_prover a.proof_prover;
Util.apply_option2 () callback a a.proof_state
Util.apply_option2 () callback a a.proof_state
| Some (nap,npc) ->
(* eprintf "prover %a on goal %s@." *)
(* Whyconf.print_prover a.proof_prover a.proof_parent.goal_name.Ident.id_string; *)
......@@ -355,11 +364,11 @@ let run_external_proof eS eT ?callback a =
try
if nap == ap then raise Not_found;
let np_a = PHprover.find g.goal_external_proofs nap in
if O.replace_prover np_a a then
if O.replace_prover np_a a then
begin
(** The notification will be done by the new proof_attempt *)
O.remove np_a.proof_key;
raise Not_found
raise Not_found
end
with Not_found ->
(** replace [a] by a new_proof attempt if [a.proof_prover] was not
......@@ -369,7 +378,7 @@ let run_external_proof eS eT ?callback a =
let a = copy_external_proof
~notify ~keygen:O.create ~prover:nap ~env_session:eS a in
O.init a.proof_key (Proof_attempt a);
a
a
in
if a.proof_edited_as = None &&
npc.prover_config.Whyconf.interactive then
......@@ -378,17 +387,10 @@ let run_external_proof eS eT ?callback a =
(Undone Unedited) a;
Util.apply_option2 () callback a a.proof_state
end
else
else
begin
let previous_result,previous_obs = a.proof_state,a.proof_obsolete in
let timelimit =
match previous_result with
| Done { Call_provers.pr_answer = Call_provers.Valid ; Call_provers.pr_time = t } ->
let time = max a.proof_timelimit (truncate (2.0*.t)) in
set_timelimit time a;
time
| _ -> a.proof_timelimit
in
let timelimit = adapt_timelimit a in
let callback result =
begin match result with
| Undone Interrupted ->
......@@ -478,7 +480,7 @@ let run_prover eS eT ~context_unproved_goals_only ~timelimit pr a =
let proof_successful_or_just_edited a =
match a.proof_state with
| Done { Call_provers.pr_answer = Call_provers.Valid }
| Done { Call_provers.pr_answer = Call_provers.Valid }
| Undone JustEdited -> true
| _ -> false
......@@ -575,8 +577,8 @@ module Todo = struct
dprintf debug "[Sched] todo : %i@." todo.todo
end
let push_report report (g,p,r) =
report := (g.goal_name,p,r)::!report
let push_report report (g,p,t,r) =
report := (g.goal_name,p,t,r)::!report
(** When no smoke *)
let check_external_proof eS eT todo a =
......@@ -593,7 +595,7 @@ let check_external_proof eS eT todo a =
| None ->
dprintf debug "[sched] prover not found : %a@."
Whyconf.print_prover ap;
Todo._done todo (g,ap,Prover_not_installed)
Todo._done todo (g,ap,0,Prover_not_installed)
(* set_proof_state ~notify ~obsolete:false a Undone *)
| Some (nap,npc) ->
let g = a.proof_parent in
......@@ -613,21 +615,24 @@ let check_external_proof eS eT todo a =
~notify ~keygen:O.create ~prover:nap ~env_session:eS a in
O.init a.proof_key (Proof_attempt a);
a in
let timelimit = adapt_timelimit a in
let callback result =
match result with
| Undone Scheduled | Undone Running | Undone Interrupted -> ()
| Undone (Unedited | JustEdited) -> assert false
| InternalFailure msg ->
Todo._done todo (g,ap,(CallFailed msg));
Todo._done todo (g,ap,timelimit,(CallFailed msg));
set_proof_state ~notify ~obsolete:false ~archived:false
result a
| Done new_res ->
begin
match a.proof_state with
| Done old_res ->
Todo._done todo (g,ap,(Result(new_res,old_res)))
Todo._done todo
(g,ap,timelimit,(Result(new_res,old_res)))
| _ ->
Todo._done todo (g,ap,No_former_result new_res)
Todo._done todo
(g,ap,timelimit,No_former_result new_res)
end;
set_proof_state ~notify ~obsolete:false ~archived:false
result a
......@@ -644,7 +649,7 @@ let check_external_proof eS eT todo a =
String.concat " " (npc.prover_config.Whyconf.command ::
npc.prover_config.Whyconf.extra_options) in
schedule_proof_attempt eT
~timelimit:a.proof_timelimit ~memlimit:0
~timelimit ~memlimit:0
?old ~command
~driver:npc.prover_driver
~callback
......@@ -661,19 +666,9 @@ let check_all eS eT ~callback =
eS.session;
let timeout () =
match Todo._end todo with
| None ->
(*
Printf.eprintf "Progress: %d/%d\r%!" !proofs_done !proofs_to_do;
*)
true
| Some reports ->
(*
Printf.eprintf "\n%!";
*)
callback !reports;false
(* decr maximum_running_proofs; *)
| None -> true
| Some reports -> callback !reports;false
in
(* incr maximum_running_proofs; *)
schedule_any_timeout eT timeout
......@@ -682,7 +677,7 @@ let check_all eS eT ~callback =
(***********************************)
let rec play_on_goal_and_children eS eT ~timelimit todo l g =
let callback _key status =
let callback _key status =
match status with
| Undone Running | Undone Scheduled -> ()
| _ ->
......@@ -690,7 +685,7 @@ let rec play_on_goal_and_children eS eT ~timelimit todo l g =
(* eprintf "todo decreased to %d@." todo.Todo.todo *)
in
List.iter
(fun p ->
(fun p ->
Todo.todo todo;
(* eprintf "todo increased to %d@." todo.Todo.todo; *)
(* eprintf "prover %a on goal %s@." *)
......@@ -724,7 +719,7 @@ let play_all eS eT ~callback ~timelimit l =
in
schedule_any_timeout eT timeout
(** Transformation *)
......
src/session/session_scheduler.mli
View file @ c6dc4315
......@@ -127,7 +127,7 @@ module Make(O: OBSERVER) : sig
O.key env_session -> t ->
?callback:(O.key proof_attempt -> proof_attempt_status -> unit) ->
O.key proof_attempt -> unit
(** [redo_external_proof es sched ?timelimit p g] run
(** [redo_external_proof es sched ?timelimit p g] run
*)
......@@ -214,14 +214,15 @@ module Make(O: OBSERVER) : sig
val check_all:
O.key env_session -> t ->
callback:((Ident.ident * Whyconf.prover * report) list -> unit) -> unit
callback:((Ident.ident * Whyconf.prover * int * report) list -> unit) ->
unit
(** [check_all session callback] reruns all the proofs of the
session, and reports for all proofs the current result and the
new one (does not change the session state) When finished,
calls the callback with the reports which are triples (goal
name, prover, report) *)
calls the callback with the reports which are 4-uples (goal
name, prover, timelimit, report) *)
val play_all :
val play_all :
O.key env_session -> t -> callback:(unit-> unit) ->
timelimit:int -> Whyconf.prover list -> unit
(** [play_all es sched l] runs every prover of list [l] on all
......
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