From 013965acaeb86bb2c620e1fecead8395f08c3bee Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 18 Feb 2023 19:12:10 +0100 Subject: [PATCH 1/3] [memo] Cleanup, progress towards #367 --- controller/cache.ml | 4 +- fleche/doc.ml | 8 +- fleche/memo.ml | 226 ++++++++++++++++++++------------------------ fleche/memo.mli | 30 +++--- 4 files changed, 123 insertions(+), 145 deletions(-) diff --git a/controller/cache.ml b/controller/cache.ml index 6bd88087..d0c0b2d5 100644 --- a/controller/cache.ml +++ b/controller/cache.ml @@ -22,7 +22,7 @@ let memo_cache_file = ".coq-lsp.cache" let memo_save_to_disk () = try - Fleche.Memo.save_to_disk ~file:memo_cache_file; + (* Fleche.Memo.save_to_disk ~file:memo_cache_file; *) LIO.trace "memo" "cache saved to disk" with exn -> LIO.trace "memo" (Printexc.to_string exn); @@ -36,7 +36,7 @@ let memo_read_from_disk () = try if Sys.file_exists memo_cache_file then ( LIO.trace "memo" "trying to load cache file"; - Fleche.Memo.load_from_disk ~file:memo_cache_file; + (* Fleche.Memo.load_from_disk ~file:memo_cache_file; *) LIO.trace "memo" "cache file loaded") else LIO.trace "memo" "cache file not present" with exn -> diff --git a/fleche/doc.ml b/fleche/doc.ml index 3583fd1a..30fb40cd 100644 --- a/fleche/doc.ml +++ b/fleche/doc.ml @@ -22,7 +22,7 @@ module Util = struct let print_stats () = (if !Config.v.mem_stats then - let size = Memo.mem_stats () in + let size = Memo.Interp.stats () in Io.Log.trace "stats" (string_of_int size)); Io.Log.trace "cache" (Stats.to_string ()); @@ -422,7 +422,7 @@ let recovery_for_failed_qed ~default nodes = | None -> Coq.Protect.E.ok (default, None) | Some ({ range; state; _ }, prev) -> ( if !Config.v.admit_on_bad_qed then - Memo.interp_admitted ~st:state + Memo.Admit.eval state |> Coq.Protect.E.map ~f:(fun state -> (state, Some range)) else match prev with @@ -433,7 +433,7 @@ let log_qed_recovery v = Coq.Protect.E.map ~f:(fun (st, range) -> let loc_msg = Option.cata Lang.Range.to_string "no loc" range in Io.Log.trace "recovery" - ("success" ^ loc_msg ^ " " ^ Memo.input_info (v, st)); + ("success" ^ loc_msg ^ " " ^ Memo.Interp.input_info (st, v)); st) (* Simple heuristic for Qed. *) @@ -456,7 +456,7 @@ let interp_and_info ~parsing_time ~st ast = let { Gc.major_words = mw_prev; _ } = Gc.quick_stat () in (* memo memory stats are disabled: slow and misleading *) let { Memo.Stats.res; cache_hit; memory = _; time } = - Memo.interp_command ~st ast + Memo.Interp.eval (st, ast) in let { Gc.major_words = mw_after; _ } = Gc.quick_stat () in let stats = Stats.dump () in diff --git a/fleche/memo.ml b/fleche/memo.ml index b6c51568..5450920c 100644 --- a/fleche/memo.ml +++ b/fleche/memo.ml @@ -15,18 +15,6 @@ module Stats = struct { res; cache_hit; memory; time } end -(* This requires a ppx likely as to ignore the CAst location *) -module VernacInput = struct - type t = Coq.Ast.t * Coq.State.t - - let equal (v1, st1) (v2, st2) = - if Coq.Ast.compare v1 v2 = 0 then - if Coq.State.compare st1 st2 = 0 then true else false - else false - - let hash (v, st) = Hashtbl.hash (Coq.Ast.hash v, st) -end - module CacheStats = struct let nhit, ntotal = (ref 0, ref 0) @@ -49,125 +37,113 @@ module CacheStats = struct Format.asprintf "cache hit rate: %3.2f" hit_rate end -let input_info (v, st) = - Format.asprintf "stm: %d | st %d" (Coq.Ast.hash v) (Hashtbl.hash st) +module Interp = struct + (* Loc-independent command evalution and caching. *) + module VernacInput = struct + type t = Coq.State.t * Coq.Ast.t -module HC = Hashtbl.Make (VernacInput) + (* This crutially relies on our ppx to ignore the CAst location *) + let equal (st1, v1) (st2, v2) = + if Coq.Ast.compare v1 v2 = 0 then + if Coq.State.compare st1 st2 = 0 then true else false + else false -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 -end + let hash (st, v) = Hashtbl.hash (Coq.Ast.hash v, st) + end + + type t = VernacInput.t + + let input_info (st, v) = + Format.asprintf "stm: %d | st %d" (Coq.Ast.hash v) (Hashtbl.hash st) + + module HC = Hashtbl.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 + end + + type cache = Result.t HC.t -type cache = Result.t HC.t - -let cache : cache ref = ref (HC.create 1000) - -let in_cache st stm = - let kind = CS.Kind.Hashing in - CS.record ~kind ~f:(HC.find_opt !cache) (stm, st) - -(* XXX: Move elsewhere *) -let loc_offset (l1 : Loc.t) (l2 : Loc.t) = - let line_offset = l2.line_nb - l1.line_nb in - let bol_offset = l2.bol_pos - l1.bol_pos in - let line_last_offset = l2.line_nb_last - l1.line_nb_last in - let bol_last_offset = l2.bol_pos_last - l1.bol_pos_last in - let bp_offset = l2.bp - l1.bp in - let ep_offset = l2.ep - l1.ep in - ( line_offset - , bol_offset - , line_last_offset - , bol_last_offset - , bp_offset - , ep_offset ) - -let loc_apply_offset + let cache : cache ref = ref (HC.create 1000) + let stats () = Obj.reachable_words (Obj.magic cache) + + let in_cache st stm = + let kind = CS.Kind.Hashing in + CS.record ~kind ~f:(HC.find_opt !cache) (st, stm) + + (* XXX: Move elsewhere *) + let loc_offset (l1 : Loc.t) (l2 : Loc.t) = + let line_offset = l2.line_nb - l1.line_nb in + let bol_offset = l2.bol_pos - l1.bol_pos in + let line_last_offset = l2.line_nb_last - l1.line_nb_last in + let bol_last_offset = l2.bol_pos_last - l1.bol_pos_last in + let bp_offset = l2.bp - l1.bp in + let ep_offset = l2.ep - l1.ep in ( line_offset , bol_offset , line_last_offset , bol_last_offset , bp_offset - , ep_offset ) (loc : Loc.t) = - { loc with - line_nb = loc.line_nb + line_offset - ; bol_pos = loc.bol_pos + bol_offset - ; line_nb_last = loc.line_nb_last + line_last_offset - ; bol_pos_last = loc.bol_pos_last + bol_last_offset - ; bp = loc.bp + bp_offset - ; ep = loc.ep + ep_offset - } - -let adjust_offset ~stm_loc ~cached_loc res = - let offset = loc_offset cached_loc stm_loc in - let f = loc_apply_offset offset in - Coq.Protect.E.map_loc ~f res - -let interp_command ~st stm : _ Stats.t = - let stm_loc = Coq.Ast.loc stm |> Option.get in - match in_cache st stm with - | Some (cached_loc, res), time -> - if Debug.cache then Io.Log.trace "memo" "cache hit"; - CacheStats.hit (); - let res = adjust_offset ~stm_loc ~cached_loc res in - Stats.make ~cache_hit:true ~time res - | 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 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 (stm, st) (stm_loc, res) in + , ep_offset ) + + let loc_apply_offset + ( line_offset + , bol_offset + , line_last_offset + , bol_last_offset + , bp_offset + , ep_offset ) (loc : Loc.t) = + { loc with + line_nb = loc.line_nb + line_offset + ; bol_pos = loc.bol_pos + bol_offset + ; line_nb_last = loc.line_nb_last + line_last_offset + ; bol_pos_last = loc.bol_pos_last + bol_last_offset + ; bp = loc.bp + bp_offset + ; ep = loc.ep + ep_offset + } + + let adjust_offset ~stm_loc ~cached_loc res = + let offset = loc_offset cached_loc stm_loc in + let f = loc_apply_offset offset in + Coq.Protect.E.map_loc ~f res + + let eval (st, stm) : _ Stats.t = + let stm_loc = Coq.Ast.loc stm |> Option.get in + match in_cache st stm with + | Some (cached_loc, res), time -> + if Debug.cache then Io.Log.trace "memo" "cache hit"; + CacheStats.hit (); + let res = adjust_offset ~stm_loc ~cached_loc res in + Stats.make ~cache_hit:true ~time res + | 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 time = time_hash +. time_interp in - Stats.make ~time res) - -module AC = Hashtbl.Make (Coq.State) - -let admit_cache = AC.create 1000 - -let interp_admitted ~st = - match AC.find_opt admit_cache st with - | None -> - let admitted_st = Coq.State.admit ~st in - AC.add admit_cache st admitted_st; - admitted_st - | Some admitted_st -> admitted_st - -let mem_stats () = Obj.reachable_words (Obj.magic cache) - -(* let _hashtbl_out oc t = () *) -(* Marshal.to_channel oc (HC.length t) []; *) -(* HC.iter *) -(* (fun vi res -> *) -(* VernacInput.marshal_out oc vi; *) -(* Result.marshal_out oc res) *) -(* t *) - -(* let _hashtbl_in ic = *) -(* let ht = HC.create 1000 in *) -(* let count : int = Marshal.from_channel ic in *) -(* for _i = 0 to count - 1 do *) -(* let vi = VernacInput.marshal_in ic in *) -(* let res = Result.marshal_in ic in *) -(* HC.add ht vi res *) -(* done; *) -(* ht *) - -let load_from_disk ~file = - let ic = open_in_bin file in - (* let in_cache : cache = hashtbl_in in_c in *) - let in_cache : cache = Marshal.from_channel ic in - cache := in_cache; - close_in ic - -let save_to_disk ~file = - let oc = open_out_bin file in - let out_cache : cache = !cache in - Marshal.to_channel oc out_cache []; - (* hashtbl_out out_c out_cache; *) - close_out oc + 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) +end + +module Admit = struct + type t = Coq.State.t + + module AC = Hashtbl.Make (Coq.State) + + let admit_cache = AC.create 1000 + + let eval st = + match AC.find_opt admit_cache st with + | None -> + let admitted_st = Coq.State.admit ~st in + AC.add admit_cache st admitted_st; + admitted_st + | Some admitted_st -> admitted_st +end diff --git a/fleche/memo.mli b/fleche/memo.mli index ad7098a3..61cf83cb 100644 --- a/fleche/memo.mli +++ b/fleche/memo.mli @@ -7,24 +7,26 @@ module Stats : sig } end -(** Interpret a command, possibly memoizing it *) -val interp_command : - st:Coq.State.t -> Coq.Ast.t -> Coq.State.t Coq.Interp.interp_result Stats.t +module Interp : sig + type t = Coq.State.t * Coq.Ast.t -val interp_admitted : st:Coq.State.t -> (Coq.State.t, Loc.t) Coq.Protect.E.t + (** Interpret a command, possibly memoizing it *) + val eval : t -> Coq.State.t Coq.Interp.interp_result Stats.t -(** Stats *) -val mem_stats : unit -> int + (** Stats *) + val stats : unit -> int -module CacheStats : sig - val reset : unit -> unit - val stats : unit -> string + (** debug *) + val input_info : t -> string end -(** Not working yet *) -val load_from_disk : file:string -> unit +module Admit : sig + type t = Coq.State.t -val save_to_disk : file:string -> unit + val eval : t -> (Coq.State.t, Loc.t) Coq.Protect.E.t +end -(** debug *) -val input_info : Coq.Ast.t * Coq.State.t -> string +module CacheStats : sig + val reset : unit -> unit + val stats : unit -> string +end From dbbbf72ac281a7a605210449f01cc5ca262d050c Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 18 Feb 2023 19:13:53 +0100 Subject: [PATCH 2/3] [coq] [cleanup] Remove [Coq.Interp.Info.t] This doesn't seem useful anymore. --- coq/interp.ml | 11 ++--------- coq/interp.mli | 6 +----- fleche/doc.ml | 6 ++---- 3 files changed, 5 insertions(+), 18 deletions(-) diff --git a/coq/interp.ml b/coq/interp.ml index fbd23842..b0de33ff 100644 --- a/coq/interp.ml +++ b/coq/interp.ml @@ -15,18 +15,11 @@ (* Written by: Emilio J. Gallego Arias *) (************************************************************************) -module Info = struct - type 'a t = { res : 'a } -end - -type 'a interp_result = ('a Info.t, Loc.t) Protect.E.t +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 Vernacinterp.interp ~st cmd |> State.of_coq -let interp ~st cmd = - Protect.eval cmd ~f:(fun cmd -> - let res = coq_interp ~st cmd in - { Info.res }) +let interp ~st cmd = Protect.eval cmd ~f:(coq_interp ~st) diff --git a/coq/interp.mli b/coq/interp.mli index f93cf3fb..74a40ae2 100644 --- a/coq/interp.mli +++ b/coq/interp.mli @@ -15,10 +15,6 @@ (* Written by: Emilio J. Gallego Arias *) (************************************************************************) -module Info : sig - type 'a t = { res : 'a } -end - -type 'a interp_result = ('a Info.t, Loc.t) Protect.E.t +type 'a interp_result = ('a, Loc.t) Protect.E.t val interp : st:State.t -> Ast.t -> State.t interp_result diff --git a/fleche/doc.ml b/fleche/doc.ml index 30fb40cd..d9c159ec 100644 --- a/fleche/doc.ml +++ b/fleche/doc.ml @@ -447,9 +447,7 @@ let state_recovery_heuristic doc st v = | Vernacexpr.VernacBullet _ | Vernacexpr.VernacEndSubproof -> Io.Log.trace "recovery" "bullet"; Coq.State.admit_goal ~st - |> Coq.Protect.E.bind ~f:(fun st -> - Coq.Interp.interp ~st v.v - |> Coq.Protect.E.map ~f:(fun { Coq.Interp.Info.res } -> res)) + |> Coq.Protect.E.bind ~f:(fun st -> Coq.Interp.interp ~st v.v) | _ -> Coq.Protect.E.ok st let interp_and_info ~parsing_time ~st ast = @@ -559,7 +557,7 @@ let recovery_interp ~doc ~st ~ast = let node_of_coq_result ~doc ~range ~ast ~st ~parsing_diags ~parsing_feedback ~feedback ~info last_tok res = match res with - | Ok { Coq.Interp.Info.res = state } -> + | Ok state -> let node = parsed_node ~range ~ast ~state ~parsing_diags ~parsing_feedback ~diags:[] ~feedback ~info From 764222e997c3eefb22fc6fcf981aae34fa87a6e1 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 18 Feb 2023 19:28:39 +0100 Subject: [PATCH 3/3] [fleche] Cache document creation Some clients, such as Visual Studio Code, may open / close buffers aggressively when working, this creates some extra load as we don't cache document creation. This PR does cache it. In general this has a very low footprint on memory by itself, as the root state is shared across all buffers, but of course, the documents themselves could be a big load, but that's already the case so we don't make things worse. Fixes #363 [Test suite passes ;)] --- coq/workspace.ml | 3 +++ coq/workspace.mli | 6 ++++++ fleche/doc.ml | 7 ++++--- fleche/doc.mli | 2 +- fleche/memo.ml | 44 ++++++++++++++++++++++++++++++++++++++------ fleche/memo.mli | 6 ++++++ lang/lUri.ml | 2 ++ lang/lUri.mli | 6 ++++++ 8 files changed, 66 insertions(+), 10 deletions(-) diff --git a/coq/workspace.ml b/coq/workspace.ml index 7b0b0778..8559dde2 100644 --- a/coq/workspace.ml +++ b/coq/workspace.ml @@ -27,6 +27,9 @@ type t = ; debug : bool } +let hash = Hashtbl.hash +let compare = Stdlib.compare + (* Lib setup, XXX unify with sysinit *) let coq_root = Names.DirPath.make [ Libnames.coq_root ] let default_root = Libnames.default_root_prefix diff --git a/coq/workspace.mli b/coq/workspace.mli index 9a357f99..9cfa8cf6 100644 --- a/coq/workspace.mli +++ b/coq/workspace.mli @@ -27,6 +27,12 @@ type t = private ; debug : bool (** Enable backtraces *) } +(** compare *) +val compare : t -> t -> int + +(** hash *) +val hash : t -> int + (** user message, debug extra data *) val describe : t -> string * string diff --git a/fleche/doc.ml b/fleche/doc.ml index d9c159ec..02655285 100644 --- a/fleche/doc.ml +++ b/fleche/doc.ml @@ -207,9 +207,7 @@ type t = ; completed : Completion.t } -let mk_doc root_state workspace uri = - Coq.Init.doc_init ~root_state ~workspace ~uri - +(* Flatten the list of document asts *) let asts doc = List.filter_map Node.ast doc.nodes (* TOC handling *) @@ -248,6 +246,9 @@ let process_init_feedback ~stats range state messages = [ { Node.range; ast = None; state; diags; messages; info } ] else [] +(* Memoized call to [Coq.Init.doc_init] *) +let mk_doc root_state workspace uri = Memo.Init.eval (root_state, workspace, uri) + let create ~state ~workspace ~uri ~version ~contents = let () = Stats.reset () in let { Coq.Protect.E.r; feedback } = mk_doc state workspace uri in diff --git a/fleche/doc.mli b/fleche/doc.mli index bb10098c..fb624e2c 100644 --- a/fleche/doc.mli +++ b/fleche/doc.mli @@ -73,7 +73,7 @@ type t = private (** Return the list of all asts in the doc *) val asts : t -> Node.Ast.t list -(** Note, [create] calls Coq but it is not cached in the Memo.t table *) +(** Create a new Coq document, this is cached! *) val create : state:Coq.State.t -> workspace:Coq.Workspace.t diff --git a/fleche/memo.ml b/fleche/memo.ml index 5450920c..5e7620c8 100644 --- a/fleche/memo.ml +++ b/fleche/memo.ml @@ -135,15 +135,47 @@ end module Admit = struct type t = Coq.State.t - module AC = Hashtbl.Make (Coq.State) + module C = Hashtbl.Make (Coq.State) - let admit_cache = AC.create 1000 + let cache = C.create 1000 - let eval st = - match AC.find_opt admit_cache st with + let eval v = + match C.find_opt cache v with | None -> - let admitted_st = Coq.State.admit ~st in - AC.add admit_cache st admitted_st; + let admitted_st = Coq.State.admit ~st:v in + C.add cache v admitted_st; admitted_st | Some admitted_st -> admitted_st end + +module Init = struct + module S = struct + type t = Coq.State.t * Coq.Workspace.t * Lang.LUri.File.t + + let equal (s1, w1, u1) (s2, w2, u2) : bool = + if Lang.LUri.File.compare u1 u2 = 0 then + if Coq.Workspace.compare w1 w2 = 0 then + if Coq.State.compare s1 s2 = 0 then true else false + else false + else false + + let hash (st, w, uri) = + Hashtbl.hash + (Coq.State.hash st, Coq.Workspace.hash w, Lang.LUri.File.hash uri) + end + + type t = S.t + + module C = Hashtbl.Make (S) + + let cache = C.create 1000 + + let eval v = + match C.find_opt cache v with + | 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; + admitted_st + | Some res -> res +end diff --git a/fleche/memo.mli b/fleche/memo.mli index 61cf83cb..8f468e22 100644 --- a/fleche/memo.mli +++ b/fleche/memo.mli @@ -7,6 +7,12 @@ module Stats : sig } end +module Init : sig + type t = Coq.State.t * Coq.Workspace.t * Lang.LUri.File.t + + val eval : t -> (Coq.State.t, Loc.t) Coq.Protect.E.t +end + module Interp : sig type t = Coq.State.t * Coq.Ast.t diff --git a/lang/lUri.ml b/lang/lUri.ml index 856eadd9..37263402 100644 --- a/lang/lUri.ml +++ b/lang/lUri.ml @@ -21,4 +21,6 @@ module File = struct let to_string_uri { uri; _ } = Uri.to_string uri let to_string_file { file; _ } = file let extension { file; _ } = Filename.extension file + let hash = Hashtbl.hash + let compare = Stdlib.compare end diff --git a/lang/lUri.mli b/lang/lUri.mli index 13a882bf..0c2430ce 100644 --- a/lang/lUri.mli +++ b/lang/lUri.mli @@ -27,4 +27,10 @@ module File : sig (** Filename version, fit for OS functions *) val to_string_file : t -> string + + (** compare *) + val compare : t -> t -> int + + (** hash *) + val hash : t -> int end