[wp] better feedback for cache miss (wp-qualif)

src/plugins/wp/Cache.ml

@@ -136,6 +136,11 @@ module MODE = WpContext.StaticGenerator(Datatype.Unit)
 let get_mode = MODE.get
 let set_mode m = MODE.clear () ; Wp_parameters.Cache.set (mode_name m)
 
+let is_updating () =
+  match MODE.get () with
+  | NoCache | Replay | Offline -> false
+  | Update | Rebuild | Cleanup -> true
+
 let task_hash wpo drv prover task =
   lazy
     begin

src/plugins/wp/Cache.mli

@@ -30,6 +30,8 @@ val get_hits : unit -> int
 val get_miss : unit -> int
 val get_removed : unit -> int
 
+val is_updating : unit -> bool
+
 val cleanup_cache : unit -> unit
 
 type runner =

src/plugins/wp/VCS.ml

@@ -317,31 +317,35 @@ let pp_result fmt r =
   | Stepout -> Format.fprintf fmt "Step limit%a" pp_perf r
   | Timeout -> Format.fprintf fmt "Timeout%a" pp_perf r
 
-let pp_cache_miss fmt st prover r =
-  let qualified =
-    match prover with
-    | Qed | Tactical -> true
-    | NativeAltErgo | NativeCoq -> r.verdict <> Timeout
-    | Why3 _ -> r.cached || r.prover_time < Rformat.epsilon
-  in
-  if not qualified && Wp_parameters.has_dkey dkey_shell then
-    Format.fprintf fmt "%s%a (unqualified)" st pp_perf r
+let is_qualified prover result =
+  match prover with
+  | Qed | Tactical -> true
+  | NativeAltErgo | NativeCoq -> result.verdict <> Timeout
+  | Why3 _ -> result.cached || result.prover_time < Rformat.epsilon
+
+let pp_cache_miss fmt st updating prover result =
+  if not updating
+  && not (is_qualified prover result)
+  && Wp_parameters.has_dkey dkey_shell
+  then
+    Format.fprintf fmt "%s%a (missing cache)" st pp_perf result
   else
-    Format.pp_print_string fmt (if is_valid r then "Valid" else "Unsuccess")
+    Format.pp_print_string fmt @@
+    if is_valid result then "Valid" else "Unsuccess"
 
-let pp_result_qualif prover fmt r =
+let pp_result_qualif ?(updating=true) prover result fmt =
   if Wp_parameters.has_dkey dkey_shell then
-    match r.verdict with
+    match result.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 -> pp_cache_miss fmt "Valid" prover r
-    | Unknown -> pp_cache_miss fmt "Unsuccess" prover r
-    | Timeout -> pp_cache_miss fmt "Timeout" prover r
-    | Stepout -> pp_cache_miss fmt "Stepout" prover r
+    | Failed -> Format.fprintf fmt "Failed@ %s" result.prover_errmsg
+    | Valid -> pp_cache_miss fmt "Valid" updating prover result
+    | Unknown -> pp_cache_miss fmt "Unsuccess" updating prover result
+    | Timeout -> pp_cache_miss fmt "Timeout" updating prover result
+    | Stepout -> pp_cache_miss fmt "Stepout" updating prover result
   else
-    pp_result fmt r
+    pp_result fmt result
 
 let compare p q =
   let rank = function

src/plugins/wp/VCS.mli

@@ -119,7 +119,8 @@ val configure : result -> config
 val autofit : result -> bool (** Result that fits the default configuration *)
 
 val pp_result : Format.formatter -> result -> unit
-val pp_result_qualif : prover -> Format.formatter -> result -> unit
+val pp_result_qualif : ?updating:bool -> prover -> result ->
+  Format.formatter -> unit
 
 val compare : result -> result -> int (* best is minimal *)
 val merge : result -> result -> result

src/plugins/wp/register.ml

@@ -391,19 +391,21 @@ let results g =
     (Wpo.get_results g)
 
 let do_wpo_failed goal =
+  let updating = Cache.is_updating () in
   match results goal with
   | [p,r] ->
-      Wp_parameters.result "[%a] Goal %s : %a%a"
+      Wp_parameters.result "[%a] Goal %s : %t%a"
         VCS.pp_prover p (Wpo.get_gid goal)
-        (VCS.pp_result_qualif p) r pp_warnings goal
+        (VCS.pp_result_qualif ~updating p r) pp_warnings goal
   | pres ->
       Wp_parameters.result "[Failed] Goal %s%t" (Wpo.get_gid goal)
         begin fun fmt ->
           pp_warnings fmt goal ;
           List.iter
             (fun (p,r) ->
-               Format.fprintf fmt "@\n%8s: @[<hv>%a@]"
-                 (VCS.title_of_prover p) (VCS.pp_result_qualif p) r
+               Format.fprintf fmt "@\n%8s: @[<hv>%t@]"
+                 (VCS.title_of_prover p)
+                 (VCS.pp_result_qualif ~updating p r)
             ) pres ;
         end
 
@@ -416,11 +418,12 @@ let do_wpo_smoke status goal =
     (Wpo.get_gid goal)
     begin fun fmt ->
       pp_warnings fmt goal ;
+      let updating = Cache.is_updating () in
       List.iter
         (fun (p,r) ->
-           Format.fprintf fmt "@\n%8s: @[<hv>%a@]"
+           Format.fprintf fmt "@\n%8s: @[<hv>%t@]"
              (VCS.title_of_prover p)
-             (VCS.pp_result_qualif p) r
+             (VCS.pp_result_qualif ~updating p r)
         ) (results goal) ;
     end
 
@@ -453,10 +456,11 @@ let do_wpo_success goal s =
             VCS.pp_prover script (Wpo.get_gid goal)
       | Some prover ->
           let result = Wpo.get_result goal prover in
+          let updating = Cache.is_updating () in
           Wp_parameters.feedback ~ontty:`Silent
-            "[%a] Goal %s : %a"
+            "[%a] Goal %s : %t"
             VCS.pp_prover prover (Wpo.get_gid goal)
-            (VCS.pp_result_qualif prover) result
+            (VCS.pp_result_qualif ~updating prover result)
     end
 
 let do_report_time fmt s =

src/plugins/wp/tests/wp/stmtcompiler_test.ml

@@ -28,8 +28,8 @@ let run () =
 
   let spawn goal =
     let result _ prv res =
-      Format.printf "[%a] %a@.@\n"
-        VCS.pp_prover prv (VCS.pp_result_qualif prv) res
+      Format.printf "[%a] %t@.@\n"
+        VCS.pp_prover prv (VCS.pp_result_qualif prv res)
     in
     let server = ProverTask.server () in
     Prover.spawn goal ~delayed:true ~result provers;

src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml

@@ -27,8 +27,8 @@ let run () =
 
   let spawn goal =
     let result _ prv res =
-      Format.printf "[%a] %a@.@\n"
-        VCS.pp_prover prv (VCS.pp_result_qualif prv) res
+      Format.printf "[%a] %t@.@\n"
+        VCS.pp_prover prv (VCS.pp_result_qualif prv res)
     in
     let server = ProverTask.server () in
     Prover.spawn goal ~delayed:true ~result provers;

src/plugins/wp/wpo.ml

@@ -283,8 +283,8 @@ struct
       List.iter
         (fun (prover,result) ->
            if result.verdict <> NoResult then
-             Format.fprintf fmt "Prover %a returns %a@\n"
-               pp_prover prover (pp_result_qualif prover) result
+             Format.fprintf fmt "Prover %a returns %t@\n"
+               pp_prover prover (pp_result_qualif prover result)
         ) results ;
     end
 
@@ -347,9 +347,9 @@ struct
       List.iter
         (fun (prover,result) ->
            if result.verdict <> NoResult then
-             Format.fprintf fmt "Prover %a returns %a@\n"
+             Format.fprintf fmt "Prover %a returns %t@\n"
                pp_prover prover
-               (pp_result_qualif prover) result
+               (pp_result_qualif prover result)
         ) results ;
     end