Wp.Stats
type pstats = {
}
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 results : smoke:bool -> (VCS.prover * VCS.result) list -> stats
val script : stats -> VCS.result
val proofs : stats -> int
val complete : stats -> bool