add -profile-lazy

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
 

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

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,21 +1358,24 @@ 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 =
   let open CClosure.RecordedSteps in
   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

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

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

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;

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;