[wp] improved output for missing caches

src/plugins/wp/ProverWhy3.ml

@@ -1216,8 +1216,8 @@ let call_prover prover_config ~timeout ~steplimit drv prover task =
         false
   in
   let command = Why3.Whyconf.get_complete_command prover_config ~with_steps in
-  let call =
-    Why3.Driver.prove_task_prepared ~command ~limit drv task in
+  let call = Why3.Driver.prove_task_prepared ~command ~limit drv task in
+  let steps = if with_steps then steps else None in
   let pp_steps fmt s =
     if with_steps then Format.fprintf fmt "%i steps" (Why3.Opt.get_def (-1) s)
     else Format.fprintf fmt ""

src/plugins/wp/VCS.ml

@@ -289,33 +289,35 @@ let cached r = if is_verdict r then { r with cached=true } else r
 
 let kfailed ?pos msg = Pretty_utils.ksfprintf (failed ?pos) msg
 
-let perfo dkey = not (Wp_parameters.has_dkey dkey)
-
-let pp_perf fmt r =
+let pp_perf_forced fmt r =
   begin
     let t = r.solver_time in
-    if t > Rformat.epsilon && perfo dkey_shell
+    if t > Rformat.epsilon
     then Format.fprintf fmt " (Qed:%a)" Rformat.pp_time t ;
     let t = r.prover_time in
-    if t > Rformat.epsilon && perfo dkey_shell
+    if t > Rformat.epsilon
     then Format.fprintf fmt " (%a)" Rformat.pp_time t ;
     let s = r.prover_steps in
-    if s > 0 && perfo dkey_shell
+    if s > 0
     then Format.fprintf fmt " (%d)" s ;
-    if r.cached && perfo dkey_shell
+    if r.cached
     then Format.fprintf fmt " (cached)" ;
   end
 
+let pp_perf_shell fmt r =
+  if not (Wp_parameters.has_dkey dkey_shell) then
+    pp_perf_forced fmt r
+
 let pp_result fmt r =
   match r.verdict with
   | NoResult -> Format.pp_print_string fmt "No Result"
   | Computing _ -> Format.pp_print_string fmt "Computing"
   | Invalid -> Format.pp_print_string fmt "Invalid"
   | Failed -> Format.fprintf fmt "Failed@ %s" r.prover_errmsg
-  | Valid -> Format.fprintf fmt "Valid%a" pp_perf r
-  | Unknown -> Format.fprintf fmt "Unknown%a" pp_perf r
-  | Stepout -> Format.fprintf fmt "Step limit%a" pp_perf r
-  | Timeout -> Format.fprintf fmt "Timeout%a" pp_perf r
+  | Valid -> Format.fprintf fmt "Valid%a" pp_perf_shell r
+  | Unknown -> Format.fprintf fmt "Unknown%a" pp_perf_shell r
+  | Stepout -> Format.fprintf fmt "Step limit%a" pp_perf_shell r
+  | Timeout -> Format.fprintf fmt "Timeout%a" pp_perf_shell r
 
 let is_qualified prover result =
   match prover with
@@ -328,7 +330,7 @@ let pp_cache_miss fmt st updating prover result =
   && not (is_qualified prover result)
   && Wp_parameters.has_dkey dkey_shell
   then
-    Format.fprintf fmt "%s%a (missing cache)" st pp_perf result
+    Format.fprintf fmt "%s%a (missing cache)" st pp_perf_forced result
   else
     Format.pp_print_string fmt @@
     if is_valid result then "Valid" else "Unsuccess"