Commit 369fe200 authored by MARCHE Claude's avatar MARCHE Claude

experimental new benchmarking option

parent 723ee788
......@@ -28,7 +28,7 @@ let opt_version = ref false
let opt_stats = ref true
let opt_force = ref false
let opt_convert_unknown_provers = ref false
let opt_bench = ref false
(** {2 Smoke detector} *)
......@@ -72,6 +72,8 @@ let spec = Arg.align [
("-smoke-detector",
Arg.Symbol (["none";"top";"deep"],set_opt_smoke),
" try to detect if the context is self-contradicting") ;
("-bench",
Arg.Set opt_bench, " run as bench (experimental)");
("-s",
Arg.Clear opt_stats,
" do not print statistics") ;
......@@ -369,12 +371,35 @@ let transform_smoke env_session =
| SD_Deep -> trans "smoke_detector_deep" env_session
let run_as_bench env_session =
let sched =
M.init (Whyconf.running_provers_max (Whyconf.get_main config))
in
let provers =
Session.PHprover.fold
(fun _ p acc ->
match p with
| None -> acc
| Some p -> p.Session.prover_config.Whyconf.prover :: acc)
env_session.Session.loaded_provers []
in
let callback () =
eprintf "We should now save the session...@.";
exit 0
in
M.play_all env_session sched ~callback ~timelimit:2 provers;
main_loop ();
eprintf "main replayer (in bench mode) exited unexpectedly@.";
exit 1
let () =
try
eprintf "Opening session...@?";
let env_session,found_obs =
let session = S.read_session project_dir in
M.update_session ~allow_obsolete:true session env config in
M.update_session ~allow_obsolete:true session env config
in
if !opt_bench then run_as_bench env_session;
transform_smoke env_session;
if !opt_convert_unknown_provers then M.convert_unknown_prover env_session;
let sched =
......
......@@ -514,33 +514,6 @@ let replay eS eT ~obsolete_only ~context_unproved_goals_only a =
~obsolete_only ~context_unproved_goals_only)
tr.transf_goals
(***********************************)
(* play all *)
(***********************************)
let rec play_on_goal_and_children eS eT ~timelimit l g =
List.iter
(fun p -> prover_on_goal eS eT ~timelimit p g)
l;
PHstr.iter
(fun _ t ->
List.iter
(play_on_goal_and_children eS eT ~timelimit l)
t.transf_goals)
g.goal_transformations
let play_all eS eT ~timelimit l =
PHstr.iter
(fun _ file ->
List.iter
(fun th ->
List.iter
(play_on_goal_and_children eS eT ~timelimit l)
th.theory_goals)
file.file_theories)
eS.session.session_files
(***********************************)
(* method: mark proofs as obsolete *)
(***********************************)
......@@ -692,6 +665,43 @@ let check_all eS eT ~callback =
(* incr maximum_running_proofs; *)
schedule_any_timeout eT timeout
(***********************************)
(* play all *)
(***********************************)
let rec play_on_goal_and_children eS eT ~timelimit l g =
List.iter
(fun p -> prover_on_goal eS eT ~timelimit p g)
l;
PHstr.iter
(fun _ t ->
List.iter
(play_on_goal_and_children eS eT ~timelimit l)
t.transf_goals)
g.goal_transformations
let play_all eS eT ~callback ~timelimit l =
let todo = Todo.create (ref ()) (fun _ _ -> ()) in
PHstr.iter
(fun _ file ->
List.iter
(fun th ->
List.iter
(play_on_goal_and_children eS eT ~timelimit l)
th.theory_goals)
file.file_theories)
eS.session.session_files;
let timeout () =
match Todo._end todo with
| None -> true
| Some _ -> callback (); false
in
schedule_any_timeout eT timeout
(** Transformation *)
let transformation_on_goal_aux eS tr keep_dumb_transformation g =
......
......@@ -180,24 +180,6 @@ module Make(O: OBSERVER) : sig
O.key proof_attempt -> unit
(** edit the given proof attempt using the appropriate editor *)
val replay :
O.key env_session -> t ->
obsolete_only:bool ->
context_unproved_goals_only:bool -> O.key any -> unit
(** [replay es sched ~obsolete_only ~context_unproved_goals_only 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 don't rerun proofs
already 'valid'
*)
val play_all :
O.key env_session -> t -> timelimit:int -> Whyconf.prover list -> unit
(** [play_all es sched l] runs every prover of list [l] on all
goals and sub-goals of the session, with the given time limit.
Useful for benchmarking provers
*)
val cancel : O.key any -> unit
(** [cancel a] marks all proofs under [a] as obsolete *)
......@@ -219,6 +201,17 @@ module Make(O: OBSERVER) : sig
| Prover_not_installed
| No_former_result of Call_provers.prover_result
val replay :
O.key env_session -> t ->
obsolete_only:bool ->
context_unproved_goals_only:bool -> O.key any -> unit
(** [replay es sched ~obsolete_only ~context_unproved_goals_only 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 don't rerun proofs
already 'valid'
*)
val check_all:
O.key env_session -> t ->
callback:((Ident.ident * Whyconf.prover * report) list -> unit) -> unit
......@@ -228,6 +221,15 @@ module Make(O: OBSERVER) : sig
calls the callback with the reports which are triples (goal
name, prover, report) *)
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
goals and sub-goals of the session, with the given time limit.
[callback] is called when all tasks are finished.
Useful for benchmarking provers
*)
val convert_unknown_prover : O.key env_session -> unit
(** Same as {!Session_tools.convert_unknown_prover} *)
......
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