Module Wp.Stats

Performance Reporting

type pstats = {
tmin : float;(*

minimum prover time (non-smoke proof only)

*)
tval : float;(*

cummulated prover time (non-smoke proof only)

*)
tmax : float;(*

maximum prover time (non-smoke proof only)

*)
tnbr : float;(*

number of non-smoke proofs

*)
time : float;(*

cumulated prover time (smoke and non-smoke)

*)
success : float;(*

number of success (valid xor smoke)

*)
}

Prover Stats

type stats = {
verdict : VCS.verdict;(*

global verdict

*)
provers : (VCS.prover * pstats) list;(*

meaningfull provers

*)
tactics : int;(*

number of tactics

*)
proved : int;(*

number of proved sub-goals

*)
trivial : int;(*

number of proved sub-goals with Qed or No-prover time

*)
timeout : int;(*

number of resulting timeouts and stepouts

*)
unknown : int;(*

number of resulting unknown

*)
noresult : int;(*

number of no-result

*)
failed : int;(*

number of resulting failures

*)
cached : int;(*

number of cached (non-trivial) results

*)
}

Cumulated Stats

Remark: for each sub-goal, only the _best_ prover result is kept

val pp_pstats : Stdlib.Format.formatter -> pstats -> unit
val pp_stats : shell:bool -> cache:Cache.mode -> Stdlib.Format.formatter -> stats -> unit
val pretty : Stdlib.Format.formatter -> stats -> unit
val empty : stats
val add : stats -> stats -> stats
val results : smoke:bool -> (VCS.prover * VCS.result) list -> stats
val tactical : qed:float -> stats list -> stats
val script : stats -> VCS.result
val proofs : stats -> int
val complete : stats -> bool