From 6d99002362efd6fdde6ce76f224464a8e3dd63ab Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 7 Jul 2022 09:07:39 +0200
Subject: [PATCH] [wp] export human-readlabel json stats
---
src/plugins/wp/Stats.ml | 1 +
src/plugins/wp/Why3Provers.ml | 2 +-
2 files changed, 2 insertions(+), 1 deletion(-)
diff --git a/src/plugins/wp/Stats.ml b/src/plugins/wp/Stats.ml
index 662b145ba0b..3732555a5f7 100644
--- a/src/plugins/wp/Stats.ml
+++ b/src/plugins/wp/Stats.ml
@@ -187,6 +187,7 @@ let pretty fmt s =
let to_json_p (p,r) : Json.t = `Assoc [
"prover", `String (VCS.name_of_prover p) ;
+ "hprover", `String (VCS.title_of_prover p) ;
"time", `Float r.time ;
"htime", `String (Pretty_utils.to_string Rformat.pp_time r.time) ;
"success", `Int r.success ;
diff --git a/src/plugins/wp/Why3Provers.ml b/src/plugins/wp/Why3Provers.ml
index 07645004d58..167dc3e1370 100644
--- a/src/plugins/wp/Why3Provers.ml
+++ b/src/plugins/wp/Why3Provers.ml
@@ -93,7 +93,7 @@ let print_wp s =
let prv = String.split_on_char ',' name in
String.concat ":" prv
-let title p = Format.asprintf "%a" Why3.Whyconf.print_prover p
+let title p = Pretty_utils.to_string Why3.Whyconf.print_prover p
let name p = p.Why3.Whyconf.prover_name
let compare = Why3.Whyconf.Prover.compare
let is_mainstream p = p.Why3.Whyconf.prover_altern = ""
--
GitLab