From db965bc788ea1f4dcff998e564684db54d6110b7 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 8 Nov 2023 18:53:54 +0100 Subject: [PATCH] [memo] Fix some cases where interrupted computations where memoized. --- CHANGES.md | 2 ++ coq/interp.ml | 2 -- coq/interp.mli | 4 +--- fleche/memo.ml | 53 +++++++++++++++++++++++++++++++++++-------------- fleche/memo.mli | 2 +- 5 files changed, 42 insertions(+), 21 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index f13b0ead9..5a4bfded5 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -19,6 +19,8 @@ - `proof/goals` request: new `mode` parameter, to specify goals after/before sentence display; renamed `pretac` to `command`, as to provide official support for speculative execution (@ejgallego, #600) + - fix some cases where interrupted computations where memoized + (@ejgallego, #603) # coq-lsp 0.1.8: Trick-or-treat ------------------------------- diff --git a/coq/interp.ml b/coq/interp.ml index b0de33ff3..e24e8d838 100644 --- a/coq/interp.ml +++ b/coq/interp.ml @@ -15,8 +15,6 @@ (* Written by: Emilio J. Gallego Arias *) (************************************************************************) -type 'a interp_result = ('a, Loc.t) Protect.E.t - let coq_interp ~st cmd = let st = State.to_coq st in let cmd = Ast.to_coq cmd in diff --git a/coq/interp.mli b/coq/interp.mli index 74a40ae23..2ddd853dd 100644 --- a/coq/interp.mli +++ b/coq/interp.mli @@ -15,6 +15,4 @@ (* Written by: Emilio J. Gallego Arias *) (************************************************************************) -type 'a interp_result = ('a, Loc.t) Protect.E.t - -val interp : st:State.t -> Ast.t -> State.t interp_result +val interp : st:State.t -> Ast.t -> (State.t, Loc.t) Protect.E.t diff --git a/fleche/memo.ml b/fleche/memo.ml index 2af20af56..6db8aba18 100644 --- a/fleche/memo.ml +++ b/fleche/memo.ml @@ -37,6 +37,35 @@ module CacheStats = struct Format.asprintf "cache hit rate: %3.2f" hit_rate end +module MemoTable = struct + module type S = sig + include Hashtbl.S + + val add_execution : + ('a, 'l) Coq.Protect.E.t t -> key -> ('a, 'l) Coq.Protect.E.t -> unit + + val add_execution_loc : + ('v * ('a, 'l) Coq.Protect.E.t) t + -> key + -> 'v * ('a, 'l) Coq.Protect.E.t + -> unit + end + + module Make (H : Hashtbl.HashedType) : S with type key = H.t = struct + include Hashtbl.Make (H) + + let add_execution t k ({ Coq.Protect.E.r; _ } as v) = + match r with + | Coq.Protect.R.Interrupted -> () + | _ -> add t k v + + let add_execution_loc t k ((_, { Coq.Protect.E.r; _ }) as v) = + match r with + | Coq.Protect.R.Interrupted -> () + | _ -> add t k v + end +end + module Interp = struct (* Loc-independent command evalution and caching. *) module VernacInput = struct @@ -56,11 +85,11 @@ module Interp = struct let input_info (st, v) = Format.asprintf "stm: %d | st %d" (Coq.Ast.hash v) (Hashtbl.hash st) - module HC = Hashtbl.Make (VernacInput) + module HC = MemoTable.Make (VernacInput) module Result = struct (* We store the location as to compute an offset for cached results *) - type t = Loc.t * Coq.State.t Coq.Interp.interp_result + type t = Loc.t * (Coq.State.t, Loc.t) Coq.Protect.E.t end type cache = Result.t HC.t @@ -118,26 +147,20 @@ module Interp = struct CacheStats.hit (); let res = adjust_offset ~stm_loc ~cached_loc res in Stats.make ~cache_hit:true ~time res - | None, time_hash -> ( + | None, time_hash -> if Debug.cache then Io.Log.trace "memo" "cache miss"; CacheStats.miss (); let kind = CS.Kind.Exec in let res, time_interp = CS.record ~kind ~f:(Coq.Interp.interp ~st) stm in + let () = HC.add_execution_loc !cache (st, stm) (stm_loc, res) in let time = time_hash +. time_interp in - match res.r with - | Coq.Protect.R.Interrupted -> - (* Don't cache interruptions *) - Stats.make ~time res - | Coq.Protect.R.Completed _ -> - let () = HC.add !cache (st, stm) (stm_loc, res) in - let time = time_hash +. time_interp in - Stats.make ~time res) + Stats.make ~time res end module Admit = struct type t = Coq.State.t - module C = Hashtbl.Make (Coq.State) + module C = MemoTable.Make (Coq.State) let cache = C.create 1000 @@ -145,7 +168,7 @@ module Admit = struct match C.find_opt cache v with | None -> let admitted_st = Coq.State.admit ~st:v in - C.add cache v admitted_st; + C.add_execution cache v admitted_st; admitted_st | Some admitted_st -> admitted_st end @@ -168,7 +191,7 @@ module Init = struct type t = S.t - module C = Hashtbl.Make (S) + module C = MemoTable.Make (S) let cache = C.create 1000 @@ -177,7 +200,7 @@ module Init = struct | None -> let root_state, workspace, uri = v in let admitted_st = Coq.Init.doc_init ~root_state ~workspace ~uri in - C.add cache v admitted_st; + C.add_execution cache v admitted_st; admitted_st | Some res -> res end diff --git a/fleche/memo.mli b/fleche/memo.mli index 4fef85b01..9e5aad834 100644 --- a/fleche/memo.mli +++ b/fleche/memo.mli @@ -17,7 +17,7 @@ module Interp : sig type t = Coq.State.t * Coq.Ast.t (** Interpret a command, possibly memoizing it *) - val eval : t -> Coq.State.t Coq.Interp.interp_result Stats.t + val eval : t -> (Coq.State.t, Loc.t) Coq.Protect.E.t Stats.t (** [size ()] Return the size in words, expensive *) val size : unit -> int