From c91243f001a818c020eb754355a7f9c31a96a20b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 18 Jul 2022 11:48:43 +0200
Subject: [PATCH] [wp] fixing test cache miss printing
---
src/plugins/wp/Stats.ml | 12 +++++++-----
1 file changed, 7 insertions(+), 5 deletions(-)
diff --git a/src/plugins/wp/Stats.ml b/src/plugins/wp/Stats.ml
index d6385e9a6ec..ff81afab526 100644
--- a/src/plugins/wp/Stats.ml
+++ b/src/plugins/wp/Stats.ml
@@ -235,13 +235,16 @@ let pp_stats ~shell ~updating fmt s =
Format.fprintf fmt " (Tactics %d)" s.tactics
else if s.tactics = 1 then
Format.fprintf fmt " (Tactic)" ;
- let perfo = not shell || (not updating && s.cached < vp) in
+ let print_cache =
+ 0 < s.cached && List.exists (fun (p,_) -> p <> Qed) s.provers in
+ let print_perfo =
+ not shell || (print_cache && not updating && s.cached < np) in
let qed_only =
match s.provers with [Qed,_] -> vp = np | _ -> false in
List.iter
(fun (p,pr) ->
let success = truncate pr.success in
- let print_perfo = perfo && pr.time > Rformat.epsilon in
+ let print_perfo = print_perfo && pr.time > Rformat.epsilon in
let print_proofs = success > 0 && np > 1 in
let print_qed = qed_only && s.verdict = Valid && vp = np in
if p != Qed || print_qed || print_perfo || print_proofs then
@@ -255,9 +258,8 @@ let pp_stats ~shell ~updating fmt s =
Format.fprintf fmt ")"
end
) s.provers ;
- if 0 < s.cached && List.exists (fun (p,_) -> p <> Qed) s.provers
- then
- if s.cached = vp || updating then
+ if print_cache then
+ if s.cached = np || updating then
Format.fprintf fmt " (Cached)"
else
if shell then
--
GitLab