From 9beb61d843560c7d897e255161e274d71d5abd9a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 1 Oct 2020 14:04:16 +0200
Subject: [PATCH] [wp] cache clearing don't need lazy hash
---
src/plugins/wp/Cache.ml | 7 ++-----
src/plugins/wp/Cache.mli | 2 +-
src/plugins/wp/ProverWhy3.ml | 3 +--
3 files changed, 4 insertions(+), 8 deletions(-)
diff --git a/src/plugins/wp/Cache.ml b/src/plugins/wp/Cache.ml
index c974a203dc5..afbda25944d 100644
--- a/src/plugins/wp/Cache.ml
+++ b/src/plugins/wp/Cache.ml
@@ -213,9 +213,9 @@ let set_cache_result ~mode hash prover result =
Wp_parameters.warning ~current:false ~once:true
"can not update cache (%s)" (Printexc.to_string err)
-let remove_cache_result hash =
- let hash = Lazy.force hash in
+let clear_result ~digest prover goal =
try
+ let hash = digest prover goal in
let dir = get_usable_dir ~make:true () in
let file = Printf.sprintf "%s/%s.json" dir hash in
Extlib.safe_remove file
@@ -287,7 +287,4 @@ let get_result ~digest ~runner ~timeout ~steplimit prover goal =
| _ -> ()
end
-let clean_entry_for ~digest prover goal =
- remove_cache_result (lazy (digest prover goal))
-
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Cache.mli b/src/plugins/wp/Cache.mli
index 0ed21713a0d..62ce8ec540b 100644
--- a/src/plugins/wp/Cache.mli
+++ b/src/plugins/wp/Cache.mli
@@ -41,6 +41,6 @@ type 'a runner =
VCS.result Task.task
val get_result: digest:('a digest) -> runner:('a runner) -> 'a runner
-val clean_entry_for: digest:('a digest) -> Why3Provers.t -> 'a -> unit
+val clear_result: digest:('a digest) -> Why3Provers.t -> 'a -> unit
(**************************************************************************)
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 9769f8b30db..fe578bed812 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -1275,9 +1275,8 @@ let scriptfile ~force ~ext wpo =
Format.sprintf "%s/%s%s" (dir :> string) wpo.Wpo.po_sid ext
let call_editor ~script wpo pconf driver prover task =
- let digest = digest wpo driver in
Wp_parameters.feedback ~ontty:`Transient "Editing %S..." script ;
- Cache.clean_entry_for digest prover task ;
+ Cache.clear_result ~digest:(digest wpo driver) prover task ;
let call = Why3.Call_provers.call_editor ~command:(editor pconf) script in
call_prover_task ~timeout:None ~steps:None pconf.prover call
--
GitLab