[wp] cache clearing don't need lazy hash

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))
-
 (* -------------------------------------------------------------------------- *)

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
 
 (**************************************************************************)

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