[wp] printing stats wrt various modes

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

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
 

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

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"
 

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 = ""
 

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

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
 
 (* ------------------------------------------------------------------------ *)