diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 212fe6f8babb88e611c1878c66090c3f20a314c8..307d9dc45c1e2d6afe130e2cf30a9e175266a778 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -1247,7 +1247,7 @@ let digest wpo drv prover task =
let _ = Command.print_file file
begin fun fmt ->
Format.fprintf fmt "(* WP Task for Prover %s *)@\n"
- (Why3Provers.print_why3 prover) ;
+ (Why3Provers.ident_why3 prover) ;
Why3.Driver.print_task_prepared drv fmt task ;
end
in Digest.file file |> Digest.to_hex
diff --git a/src/plugins/wp/Stats.ml b/src/plugins/wp/Stats.ml
index de3d5cee53e92a51c465c7d2d5b94e48d5ee52b8..32e6fb46c184431afa9d5f919f3909473877b304 100644
--- a/src/plugins/wp/Stats.ml
+++ b/src/plugins/wp/Stats.ml
@@ -124,16 +124,14 @@ let consolidated ~smoke = function
r.verdict,
(if cached then 1 else 0),
if p = Qed then [Qed,pqed r]
- else
- if VCS.is_valid r
- then pmerge [Qed,psolver r] [p,if smoke then psmoke r else presult r]
- else []
+ else pmerge [Qed,psolver r] [p,if smoke then psmoke r else presult r]
let smoked_result (p,r) = p, { r with verdict = VCS.smoked r.verdict }
let results ~smoke prs =
let prs = if smoke then List.map smoked_result prs else prs in
let verdict, cached, provers = consolidated ~smoke prs in
+ verdict,
match verdict with
| Valid ->
{ zero with provers ; cached ; proved = 1 }
@@ -194,7 +192,7 @@ let pp_pstats fmt p =
Rformat.pp_time mean
Rformat.pp_time p.tmax
-let pp_stats fmt s =
+let pp_stats ~shell ~updating fmt s =
let vp = s.proved in
let np = proofs s in
if vp < np && np > 1 then
@@ -203,21 +201,30 @@ let pp_stats fmt s =
Format.fprintf fmt " (Tactics %d)" s.tactics
else if np <= 1 && s.tactics = 1 then
Format.fprintf fmt " (Tactic)" ;
- let shell = Wp_parameters.has_dkey dkey_shell in
+ let perfo = not shell || (not updating && s.cached < vp) in
+ let only_qed = match s.provers with [Qed,_] -> true | _ -> false in
List.iter
(fun (p,pr) ->
let success = truncate pr.success in
- let title = VCS.title_of_prover ~version:false p in
- Format.fprintf fmt " (%s" title ;
- if success > 0 && np > 1 then
- Format.fprintf fmt " %d/%d" success np ;
- if not shell && pr.time > Rformat.epsilon then
- Format.fprintf fmt " %a" Rformat.pp_time pr.time ;
- Format.fprintf fmt ")"
+ let print_perfo = perfo && pr.time > Rformat.epsilon in
+ let print_proofs = success > 0 && np > 1 in
+ if p != Qed || only_qed || print_perfo || print_proofs then
+ begin
+ let title = VCS.title_of_prover ~version:false p in
+ Format.fprintf fmt " (%s" title ;
+ if print_proofs then
+ Format.fprintf fmt " %d/%d" success np ;
+ if print_perfo then
+ Format.fprintf fmt " %a" Rformat.pp_time pr.time ;
+ Format.fprintf fmt ")"
+ end
) s.provers ;
if 0 < s.cached then
- if s.cached = np then
+ if s.cached = vp || updating then
Format.fprintf fmt " (Cached)"
+ else
+ if shell then
+ Format.fprintf fmt " (Cache miss %d)" (np - s.cached)
else
Format.fprintf fmt " (Cached %d/%d)" s.cached np
diff --git a/src/plugins/wp/Stats.mli b/src/plugins/wp/Stats.mli
index 0a2023db5fc91d69f7d5228746effd219a02673b..c1ced421667ad9029a5c880a8541498fad1595c3 100644
--- a/src/plugins/wp/Stats.mli
+++ b/src/plugins/wp/Stats.mli
@@ -47,9 +47,9 @@ type stats = {
}
val pp_pstats : Format.formatter -> pstats -> unit
-val pp_stats : Format.formatter -> stats -> unit
+val pp_stats : shell:bool -> updating:bool -> Format.formatter -> stats -> unit
-val results : smoke:bool -> (VCS.prover * VCS.result) list -> stats
+val results : smoke:bool -> (VCS.prover * VCS.result) list -> VCS.verdict * stats
val tactical : qed:float -> stats list -> stats
val proofs : stats -> int
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index a280067c96a44566108d3d12744afecf72fd8fa4..3a94da3f3fc1efa70743fc878bbd55f8a6fcba0d 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -55,7 +55,7 @@ let parse_prover = function
| Fallback p ->
Wp_parameters.warning ~current:false ~once:true
"Prover '%s' not found, fallback to '%s'"
- (String.concat ":" prv) (Why3Provers.print_wp p) ;
+ (String.concat ":" prv) (Why3Provers.ident_wp p) ;
Some (Why3 p)
| NotFound ->
Wp_parameters.error ~once:true
@@ -75,18 +75,15 @@ let parse_mode m =
Batch
let name_of_prover = function
- | Why3 s -> Why3Provers.print_wp s
+ | Why3 s -> Why3Provers.ident_wp s
| Qed -> "qed"
| Tactical -> "script"
let title_of_prover ?version = function
| Why3 s ->
- let v = match version with Some v -> v | None ->
- Wp_parameters.has_dkey dkey_shell
- in
- if v
- then Why3Provers.name s
- else Why3Provers.title s
+ let version = match version with Some v -> v | None ->
+ not (Wp_parameters.has_dkey dkey_shell)
+ in Why3Provers.title ~version s
| Qed -> "Qed"
| Tactical -> "Script"
@@ -112,7 +109,7 @@ let sanitize_why3 s =
Buffer.contents buffer
let filename_for_prover = function
- | Why3 s -> sanitize_why3 (Why3Provers.print_wp s)
+ | Why3 s -> sanitize_why3 (Why3Provers.ident_wp s)
| Qed -> "Qed"
| Tactical -> "Tactical"
diff --git a/src/plugins/wp/Why3Provers.ml b/src/plugins/wp/Why3Provers.ml
index 167dc3e1370b6261b1861de7846aaf73e0402c48..0d2e6511ac8174b9c033b67ccf42724508f9cbfb 100644
--- a/src/plugins/wp/Why3Provers.ml
+++ b/src/plugins/wp/Why3Provers.ml
@@ -87,14 +87,15 @@ let find_fallback name =
end
| _ -> NotFound
-let print_why3 = Why3.Whyconf.prover_parseable_format
-let print_wp s =
+let ident_why3 = Why3.Whyconf.prover_parseable_format
+let ident_wp s =
let name = Why3.Whyconf.prover_parseable_format s in
let prv = String.split_on_char ',' name in
String.concat ":" prv
-let title p = Pretty_utils.to_string Why3.Whyconf.print_prover p
-let name p = p.Why3.Whyconf.prover_name
+let title ?(version=true) p =
+ if version then Pretty_utils.to_string Why3.Whyconf.print_prover p
+ else p.Why3.Whyconf.prover_name
let compare = Why3.Whyconf.Prover.compare
let is_mainstream p = p.Why3.Whyconf.prover_altern = ""
diff --git a/src/plugins/wp/Why3Provers.mli b/src/plugins/wp/Why3Provers.mli
index 5463b35fa4888dcf53f4f43e6b6b4bf09af41e13..13f9ef446de1181e99c3dea4b7b5cc82b81c7a18 100644
--- a/src/plugins/wp/Why3Provers.mli
+++ b/src/plugins/wp/Why3Provers.mli
@@ -32,10 +32,9 @@ val find_opt : string -> t option
type fallback = Exact of t | Fallback of t | NotFound
val find_fallback : string -> fallback
-val print_why3 : t -> string
-val print_wp : t -> string
-val title : t -> string
-val name : t -> string
+val ident_why3 : t -> string
+val ident_wp : t -> string
+val title : ?version:bool -> t -> string
val compare : t -> t -> int
val provers : unit -> t list
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 8952be0b7507acf53ab0904514702dfcac842558..99bd498c8a59e1f84803e72ceae9469c01482c44 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -873,7 +873,7 @@ let do_prover_detect () =
Wp_parameters.result "Prover %10s %-6s [%a%s]"
p.prover_name p.prover_version
print_prover_shortcuts_for p
- (Why3Provers.print_wp p)
+ (Why3Provers.ident_wp p)
) provers
(* ------------------------------------------------------------------------ *)