diff --git a/src/plugins/wp/Cache.ml b/src/plugins/wp/Cache.ml
index d08034e93ca7bd84a44ba06bb4d5b340ad474e75..65da7ca4b528daae67654b0f7d37fdcc9eb24103 100644
--- a/src/plugins/wp/Cache.ml
+++ b/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
diff --git a/src/plugins/wp/Cache.mli b/src/plugins/wp/Cache.mli
index 39af510514147e3d227b1a69b7b02ca38789e2b9..85130ef5bbf06c648b9bd4bd09b4dd50ed1735c9 100644
--- a/src/plugins/wp/Cache.mli
+++ b/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 =
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index 1a855c3bbbe474b41d5fb2df7d0fc903235b27e0..50507c33c3974e967750caf41b168e317e152ccb 100644
--- a/src/plugins/wp/VCS.ml
+++ b/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
diff --git a/src/plugins/wp/VCS.mli b/src/plugins/wp/VCS.mli
index 0e869ebea1458ef899c8e8ea6ff4b563cf224644..54b34f23ef850f4e974c4a2e18034c035d510ec4 100644
--- a/src/plugins/wp/VCS.mli
+++ b/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
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 6cb8afbc7c0ed22294ae6d0c2bec466ce0d261b6..58c0b6ab08ba24e487a3d5de3182d46d467661a9 100644
--- a/src/plugins/wp/register.ml
+++ b/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 =
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test.ml b/src/plugins/wp/tests/wp/stmtcompiler_test.ml
index 7d61b014274483fc8f0d3e8782735b9a3c84b10d..07e77bf23093eb5c0ec694eecf32ac30f6317f15 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test.ml
+++ b/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;
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
index 513c205deeacdeef55bdc3c3f05713a9800eb399..f38450c4501df76ed0fdbe6cbebbee247a3431d8 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
+++ b/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;
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index 1e5cc14b71bfb9a0432824d9cc734f81d514c387..0574facb577f4e77dfa37fbe2ebb334da8594cbc 100644
--- a/src/plugins/wp/wpo.ml
+++ b/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