From 68b749895b2d28de528602c270f6999526e841a0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 16 Dec 2024 14:50:51 +0100 Subject: [PATCH] add -profile-lazy --- kernel/cClosure.ml | 44 +++++++++++++++++++++++++++----------- kernel/cClosure.mli | 3 +++ pretyping/reductionops.ml | 23 +++++++++++++------- pretyping/reductionops.mli | 2 ++ sysinit/coqargs.ml | 3 +++ sysinit/coqargs.mli | 1 + sysinit/coqinit.ml | 10 +++++++++ 7 files changed, 66 insertions(+), 20 deletions(-) diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 19354786e6e6..7de0ff923481 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -475,6 +475,8 @@ let add_step record : step_kind -> unit = function | Match -> record.matches <- 1 + record.matches | Fix -> record.fixpoints <- 1 + record.fixpoints +let global_steps = ref None + type clos_tab = { tab : Table.t; recorded_steps : recorded_steps RedContextTbl.t option; @@ -520,6 +522,13 @@ module RecordedSteps = struct | None -> false | Some record -> RedContextTbl.length record > 0 + let globally_record_steps () = global_steps := Some (RedContextTbl.create 57) + + let get_global_steps () = + match !global_steps with + | None -> [] + | Some record -> RedContextTbl.to_seq record |> Seq.map (on_snd copy) |> List.of_seq + let get_recorded_steps tab = match tab.recorded_steps with | None -> [] @@ -1939,21 +1948,30 @@ let lazy_trace flag ctx = lazy_trace Pp.(fun () -> | None | Some [] -> str "top" | Some kns -> prlist_with_sep pr_comma GlobRef.print kns) +let record_step_in records flag ctx = + let record = match RedContextTbl.find_opt records ctx with + | Some record -> record + | None -> + let record = empty_recorded_steps () in + RedContextTbl.add records ctx record; + record + in + add_step record flag + let record_step tab flag ctx = - let () = match tab.recorded_steps with - | None -> () - | Some records -> + let () = match tab.recorded_steps, !global_steps with + | None, None -> () + | Some records, None | None, Some records -> + let num,denum = !RecordedSteps.sample_rate in + (* sample [num / denum] of the steps *) + if num = denum || Random.int denum < num then + record_step_in records flag ctx + | Some records1, Some records2 -> let num,denum = !RecordedSteps.sample_rate in (* sample [num / denum] of the steps *) if num = denum || Random.int denum < num then begin - let record = match RedContextTbl.find_opt records ctx with - | Some record -> record - | None -> - let record = empty_recorded_steps () in - RedContextTbl.add records ctx record; - record - in - add_step record flag + record_step_in records1 flag ctx; + record_step_in records2 flag ctx end in lazy_trace flag ctx @@ -1975,7 +1993,9 @@ let push_context fl ctx v = v.ctx <- ctx let push_context tab fl ctx v = - if Option.is_empty tab.recorded_steps && not (CDebug.get_flag lazy_trace_flag) + if Option.is_empty !global_steps && + Option.is_empty tab.recorded_steps && + not (CDebug.get_flag lazy_trace_flag) then () else push_context fl ctx v diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 5f430d215fab..e4de31c7b471 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -166,6 +166,9 @@ module RecordedSteps : sig val get_recorded_steps : clos_tab -> (current_context * t) list + val globally_record_steps : unit -> unit + + val get_global_steps : unit -> (current_context * t) list end val info_env : clos_infos -> env diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 3d977c9c8fab..7f9976c37582 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1302,6 +1302,10 @@ let process_steps steps = let inherited = RedContextMap.bindings inherited in total, steps, inherited +let safe_pr_global gr = + try Nametab.pr_global_env Id.Set.empty gr + with Not_found -> GlobRef.print gr + let to_table header total steps = let open Pp in let pr_row (ctx, (steps:CClosure.RecordedSteps.t)) = @@ -1310,7 +1314,7 @@ let to_table header total steps = | Some ctx -> hov 2 (prlist_with_sep (fun () -> spc() ++ str "in ") - (Nametab.pr_global_env Id.Set.empty) + safe_pr_global ctx) in let pp_flag get = @@ -1354,6 +1358,15 @@ let print_conversion_steps left right = let () = Conversion.dbg_msg := print_conversion_steps +let format_steps steps = + let open Pp in + let total, steps, inherited = process_steps steps in + let rate = pp_sample_rate !CClosure.RecordedSteps.sample_rate in + pr_opt (fun rate -> str "sample rate: " ++ str rate) rate ++ + to_table "individual" total steps ++ fnl() ++ + fnl() ++ + to_table "inherited" total inherited + (* future work: print percentages, print step counts in children nicer formatting (some kind of table?) *) let print_recorded_steps tab = @@ -1361,14 +1374,8 @@ let print_recorded_steps tab = if not @@ has_recorded_steps tab then () else print_recorded_steps @@ fun () -> - let open Pp in let steps = get_recorded_steps tab in - let total, steps, inherited = process_steps steps in - let rate = pp_sample_rate !CClosure.RecordedSteps.sample_rate in - pr_opt (fun rate -> str "sample rate: " ++ str rate) rate ++ - to_table "individual" total steps ++ fnl() ++ - fnl() ++ - to_table "inherited" total inherited + format_steps steps (* lazy reduction functions. The infos must be created for each term *) (* Note by HH [oct 08] : why would it be the job of clos_norm_flags to add diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 721559fb1db2..da67d3b1a4df 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -318,6 +318,8 @@ exception AnomalyInConversion of exn (* inferred_universes just gathers the constraints. *) val inferred_universes : (UGraph.t * Univ.Constraints.t, UGraph.univ_inconsistency) Conversion.universe_compare +val format_steps : (CClosure.current_context * CClosure.RecordedSteps.t) list -> Pp.t + (** Deprecated *) val splay_prod : env -> evar_map -> constr -> (Name.t EConstr.binder_annot * constr) list * constr diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml index c365625600d1..8e8483bb1ac6 100644 --- a/sysinit/coqargs.ml +++ b/sysinit/coqargs.ml @@ -68,6 +68,7 @@ type coqargs_config = { beautify : bool; quiet : bool; time : time_config option; + profile_lazy : bool; test_mode : bool; profile : string option; print_emacs : bool; @@ -136,6 +137,7 @@ let default_config = { beautify = false; quiet = false; time = None; + profile_lazy = false; test_mode = false; profile = None; print_emacs = false; @@ -413,6 +415,7 @@ let parse_args ~init arglist : t * string list = |"-time" -> { oval with config = { oval.config with time = Some ToFeedback }} |"-time-file" -> { oval with config = { oval.config with time = Some (ToFile (next())) }} | "-profile" -> { oval with config = { oval.config with profile = Some (next()) } } + | "-profile-lazy" -> { oval with config = { oval.config with profile_lazy = true } } |"-type-in-type" -> set_logic (fun o -> { o with type_in_type = true }) oval |"-unicode" -> add_vo_require oval "Utf8_core" None (Some Import) |"-where" -> set_query oval PrintWhere diff --git a/sysinit/coqargs.mli b/sysinit/coqargs.mli index 0a550b76d584..7dff1c1e9d39 100644 --- a/sysinit/coqargs.mli +++ b/sysinit/coqargs.mli @@ -63,6 +63,7 @@ type coqargs_config = { beautify : bool; quiet : bool; time : time_config option; + profile_lazy : bool; test_mode : bool; profile : string option; print_emacs : bool; diff --git a/sysinit/coqinit.ml b/sysinit/coqinit.ml index 709b41af5189..3c60a94f6608 100644 --- a/sysinit/coqinit.ml +++ b/sysinit/coqinit.ml @@ -171,10 +171,20 @@ let init_profile ~file = NewProfile.finish (); close_out ch) +let init_profile_lazy () = + CClosure.RecordedSteps.globally_record_steps (); + at_exit (fun () -> + let steps = CClosure.RecordedSteps.get_global_steps () in + if CList.is_empty steps then () + else + let pp = Reductionops.format_steps steps in + Feedback.msg_info pp) + let init_runtime ~usage opts = let open Coqargs in Vernacextend.static_linking_done (); Option.iter (fun file -> init_profile ~file) opts.config.profile; + if opts.config.profile_lazy then init_profile_lazy (); Lib.init (); init_coqlib opts; if opts.post.memory_stat then at_exit print_memory_stat;