Commit 78c34cf3 authored by MARCHE Claude's avatar MARCHE Claude

ITP: fixed issues with limits and replay

- removed a temporary harcoded setting of steps limits
- allow reply to replay only obsolete proofs
parent 5ac7d3c2
......@@ -561,7 +561,7 @@ let interpNotif (n: notification) =
| Query_Error (_nid, s) ->
PE.error_print_msg
(Format.asprintf "Query error on selected node: \"%s\"" s)
| Query_Info (nid, s) -> PE.error_print_msg s
| Query_Info (_nid, s) -> PE.error_print_msg s
| Help s -> PE.error_print_msg s
| Information s -> PE.error_print_msg s
| Error s ->
......@@ -579,6 +579,7 @@ let interpNotif (n: notification) =
| Node_change (nid, up) ->
begin
match up with
| Obsolete _ -> assert false (* TODO *)
| Proved true -> TaskList.update_status `Valid (string_of_int nid)
| Proved false -> TaskList.update_status `Unknown (string_of_int nid)
| Proof_status_change (c, _obsolete, _rl) ->
......
......@@ -551,8 +551,7 @@ let run_timeout_handler () =
let schedule_proof_attempt_r c id pr ~limit ~callback =
let panid =
graft_proof_attempt c.controller_session id pr
~timelimit:limit.Call_provers.limit_time
graft_proof_attempt c.controller_session id pr ~limit
in
Queue.add (c,id,pr,limit,callback panid) scheduled_proof_attempts;
callback panid Scheduled;
......@@ -812,7 +811,8 @@ let replay_print fmt (lr: (proofNodeID * Whyconf.prover * Call_provers.resource_
in
Format.fprintf fmt "%a@." (Pp.print_list Pp.newline pp_elem) lr
let replay ~remove_obsolete ~use_steps c ~callback ~notification ~final_callback =
let replay ?(obsolete_only=true) ?(use_steps=false)
c ~callback ~notification ~final_callback =
let craft_report count s r id pr limits pa =
match s with
......@@ -834,15 +834,6 @@ let replay ~remove_obsolete ~use_steps c ~callback ~notification ~final_callback
r := (id, pr, limits, Prover_not_installed) :: !r;
in
let update_uninstalled c remove_obsolete id s pr =
match s with
| Uninstalled _ ->
if remove_obsolete then
remove_proof_attempt c.controller_session id pr
else
()
| _ -> () in
(* === replay === *)
let session = c.controller_session in
let count = ref 0 in
......@@ -851,26 +842,28 @@ let replay ~remove_obsolete ~use_steps c ~callback ~notification ~final_callback
(* TODO count the number of node in a more efficient way *)
(* Counting the number of proof_attempt to print report only once *)
Session_itp.session_iter_proof_attempt
(fun _ _ -> incr count) session;
(fun _ pa -> if pa.proof_obsolete || not obsolete_only then incr count) session;
(* Replaying function *)
let replay_pa id pa =
let parid = pa.parent in
let pr = pa.prover in
(* If use_steps, we give only steps as a limit *)
let limit =
if use_steps then
Call_provers.{empty_limit with limit_steps = pa.limit.limit_steps}
else
Call_provers.{ pa.limit with limit_steps = empty_limit.limit_steps }
in
replay_proof_attempt c pr limit parid id
~callback:(fun id s ->
craft_report count s report parid pr limit pa;
update_uninstalled c remove_obsolete parid s pr;
callback id s;
if !count = 0 then final_callback !report)
~notification in
if pa.proof_obsolete || not obsolete_only then
begin
let parid = pa.parent in
let pr = pa.prover in
(* If use_steps, we give only steps as a limit *)
let limit =
if use_steps then
Call_provers.{empty_limit with limit_steps = pa.limit.limit_steps}
else
Call_provers.{ pa.limit with limit_steps = empty_limit.limit_steps }
in
replay_proof_attempt c pr limit parid id
~callback:(fun id s ->
craft_report count s report parid pr limit pa;
callback id s;
if !count = 0 then final_callback !report)
~notification
end in
(* Calling replay on all the proof_attempts of the session *)
Session_itp.session_iter_proof_attempt replay_pa session
......
......@@ -250,10 +250,8 @@ val replay_print:
unit
val replay:
remove_obsolete:bool ->
(** If true, removes obsolete attempt in all cases. Otherwise keep it in
some cases: for example when prover is not installed *)
use_steps:bool -> (** Replay use recorded number of proof steps if true *)
?obsolete_only:bool ->
?use_steps:bool ->
controller ->
callback:(proofAttemptID -> proof_attempt_status -> unit) ->
notification:(any -> bool -> unit) ->
......@@ -261,11 +259,24 @@ val replay:
((proofNodeID * Whyconf.prover * Call_provers.resource_limit * report) list
-> unit) ->
unit
(** This function reruns all the proofs of the session, and reports for all
proofs the current result and new one (does change the session state and if
remove_obsolete is true also remove obsolete proofs that could not be
replayed). When finished, call the callback with the reports which are
4-uples [(goalID, prover, limits, report)] *)
(** This function reruns all the proofs of the session, and produces a report
comparing the results with the former ones.
The proofs are replayed asynchronously, and the states of these proofs are
notified via [callback] similarly as for [schedule_proof_attempt].
The session state is changed, all changes are notified via the
callback [notification]
When finished, call the callback [final_callback] with the report,
a list of 4-uples [(goalID, prover, limits, report)]
When obsolete_only is set, only obsolete proofs are replayed (default)
When use_steps is set, replay use the recorded number of proof
steps (not set by default)
*)
end
......@@ -938,7 +938,7 @@ let () =
let final_callback lr =
P.notify (Message (Replay_Info (Pp.string_of C.replay_print lr))) in
(* TODO make replay print *)
C.replay ~use_steps:false ~remove_obsolete:false d.cont
C.replay ~use_steps:false ~obsolete_only:true d.cont
~callback ~notification:notify_change_proved ~final_callback
(* ---------------- Mark obsolete ------------------ *)
......
......@@ -199,17 +199,17 @@ let parse_prover_name config name args :
if (List.length args > 2) then None else
match args with
| [] ->
let default_limit = Call_provers.{limit_time = Whyconf.timelimit main;
limit_mem = Whyconf.memlimit main;
limit_steps = 0} in
let default_limit = Call_provers.{empty_limit with
limit_time = Whyconf.timelimit main;
limit_mem = Whyconf.memlimit main} in
Some (prover_config, default_limit)
| [timeout] -> Some (prover_config,
Call_provers.{empty_limit with
limit_time = int_of_string timeout})
| [timeout; oom ] ->
Some (prover_config, Call_provers.{limit_time = int_of_string timeout;
limit_mem = int_of_string oom;
limit_steps = 0})
Some (prover_config, Call_provers.{empty_limit with
limit_time = int_of_string timeout;
limit_mem = int_of_string oom})
| _ -> None
end
......
......@@ -515,10 +515,7 @@ let add_proof_attempt session prover limit state obsolete edit parentID =
id
let graft_proof_attempt (s : session) (id : proofNodeID) (pr : Whyconf.prover)
~timelimit =
let limit = { Call_provers.limit_time = timelimit;
Call_provers.limit_mem = 0;
Call_provers.limit_steps = -1; } in
~limit =
add_proof_attempt s pr limit None false None id
......
......@@ -129,11 +129,11 @@ val merge_file_section :
theory *)
val graft_proof_attempt : session -> proofNodeID -> Whyconf.prover ->
timelimit:int -> proofAttemptID
(** [graft_proof_attempt s id pr t] adds a proof attempt with prover
[pr] and timelimit [t] in the session [s] as a child of the task
limit:Call_provers.resource_limit -> proofAttemptID
(** [graft_proof_attempt s id pr l] adds a proof attempt with prover
[pr] and limits [l] in the session [s] as a child of the task
[id]. If there already a proof attempt with the same prover, it
updates it with the new timelimit. It returns the id of the
updates it with the limits. It returns the id of the
generated proof attempt. *)
val update_proof_attempt : session -> proofNodeID -> Whyconf.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