From ec578debfcf5826c45db15eed389ef1d103fc934 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 10 Sep 2019 12:56:32 +0200
Subject: [PATCH] [wp/cache] use also environment for cache mode
(with deactivated trivial task detection)
---
src/plugins/wp/ProverWhy3.ml | 35 +++++++++++++++++++++++++++--------
src/plugins/wp/ProverWhy3.mli | 1 +
src/plugins/wp/register.ml | 10 +++++++---
3 files changed, 35 insertions(+), 11 deletions(-)
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 5922eabe1d1..c13cc803cce 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -20,7 +20,8 @@
(* *)
(**************************************************************************)
-[@@@ warning "-40-42-32"]
+(* Allow type-desambiguation for symbols *)
+[@@@ warning "-40-42"]
let dkey = Wp_parameters.register_category "prover"
let dkey_api = Wp_parameters.register_category "why3_api"
@@ -1094,18 +1095,36 @@ let reset () = hits := 0 ; miss := 0
let get_hits () = !hits
let get_miss () = !miss
-let get_mode () =
- match Wp_parameters.Cache.get () with
+let parse_mode ~origin ~fallback = function
| "none" -> NoCache
| "update" -> Update
| "replay" -> Replay
| "rebuild" -> Rebuild
| "offline" -> Offline
| "markup" -> Markup
- | m -> Wp_parameters.error
- ~once:true
- "Unknown -wp-cache %S (use 'none' instead)" m ;
- NoCache
+ | m ->
+ Wp_parameters.warning ~current:false
+ "Unknown %s mode %S (use %s instead)" origin m fallback ;
+ raise Not_found
+
+module MODE = WpContext.StaticGenerator(Datatype.Unit)
+ (struct
+ type key = unit
+ type data = mode
+ let name = "Wp.Cache.mode"
+ let compile () =
+ try
+ let origin = "FRAMAC_WP_CACHE" in
+ parse_mode ~origin ~fallback:"-wp-cache" (Sys.getenv origin)
+ with Not_found ->
+ try
+ parse_mode ~origin:"-wp-cache" ~fallback:"'none'"
+ (Wp_parameters.Cache.get())
+ with Not_found ->
+ NoCache
+ end)
+
+let get_mode = MODE.get
let task_hash wpo drv prover task =
lazy
@@ -1209,7 +1228,7 @@ let prove ?timeout ?steplimit ~prover wpo =
(* Why3 typed checked the task during its build *)
Task.return VCS.checked
else
- if is_trivial task then
+ if false && is_trivial task then
Task.return VCS.valid
else
let mode = get_mode () in
diff --git a/src/plugins/wp/ProverWhy3.mli b/src/plugins/wp/ProverWhy3.mli
index 47f63870138..4beeea60d2b 100644
--- a/src/plugins/wp/ProverWhy3.mli
+++ b/src/plugins/wp/ProverWhy3.mli
@@ -37,3 +37,4 @@ val reset : unit -> unit (** Reset cache statistics *)
val get_hits : unit -> int
val get_miss : unit -> int
+(**************************************************************************)
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 43ba83d815c..25ae43c9da7 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -361,12 +361,16 @@ let do_wpo_success goal s =
) pres ;
end
end
+ | Some (VCS.Tactical as p) ->
+ Wp_parameters.feedback ~ontty:`Silent
+ "[%a] Goal %s : Valid"
+ VCS.pp_prover p (Wpo.get_gid goal)
| Some p ->
let r = Wpo.get_result goal p in
Wp_parameters.feedback ~ontty:`Silent
- "[%a] Goal %s : %a%a"
+ "[%a] Goal %s : %a"
VCS.pp_prover p (Wpo.get_gid goal)
- VCS.pp_result r pp_warnings goal
+ VCS.pp_result r
let do_report_time fmt s =
begin
@@ -412,7 +416,7 @@ let do_report_stopped fmt s =
else
begin
if s.interrupted > 0 then
- Format.fprintf fmt " (stopped: %d)" s.interrupted ;
+ Format.fprintf fmt " (interrupted: %d)" s.interrupted ;
if s.unknown > 0 then
Format.fprintf fmt " (unknown: %d)" s.unknown ;
if s.incache > 0 then
--
GitLab