diff --git a/src/plugins/wp/Cache.ml b/src/plugins/wp/Cache.ml index c974a203dc5040af9966347b1460bfd9f0046cb2..afbda25944dc4577d6197d92ec775b88976c69d3 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 0ed21713a0d2f4410eb18124fda0ad3b24f3c91d..62ce8ec540b2696d7a8fd52eaa9fd1a5ec1695e4 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 9769f8b30db772615ebc4606fbae13579398a497..fe578bed812d067dfdd1834d09f7c951c67e3c96 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