From 14c1b9b2e072d77febc628edcadb262b9236ab24 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Wed, 24 May 2023 13:16:40 +0200
Subject: [PATCH 01/11] NewProfile produces google trace format

display using https://profiler.firefox.com/
or https://ui.perfetto.dev/
(or in chrome's builtin display but I didn't test it)
---
 lib/newProfile.ml  | 136 +++++++++++++++++++++++++++++++++++++++++++++
 lib/newProfile.mli |  27 +++++++++
 2 files changed, 163 insertions(+)
 create mode 100644 lib/newProfile.ml
 create mode 100644 lib/newProfile.mli

diff --git a/lib/newProfile.ml b/lib/newProfile.ml
new file mode 100644
index 000000000000..e487ab65d8a2
--- /dev/null
+++ b/lib/newProfile.ml
@@ -0,0 +1,136 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+type settings =
+  { file : string
+  }
+
+type accu =
+  | No
+  | File of out_channel
+
+let accu = ref No
+
+let pid = Unix.getpid()
+
+let is_profiling () = !accu <> No
+
+let f fmt = match !accu with
+  | No -> assert false
+  | File ch -> Printf.fprintf ch fmt
+
+module MiniJson = struct
+  type t =
+    | String of string
+    | Int of string (* string not int so that we can have large ints *)
+    | Record of (string * t) list
+    | Array of t list
+
+  let rec pr ch = function
+    | String s ->
+      let s = String.split_on_char '"' s in
+      let s = String.concat "\\\"" s in
+      Printf.fprintf ch "\"%s\"" s
+    | Int s -> Printf.fprintf ch "%s" s
+    | Record elts ->
+      Printf.fprintf ch "{ %a }" prrecord elts
+    | Array elts ->
+      Printf.fprintf ch "[\n%a\n]" prarray elts
+
+  and prrecord ch = function
+    | [] -> ()
+    | [(x,v)] -> Printf.fprintf ch "\"%s\": %a" x pr v
+    | (x,v) :: l -> Printf.fprintf ch "\"%s\": %a, %a" x pr v prrecord l
+
+  and prarray ch = function
+    | [] -> ()
+    | [x] -> pr ch x
+    | x :: l -> Printf.fprintf ch "%a,\n%a" pr x prarray l
+
+
+  let pids = string_of_int pid
+  let base = [("pid", Int pids); ("tid", Int pids)]
+
+  let duration ~name ~ph ~ts ?args () =
+    let l = ("name", String name) :: ("ph", String ph) :: ("ts", Int ts) :: base in
+    let l = match args with
+      | None -> l
+      | Some args -> ("args", args) :: l
+    in
+    Record l
+end
+
+let prtime () =
+  let t = Unix.gettimeofday() in
+  Printf.sprintf "%.0f" (t *. 1E6)
+
+let global_start = prtime()
+let global_start_stat = Gc.quick_stat()
+
+let duration_gen ?time name ph ?args last () =
+  let time = match time with None -> prtime() | Some t -> t in
+  f "%a%s\n" MiniJson.pr (MiniJson.duration ~name ~ph ~ts:time ?args ()) last
+
+let duration ?time name ph ?args () = duration_gen ?time name ph ?args "," ()
+let enter ?time name ?args () = duration ?time name "B" ?args  ()
+let leave ?time name ?args () = duration ?time name "E" ?args ()
+
+let make_mem_diff ~(mstart:Gc.stat) ~(mend:Gc.stat) =
+  (* XXX we could use memprof to get sampling stats instead?
+     eg stats about how much of the allocation was collected
+     in the same span vs how much survived it *)
+  let major = mend.major_words -. mstart.major_words in
+  let minor = mend.minor_words -. mstart.minor_words in
+  let pp tdiff = MiniJson.String (Printf.sprintf "%.3G w" tdiff) in
+  MiniJson.Record [("major",pp major); ("minor", pp minor)]
+
+let profile name ?args f () =
+  if not (is_profiling ()) then f ()
+  else begin
+    let args = Option.map (fun f -> f()) args in
+    enter name ?args ();
+    let mstart = Gc.quick_stat () in
+    let v = try f ()
+      with e ->
+        let e = Exninfo.capture e in
+        let mend = Gc.quick_stat () in
+        let args = make_mem_diff ~mstart ~mend in
+        leave name ~args ();
+        Exninfo.iraise e
+    in
+    let mend = Gc.quick_stat () in
+    let args = make_mem_diff ~mstart ~mend in
+    leave name ~args ();
+    v
+  end
+
+let init opts =
+  let () = assert (not (is_profiling())) in
+  match opts with
+  | None ->
+    accu := No
+  | Some { file } ->
+    let ch = open_out file in
+    accu := File ch;
+    f "{ \"traceEvents\": [\n";
+    enter ~time:global_start "process" ();
+    enter ~time:global_start "init" ();
+    leave "init" ~args:(make_mem_diff ~mstart:global_start_stat ~mend:(Gc.quick_stat())) ()
+
+let finish () = match !accu with
+  | No -> ()
+  | File ch ->
+    duration_gen "process" "E" ""
+      ~args:(make_mem_diff ~mstart:global_start_stat ~mend:(Gc.quick_stat()))
+      ();
+    Printf.fprintf ch "],\n\"displayTimeUnit\": \"us\" }";
+    close_out ch
+
+let () = at_exit finish
diff --git a/lib/newProfile.mli b/lib/newProfile.mli
new file mode 100644
index 000000000000..18705afb70fd
--- /dev/null
+++ b/lib/newProfile.mli
@@ -0,0 +1,27 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+module MiniJson : sig
+  type t =
+    | String of string
+    | Int of string (* string not int so that we can have large ints *)
+    | Record of (string * t) list
+    | Array of t list
+end
+
+val profile : string -> ?args:(unit -> MiniJson.t) -> (unit -> 'a) -> unit -> 'a
+
+val is_profiling : unit -> bool
+
+type settings =
+  { file : string
+  }
+
+val init : settings option -> unit

From e3f0c9e643edf682682f456281701942215b1619 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Wed, 24 May 2023 13:17:03 +0200
Subject: [PATCH 02/11] add NewProfile calls

---
 interp/constrintern.ml   |  4 +++-
 kernel/conversion.ml     | 19 ++++++++++---------
 kernel/typeops.ml        |  6 ++++++
 kernel/vars.ml           |  5 +++++
 kernel/vconv.ml          |  7 ++++++-
 library/global.ml        | 13 +++++++++----
 pretyping/evarconv.ml    |  5 +++++
 pretyping/pretyping.ml   |  5 +++++
 sysinit/coqargs.ml       |  3 +++
 sysinit/coqargs.mli      |  1 +
 sysinit/coqinit.ml       |  1 +
 tactics/class_tactics.ml |  6 ++++--
 toplevel/vernac.ml       | 13 ++++++++++---
 vernac/vernacinterp.ml   | 10 ++++++----
 vernac/vernacstate.ml    | 14 ++++++++++----
 15 files changed, 84 insertions(+), 28 deletions(-)

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 2259f0e06d7a..542dc5f588d8 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2585,7 +2585,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
       a :: (intern_args env subscopes args)
 
   in
-  intern env c
+  NewProfile.profile "intern" (fun () ->
+      intern env c)
+    ()
 
 (**************************************************************************)
 (* Functions to translate constr_expr into glob_constr                    *)
diff --git a/kernel/conversion.ml b/kernel/conversion.ml
index d8d5dfc1202e..39c8329eabd0 100644
--- a/kernel/conversion.ml
+++ b/kernel/conversion.ml
@@ -864,15 +864,16 @@ and convert_list l2r infos lft1 lft2 v1 v2 cuniv = match v1, v2 with
 | _, _ -> raise NotConvertible
 
 let clos_gen_conv trans cv_pb l2r evars env graph univs t1 t2 =
-  let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in
-  let infos = create_conv_infos ~univs:graph ~evars reds env in
-  let infos = {
-    cnv_inf = infos;
-    lft_tab = create_tab ();
-    rgt_tab = create_tab ();
-  } in
-  ccnv cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs
-
+  NewProfile.profile "Conversion" (fun () ->
+      let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in
+      let infos = create_conv_infos ~univs:graph ~evars reds env in
+      let infos = {
+        cnv_inf = infos;
+        lft_tab = create_tab ();
+        rgt_tab = create_tab ();
+      } in
+      ccnv cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs)
+    ()
 
 let check_eq univs u u' =
   if not (UGraph.check_eq_sort univs u u') then raise NotConvertible
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 2a5720bfeaa0..5798f7d31136 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -853,6 +853,9 @@ and execute_array env cs =
   let cs = Array.Smart.map_i (fun i c -> let c, ty = execute env c in tys.(i) <- ty; c) cs in
   cs, tys
 
+let execute env c =
+  NewProfile.profile "Typeops.infer" (fun () -> execute env c) ()
+
 (* Derived functions *)
 
 let check_wellformed_universes env c =
@@ -861,6 +864,9 @@ let check_wellformed_universes env c =
   with UGraph.UndeclaredLevel u ->
     error_undeclared_universe env u
 
+let check_wellformed_universes env c =
+  NewProfile.profile "check-wf-univs" (fun () -> check_wellformed_universes env c) ()
+
 let infer env constr =
   let () = check_wellformed_universes env constr in
   let constr, t = execute env constr in
diff --git a/kernel/vars.ml b/kernel/vars.ml
index 5195e24b9701..2803a38359c4 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -409,3 +409,8 @@ let universes_of_constr c =
       Constr.fold aux s c
     | _ -> Constr.fold aux s c
   in aux Level.Set.empty c
+
+let universes_of_constr c =
+  NewProfile.profile "universes_of_constr" (fun () ->
+      universes_of_constr c)
+    ()
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 739444b62b8f..8f9c27cd8dc6 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -223,4 +223,9 @@ let vm_conv cv_pb env t1 t2 =
   in
   if not b then
     let state = (univs, checked_universes) in
-    let _ = vm_conv_gen cv_pb Genlambda.empty_evars env state t1 t2 in ()
+    let _ : UGraph.t =
+      NewProfile.profile "vm_conv" (fun () ->
+          vm_conv_gen cv_pb Genlambda.empty_evars env state t1 t2)
+        ()
+    in
+    ()
diff --git a/library/global.ml b/library/global.ml
index abaf85918bdb..6a45bb45cdfe 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -50,18 +50,23 @@ let env () = Safe_typing.env_of_safe_env (safe_env ())
 
 (** Turn ops over the safe_environment state monad to ops on the global env *)
 
-let globalize0 f = GlobalSafeEnv.set_safe_env (f (safe_env ()))
+let prof f () =
+  NewProfile.profile "kernel" f ()
+
+let globalize0 f = prof (fun () -> GlobalSafeEnv.set_safe_env (f (safe_env ()))) ()
 
 let globalize f =
-  let res,env = f (safe_env ()) in GlobalSafeEnv.set_safe_env env; res
+  prof (fun () ->
+      let res,env = f (safe_env ()) in GlobalSafeEnv.set_safe_env env; res)
+    ()
 
 let globalize0_with_summary fs f =
-  let env = f (safe_env ()) in
+  let env = prof (fun () -> f (safe_env ())) () in
   Summary.Interp.unfreeze_summaries fs;
   GlobalSafeEnv.set_safe_env env
 
 let globalize_with_summary fs f =
-  let res,env = f (safe_env ()) in
+  let res,env = prof (fun () -> f (safe_env ())) () in
   Summary.Interp.unfreeze_summaries fs;
   GlobalSafeEnv.set_safe_env env;
   res
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 48c79520f4a4..83d93ac53294 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1859,6 +1859,11 @@ let solve_unif_constraints_with_heuristics env
 
 exception UnableToUnify of evar_map * unification_error
 
+let evar_conv_x flags env evd pb x1 x2 : unification_result =
+  NewProfile.profile "unification" (fun () ->
+      evar_conv_x flags env evd pb x1 x2)
+    ()
+
 let unify_delay ?flags env evd t1 t2 =
   let flags =
     match flags with
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e413b398dfa8..2fe9d2a26038 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1407,6 +1407,11 @@ let ise_pretype_gen (flags : inference_flags) env sigma lvar kind c =
   in
   process_inference_flags flags !!env sigma (sigma',c',c'_ty)
 
+let ise_pretype_gen flags env sigma lvar kind c : _ * _ * _ =
+  NewProfile.profile "pretyping" (fun () ->
+      ise_pretype_gen flags env sigma lvar kind c)
+    ()
+
 let default_inference_flags fail = {
   use_coercions = true;
   use_typeclasses = UseTC;
diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml
index 8b46328a59e7..f019b184e9bf 100644
--- a/sysinit/coqargs.ml
+++ b/sysinit/coqargs.ml
@@ -66,6 +66,7 @@ type coqargs_config = {
   native_output_dir : CUnix.physical_path;
   native_include_dirs : CUnix.physical_path list;
   time        : time_config option;
+  profile : string option;
   print_emacs : bool;
 }
 
@@ -121,6 +122,7 @@ let default_config = {
   native_output_dir = ".coq-native";
   native_include_dirs = [];
   time         = None;
+  profile = None;
   print_emacs  = false;
 
   (* Quiet / verbosity options should be here *)
@@ -408,6 +410,7 @@ let parse_args ~usage ~init arglist : t * string list =
       oval
     |"-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()) } }
     |"-type-in-type" -> set_logic (fun o -> { o with type_in_type = true }) oval
     |"-unicode" -> add_vo_require oval "Utf8_core" None (Some Lib.Import)
     |"-where" -> set_query oval PrintWhere
diff --git a/sysinit/coqargs.mli b/sysinit/coqargs.mli
index 7900f1466d74..60dbffb8c087 100644
--- a/sysinit/coqargs.mli
+++ b/sysinit/coqargs.mli
@@ -58,6 +58,7 @@ type coqargs_config = {
   native_output_dir : CUnix.physical_path;
   native_include_dirs : CUnix.physical_path list;
   time        : time_config option;
+  profile : string option;
   print_emacs : bool;
 }
 
diff --git a/sysinit/coqinit.ml b/sysinit/coqinit.ml
index 68ca24a71457..03807750151c 100644
--- a/sysinit/coqinit.ml
+++ b/sysinit/coqinit.ml
@@ -146,6 +146,7 @@ let init_load_paths opts =
 let init_runtime opts =
   let open Coqargs in
   Vernacextend.static_linking_done ();
+  NewProfile.init (Option.map (fun file -> { NewProfile.file }) opts.config.profile);
   Lib.init ();
   init_coqlib opts;
   if opts.post.memory_stat then at_exit print_memory_stat;
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 011a49161813..688a5b7aea20 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1065,11 +1065,13 @@ module Search = struct
       ~depth ~dep:(unique || dep) hints in
     run_on_evars env evd p eauto_tac
 
-  let typeclasses_eauto env evd ?depth unique ~best_effort st hints p =
-    evars_eauto env evd depth true ~best_effort unique false st hints p
   (** Typeclasses eauto is an eauto which tries to resolve only
       goals of typeclass type, and assumes that the initially selected
       evars in evd are independent of the rest of the evars *)
+  let typeclasses_eauto env evd ?depth unique ~best_effort st hints p =
+    NewProfile.profile "typeclass search" (fun () ->
+        evars_eauto env evd depth true ~best_effort unique false st hints p)
+      ()
 
   let typeclasses_resolve env evd depth unique ~best_effort p =
     let db = searchtable_map typeclasses_db in
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 52e47824376d..1910926452be 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -105,8 +105,10 @@ let load_vernac_core ~echo ~check ~state ?source file =
   let rec loop state ids =
     let tstart = System.get_time () in
     match
-      Stm.parse_sentence
-        ~doc:state.doc ~entry:Pvernac.main_entry state.sid in_pa
+      NewProfile.profile "parse_command" (fun () ->
+          Stm.parse_sentence
+            ~doc:state.doc ~entry:Pvernac.main_entry state.sid in_pa)
+        ()
     with
     | None ->
       input_cleanup ();
@@ -119,7 +121,12 @@ let load_vernac_core ~echo ~check ~state ?source file =
 
       let state =
         try_finally
-          (fun () -> Flags.silently (interp_vernac ~check ~state) ast)
+          (fun () ->
+             NewProfile.profile "command"
+               ~args:(fun () ->
+                   Record [("cmd", String (Pp.string_of_ppcmds (Topfmt.pr_cmd_header ast)))])
+               (fun () ->
+             Flags.silently (interp_vernac ~check ~state) ast) ())
           ()
           (fun () ->
              let tend = System.get_time () in
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 95de8025fa78..7c13a6d2e84b 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -214,8 +214,8 @@ let interp_gen ~verbosely ~st ~interp_fn cmd =
 let interp ?(verbosely=true) ~st cmd =
   Vernacstate.unfreeze_full_state st;
   vernac_pperr_endline Pp.(fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr cmd.CAst.v.expr);
-  let entry = Synterp.synterp_control cmd in
-  let interp = interp_gen ~verbosely ~st ~interp_fn:interp_control entry in
+  let entry = NewProfile.profile "synterp" (fun () -> Synterp.synterp_control cmd) () in
+  let interp = NewProfile.profile "interp" (fun () -> interp_gen ~verbosely ~st ~interp_fn:interp_control entry) () in
   Vernacstate.{ synterp = Vernacstate.Synterp.freeze (); interp }
 
 let interp_entry ?(verbosely=true) ~st entry =
@@ -226,5 +226,7 @@ let interp_qed_delayed_proof ~proof ~st ~control (CAst.{loc; v = pe } as e) : Ve
   let cmd = CAst.make ?loc { control; expr = VernacSynPure (VernacEndProof pe); attrs = [] } in
   let CAst.{ loc; v = entry } = Synterp.synterp_control cmd in
   let control = entry.control in
-  interp_gen ~verbosely:false ~st
-    ~interp_fn:(interp_qed_delayed_control ~proof ~control) e
+  NewProfile.profile "interp-delayed-qed" (fun () ->
+      interp_gen ~verbosely:false ~st
+        ~interp_fn:(interp_qed_delayed_control ~proof ~control) e)
+    ()
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 50127a3903e2..8bc661a40eb9 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -198,8 +198,10 @@ let freeze_full_state () =
   }
 
 let unfreeze_full_state st =
-  Synterp.unfreeze st.synterp;
-  Interp.unfreeze_interp_state st.interp
+  NewProfile.profile "unfreeze_full_state" (fun () ->
+      Synterp.unfreeze st.synterp;
+      Interp.unfreeze_interp_state st.interp)
+    ()
 
 (* Compatibility module *)
 module Declare_ = struct
@@ -257,10 +259,14 @@ module Declare_ = struct
   let return_partial_proof () = cc Declare.Proof.return_partial_proof
 
   let close_future_proof ~feedback_id pf =
-    cc (fun pt -> Declare.Proof.close_future_proof ~feedback_id pt pf)
+    NewProfile.profile "close_future_proof" (fun () ->
+        cc (fun pt -> Declare.Proof.close_future_proof ~feedback_id pt pf))
+      ()
 
   let close_proof ~opaque ~keep_body_ucst_separate =
-    cc (fun pt -> Declare.Proof.close_proof ~opaque ~keep_body_ucst_separate pt)
+    NewProfile.profile "close_proof" (fun () ->
+        cc (fun pt -> Declare.Proof.close_proof ~opaque ~keep_body_ucst_separate pt))
+      ()
 
   let discard_all () = s_lemmas := None
   let update_sigma_univs ugraph = dd (Declare.Proof.update_sigma_univs ugraph)

From f167000be9c9dc50902aa6e166860b5004d4dced Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Wed, 24 May 2023 16:57:42 +0200
Subject: [PATCH 03/11] coq_makefile produces profile info when PROFILING set,
 bench sets it

profiles seem to compress well, for instance from profiling Hurkens:

- .vo: 48KB (for reference)
- .prof.json: 2.6MB
- .prof.json.gz: 144KB (compression level 6 (default))
- .prof.json.gz: 124KB (compression level 9 (best))
- .prof.json.xz: 108KB (compression level 6 (default); also 9)
- .prof.json.7z: 116KB
- .prof.json.zip: 124KB (compression level 9)

The chrome displayer supports importing straight from gzip so we use that.
---
 dev/bench/bench.sh         |  1 +
 dev/bench/gitlab-bench.yml |  2 ++
 tools/CoqMakefile.in       | 13 +++++++++++--
 3 files changed, 14 insertions(+), 2 deletions(-)

diff --git a/dev/bench/bench.sh b/dev/bench/bench.sh
index 49d76b484503..637ed13cb524 100755
--- a/dev/bench/bench.sh
+++ b/dev/bench/bench.sh
@@ -458,6 +458,7 @@ skipped_packages=
 
 # Generate per line timing info in devs that use coq_makefile
 export TIMING=1
+export PROFILING=1
 
 for coq_opam_package in $sorted_coq_opam_packages; do
 
diff --git a/dev/bench/gitlab-bench.yml b/dev/bench/gitlab-bench.yml
index cfae11e4948d..563bc5a5ae31 100644
--- a/dev/bench/gitlab-bench.yml
+++ b/dev/bench/gitlab-bench.yml
@@ -19,8 +19,10 @@ bench:
       - _bench/files.listing
       - _bench/opam.NEW/**/*.log
       - _bench/opam.NEW/**/*.timing
+      - _bench/opam.NEW/**/*.prof.json.gz
       - _bench/opam.OLD/**/*.log
       - _bench/opam.OLD/**/*.timing
+      - _bench/opam.OLD/**/*.prof.json.gz
     when: always
     expire_in: 1 year
   environment: bench
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 143b431a6f11..8275d2fc061e 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -307,6 +307,14 @@ else
   TIMING_ARG=
 endif
 
+ifneq (,$(PROFILING))
+  PROFILE_ARG=-profile $<.prof.json
+  PROFILE_ZIP=gzip $<.prof.json
+else
+  PROFILE_ARG=
+  PROFILE_ZIP=true
+endif
+
 # Files #######################################################################
 #
 # We here define a bunch of variables about the files being part of the
@@ -810,7 +818,7 @@ define globvorule=
 # take care to $$ variables using $< etc
   $(1).vo $(1).glob &: $(1).v | $(VDFILE)
 	$(SHOW)COQC $(1).v
-	$(HIDE)$$(TIMER) $(COQC) $(COQDEBUG) $$(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $(1).v
+	$(HIDE)$$(TIMER) $(COQC) $(COQDEBUG) $$(TIMING_ARG) $$(PROFILE_ARG) $(COQFLAGS) $(COQLIBS) $(1).v
 ifeq ($(COQDONATIVE), "yes")
 	$(SHOW)COQNATIVE $(1).vo
 	$(HIDE)$(call TIMER,$(1).vo.native) $(COQNATIVE) $(COQLIBS) $(1).vo
@@ -821,7 +829,8 @@ else
 
 $(VOFILES): %.vo: %.v | $(VDFILE)
 	$(SHOW)COQC $<
-	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $<
+	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(PROFILE_ARG) $(COQFLAGS) $(COQLIBS) $<
+	$(HIDE)$(PROFILE_ZIP)
 ifeq ($(COQDONATIVE), "yes")
 	$(SHOW)COQNATIVE $@
 	$(HIDE)$(call TIMER,$@.native) $(COQNATIVE) $(COQLIBS) $@

From 6c72e506c424eea0a2f94d12b7965a547c5cf82e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Fri, 26 May 2023 16:00:16 +0200
Subject: [PATCH 04/11] newprofile: include sum of times and call counts of
 subcategories in args

although this could be computed afterwards this makes it easier to
display

nb because we sum floats accuracy may be shit
---
 lib/newProfile.ml  | 62 ++++++++++++++++++++++++++++++++++++----------
 lib/newProfile.mli |  2 +-
 toplevel/vernac.ml |  2 +-
 3 files changed, 51 insertions(+), 15 deletions(-)

diff --git a/lib/newProfile.ml b/lib/newProfile.ml
index e487ab65d8a2..9721f46ed06d 100644
--- a/lib/newProfile.ml
+++ b/lib/newProfile.ml
@@ -62,25 +62,60 @@ module MiniJson = struct
     let l = ("name", String name) :: ("ph", String ph) :: ("ts", Int ts) :: base in
     let l = match args with
       | None -> l
-      | Some args -> ("args", args) :: l
+      | Some args -> ("args", Record args) :: l
     in
     Record l
 end
 
-let prtime () =
-  let t = Unix.gettimeofday() in
+let gettime = Unix.gettimeofday
+
+let gettimeopt = function
+  | Some t -> t
+  | None -> gettime()
+
+let prtime t =
   Printf.sprintf "%.0f" (t *. 1E6)
 
-let global_start = prtime()
+let global_start = gettime()
 let global_start_stat = Gc.quick_stat()
 
-let duration_gen ?time name ph ?args last () =
-  let time = match time with None -> prtime() | Some t -> t in
-  f "%a%s\n" MiniJson.pr (MiniJson.duration ~name ~ph ~ts:time ?args ()) last
-
-let duration ?time name ph ?args () = duration_gen ?time name ph ?args "," ()
-let enter ?time name ?args () = duration ?time name "B" ?args  ()
-let leave ?time name ?args () = duration ?time name "E" ?args ()
+let duration ~time name ph ?args ?(last=",") () =
+  f "%a%s\n" MiniJson.pr (MiniJson.duration ~name ~ph ~ts:(prtime time) ?args ()) last
+
+let sums = ref []
+
+let enter ?time name ?args ?last () =
+  let time = gettimeopt time in
+  sums := (time, CString.Map.empty) :: !sums;
+  duration ~time name "B" ?args ?last ()
+
+let leave ?time name ?(args=[]) ?last () =
+  let time = gettimeopt time in
+  let sum = match !sums with
+    | [] -> assert false
+    | [_,sum] -> sum
+    | (start, sum) :: (start', next) :: rest ->
+      let dur = time -. start in
+      let next = CString.Map.update name (function
+          | None -> Some (dur, 1)
+          | Some (dur', cnt) -> Some (dur +. dur', cnt+1))
+          next
+      in
+      let next = CString.Map.union (fun name' (l,cnt) (r,cnt') ->
+          if String.equal name name' then Some (r,cnt+cnt')
+          else Some (l +. r, cnt+cnt'))
+          sum next
+      in
+      sums := (start', next) :: rest;
+      sum
+  in
+  let sum = List.map (fun (name, (t, cnt)) ->
+      name, MiniJson.String
+        (Printf.sprintf "%.3G us, %d %s" (t *. 1E6) cnt (CString.plural cnt "call")))
+      (CString.Map.bindings sum)
+  in
+  let args = ("subtimes", MiniJson.Record sum) :: args in
+  duration ~time name "E" ~args ?last ()
 
 let make_mem_diff ~(mstart:Gc.stat) ~(mend:Gc.stat) =
   (* XXX we could use memprof to get sampling stats instead?
@@ -89,7 +124,7 @@ let make_mem_diff ~(mstart:Gc.stat) ~(mend:Gc.stat) =
   let major = mend.major_words -. mstart.major_words in
   let minor = mend.minor_words -. mstart.minor_words in
   let pp tdiff = MiniJson.String (Printf.sprintf "%.3G w" tdiff) in
-  MiniJson.Record [("major",pp major); ("minor", pp minor)]
+  [("major",pp major); ("minor", pp minor)]
 
 let profile name ?args f () =
   if not (is_profiling ()) then f ()
@@ -127,7 +162,8 @@ let init opts =
 let finish () = match !accu with
   | No -> ()
   | File ch ->
-    duration_gen "process" "E" ""
+    leave "process"
+      ~last:""
       ~args:(make_mem_diff ~mstart:global_start_stat ~mend:(Gc.quick_stat()))
       ();
     Printf.fprintf ch "],\n\"displayTimeUnit\": \"us\" }";
diff --git a/lib/newProfile.mli b/lib/newProfile.mli
index 18705afb70fd..28e2c07548a4 100644
--- a/lib/newProfile.mli
+++ b/lib/newProfile.mli
@@ -16,7 +16,7 @@ module MiniJson : sig
     | Array of t list
 end
 
-val profile : string -> ?args:(unit -> MiniJson.t) -> (unit -> 'a) -> unit -> 'a
+val profile : string -> ?args:(unit -> (string * MiniJson.t) list) -> (unit -> 'a) -> unit -> 'a
 
 val is_profiling : unit -> bool
 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 1910926452be..59667412165f 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -124,7 +124,7 @@ let load_vernac_core ~echo ~check ~state ?source file =
           (fun () ->
              NewProfile.profile "command"
                ~args:(fun () ->
-                   Record [("cmd", String (Pp.string_of_ppcmds (Topfmt.pr_cmd_header ast)))])
+                   [("cmd", String (Pp.string_of_ppcmds (Topfmt.pr_cmd_header ast)))])
                (fun () ->
              Flags.silently (interp_vernac ~check ~state) ast) ())
           ()

From 67a44fd7d2bd6db9198eca84ab1c65c85e0c568c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Fri, 16 Jun 2023 14:33:09 +0200
Subject: [PATCH 05/11] newprofile: filter components to print events for using
 COQ_PROFILE_COMPONENTS

This interacts a bit weirdly with the minimum duration based skip, but
maybe I'll remove the skip if this works well enough.
---
 dev/bench/bench.sh |  1 +
 lib/newProfile.ml  | 46 +++++++++++++++++++++++++++++++++++++---------
 2 files changed, 38 insertions(+), 9 deletions(-)

diff --git a/dev/bench/bench.sh b/dev/bench/bench.sh
index 637ed13cb524..c644a6d953b5 100755
--- a/dev/bench/bench.sh
+++ b/dev/bench/bench.sh
@@ -459,6 +459,7 @@ skipped_packages=
 # Generate per line timing info in devs that use coq_makefile
 export TIMING=1
 export PROFILING=1
+export COQ_PROFILE_COMPONENTS=command,parse_command
 
 for coq_opam_package in $sorted_coq_opam_packages; do
 
diff --git a/lib/newProfile.ml b/lib/newProfile.ml
index 9721f46ed06d..4c3b05adba55 100644
--- a/lib/newProfile.ml
+++ b/lib/newProfile.ml
@@ -84,16 +84,20 @@ let duration ~time name ph ?args ?(last=",") () =
 
 let sums = ref []
 
-let enter ?time name ?args ?last () =
+let enter_sums ?time () =
   let time = gettimeopt time in
-  sums := (time, CString.Map.empty) :: !sums;
-  duration ~time name "B" ?args ?last ()
+  sums := (time, CString.Map.empty) :: !sums
 
-let leave ?time name ?(args=[]) ?last () =
+let enter ?time name ?args () =
+  let time = gettimeopt time in
+  enter_sums ~time ();
+  duration ~time name "B" ?args ()
+
+let leave_sums ?time name () =
   let time = gettimeopt time in
-  let sum = match !sums with
+  match !sums with
     | [] -> assert false
-    | [_,sum] -> sum
+    | [start,sum] -> sums := []; sum, time -. start
     | (start, sum) :: (start', next) :: rest ->
       let dur = time -. start in
       let next = CString.Map.update name (function
@@ -107,8 +111,11 @@ let leave ?time name ?(args=[]) ?last () =
           sum next
       in
       sums := (start', next) :: rest;
-      sum
-  in
+      sum, dur
+
+let leave ?time name ?(args=[]) ?last () =
+  let time = gettimeopt time in
+  let sum, dur = leave_sums ~time name () in
   let sum = List.map (fun (name, (t, cnt)) ->
       name, MiniJson.String
         (Printf.sprintf "%.3G us, %d %s" (t *. 1E6) cnt (CString.plural cnt "call")))
@@ -126,9 +133,19 @@ let make_mem_diff ~(mstart:Gc.stat) ~(mend:Gc.stat) =
   let pp tdiff = MiniJson.String (Printf.sprintf "%.3G w" tdiff) in
   [("major",pp major); ("minor", pp minor)]
 
+(* NB: "process" and "init" are unconditional because they don't go
+   through [profile] and I'm too lazy to make them conditional *)
+let components =
+  match Sys.getenv_opt "COQ_PROFILE_COMPONENTS" with
+  | None -> CString.Pred.full
+  | Some s ->
+    List.fold_left (fun cs c -> CString.Pred.add c cs)
+      CString.Pred.empty
+      (String.split_on_char ',' s)
+
 let profile name ?args f () =
   if not (is_profiling ()) then f ()
-  else begin
+  else if CString.Pred.mem name components then begin
     let args = Option.map (fun f -> f()) args in
     enter name ?args ();
     let mstart = Gc.quick_stat () in
@@ -145,6 +162,17 @@ let profile name ?args f () =
     leave name ~args ();
     v
   end
+  else begin
+    enter_sums ();
+    let v = try f ()
+      with e ->
+        let e = Exninfo.capture e in
+        ignore (leave_sums name () : _ * _);
+        Exninfo.iraise e
+    in
+    ignore (leave_sums name () : _ * _);
+    v
+  end
 
 let init opts =
   let () = assert (not (is_profiling())) in

From 306cdb7f95715bc289daab9216d4f729599a0b65 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Fri, 16 Jun 2023 16:14:27 +0200
Subject: [PATCH 06/11] newprofile: include line number for "command" component
 extra data

---
 toplevel/vernac.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 59667412165f..c224c360bd32 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -124,7 +124,12 @@ let load_vernac_core ~echo ~check ~state ?source file =
           (fun () ->
              NewProfile.profile "command"
                ~args:(fun () ->
-                   [("cmd", String (Pp.string_of_ppcmds (Topfmt.pr_cmd_header ast)))])
+                   let lnum = match ast.loc with
+                     | None -> "unknown"
+                     | Some loc -> string_of_int loc.line_nb
+                   in
+                   [("cmd", String (Pp.string_of_ppcmds (Topfmt.pr_cmd_header ast)));
+                    ("line", String lnum)])
                (fun () ->
              Flags.silently (interp_vernac ~check ~state) ast) ())
           ()

From 187b82ce64e2797ee10f4b7f56818c478057257c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Tue, 20 Jun 2023 12:41:02 +0200
Subject: [PATCH 07/11] Doc for newprofile

---
 .../17702-trace.rst                           |  4 ++
 doc/sphinx/practical-tools/coq-commands.rst   | 49 +++++++++++++++++++
 doc/sphinx/practical-tools/utilities.rst      | 15 ++++--
 3 files changed, 65 insertions(+), 3 deletions(-)
 create mode 100644 doc/changelog/08-vernac-commands-and-options/17702-trace.rst

diff --git a/doc/changelog/08-vernac-commands-and-options/17702-trace.rst b/doc/changelog/08-vernac-commands-and-options/17702-trace.rst
new file mode 100644
index 000000000000..4c30e1deb003
--- /dev/null
+++ b/doc/changelog/08-vernac-commands-and-options/17702-trace.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  `-profile` command line argument and `PROFILE` variable in `coq_makefile` to control a new :ref:`profiling` system
+  (`#17702 <https://github.com/coq/coq/pull/17702>`_,
+  by Gaëtan Gilbert).
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index b94898e49328..19ae0a663cda 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -168,6 +168,17 @@ except that ``space_overhead`` is set to 120 and ``minor_heap_size`` is set to 3
 
 .. todo how about COQLIB, COQCORELIB, DOCDIR
 
+.. _COQ_PROFILE_COMPONENTS:
+
+Control which components produce events when using the
+:ref:`profiling` system. It should be a comma separated list of
+components.
+
+If the variable is not set, all components produce events.
+
+Components are internally defined, but `command` which corresponds to
+the interpretation of one command is particularly notable.
+
 .. _command-line-options:
 
 Command line options
@@ -432,7 +443,45 @@ and ``coqtop``, unless stated otherwise:
 :-list-tags: Print the highlight tags known by Coq as well as their
   currently associated color and exit.
 :-h, --help: Print a short usage and exit.
+:-time: Output timing information for each command to standard output.
+:-time-file *file*: Output timing information for each command to the given file.
+:-profile *file*: Output :ref:`profiling` information to the given file.
+
+.. _profiling:
+
+Profiling
+---------
+
+Using the `coqc` command line argument `-profile` or the environment
+variable `PROFILE` with `coq_makefile`, profiling information is produced in
+`Google trace format <https://docs.google.com/document/d/1CvAClvFfyA5R-PhYUmn5OOQtYMH4h6I0nSsKchNAySU/edit>`.
+
+The output consists of duration events for the execution of various
+components of Coq (for instance `process` for the whole file,
+`command` for each command, `pretyping` for elaboration).
+
+Environment variable `COQ_PROFILE_COMPONENTS` can be used to filter
+the components which produce events. This may be needed to reduce the
+size of the produced file.
+
+The produced file can be visualized for instance in
+<https://ui.perfetto.dev> (which can directly load the `.gz`
+compressed file produced by `coq_makefile`) or processed using any
+JSON-capable system.
+
+Events are annotated with additional information in the `args` field
+(either on the beginning `B` or end `E` event):
+
+- `major` and `minor` indicate how many major and minor words were allocated during the event.
+
+- `subtimes` indicates how much time was spent in sub-components and
+  how many times each sub-component was profiled during the event
+  (including sub-components which do not appear in
+  `COQ_PROFILE_COMPONENTS`).
 
+- for the `command` event, `cmd` displays the precise location of the
+  command and a compressed representation of it (like the `-time` header),
+  and `line` is the start line of the command.
 
 .. _compiled-interfaces:
 
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index 8a804f5d9af2..1a5d5ff12f8e 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -734,8 +734,10 @@ variables are already accessible in recipes for rules added in
 Timing targets and performance testing
 ++++++++++++++++++++++++++++++++++++++
 
-The generated ``Makefile`` supports the generation of two kinds of timing
-data: per-file build-times, and per-line times for an individual file.
+The generated ``Makefile`` supports the generation of three kinds of
+timing data: per-file build-times, per-line times for an individual
+file, and profiling data in Google trace format for an individual
+file.
 
 The following targets and Makefile variables allow collection of per-
 file timing data:
@@ -875,7 +877,7 @@ line timing data:
 
 
 + ``TIMING=1``
-    passing this variable will cause ``make`` to use ``coqc -time`` to
+    passing this variable will cause ``make`` to use ``coqc -time-file`` to
     write to a ``.v.timing`` file for each ``.v`` file compiled, which contains
     line-by-line timing information.
 
@@ -972,6 +974,13 @@ line timing data:
     .. note::
       This target requires python to build the table.
 
++ ``PROFILE=1``
+  passing this variable or setting it in the environment will cause
+  ``make`` to use ``coqc -profile`` to write to a ``.v.prof.json``
+  file for each ``.v`` file compiled, which contains :ref:`profiling`
+  information.
+
+  The ``.v.prof.json`` is then compressed by ``gzip`` to a ``.v.prof.json.gz``.
 
 Building a subset of the targets with ``-j``
 ++++++++++++++++++++++++++++++++++++++++++++

From 695d1f7bb8699c75d7158e2eb2b1a08c7599079e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Fri, 30 Jun 2023 14:05:12 +0200
Subject: [PATCH 08/11] Apply suggestions from code review

Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
---
 doc/sphinx/practical-tools/coq-commands.rst | 26 ++++++++++-----------
 doc/sphinx/practical-tools/utilities.rst    |  6 ++---
 2 files changed, 16 insertions(+), 16 deletions(-)

diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index 19ae0a663cda..c0cf41638dce 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -170,13 +170,13 @@ except that ``space_overhead`` is set to 120 and ``minor_heap_size`` is set to 3
 
 .. _COQ_PROFILE_COMPONENTS:
 
-Control which components produce events when using the
-:ref:`profiling` system. It should be a comma separated list of
-components.
+Specifies which components produce events when using the
+:ref:`profiling` system. It is a comma separated list of
+component names.
 
 If the variable is not set, all components produce events.
 
-Components are internally defined, but `command` which corresponds to
+Component names are internally defined, but `command` which corresponds to
 the interpretation of one command is particularly notable.
 
 .. _command-line-options:
@@ -452,19 +452,19 @@ and ``coqtop``, unless stated otherwise:
 Profiling
 ---------
 
-Using the `coqc` command line argument `-profile` or the environment
-variable `PROFILE` with `coq_makefile`, profiling information is produced in
+Use the `coqc` command line argument `-profile` or the environment
+variable `PROFILE` in `coq_makefile`, to generate profiling information in
 `Google trace format <https://docs.google.com/document/d/1CvAClvFfyA5R-PhYUmn5OOQtYMH4h6I0nSsKchNAySU/edit>`.
 
-The output consists of duration events for the execution of various
+The output gives the duration and event counts for the execution of
 components of Coq (for instance `process` for the whole file,
 `command` for each command, `pretyping` for elaboration).
 
-Environment variable `COQ_PROFILE_COMPONENTS` can be used to filter
-the components which produce events. This may be needed to reduce the
-size of the produced file.
+Environment variable :ref:`COQ_PROFILE_COMPONENTS <COQ_PROFILE_COMPONENTS>` can be used to filter
+which components produce events. This may be needed to reduce the
+size of the generated file.
 
-The produced file can be visualized for instance in
+The generated file can be visualized with
 <https://ui.perfetto.dev> (which can directly load the `.gz`
 compressed file produced by `coq_makefile`) or processed using any
 JSON-capable system.
@@ -475,8 +475,8 @@ Events are annotated with additional information in the `args` field
 - `major` and `minor` indicate how many major and minor words were allocated during the event.
 
 - `subtimes` indicates how much time was spent in sub-components and
-  how many times each sub-component was profiled during the event
-  (including sub-components which do not appear in
+  how many times each subcomponent was profiled during the event
+  (including subcomponents which do not appear in
   `COQ_PROFILE_COMPONENTS`).
 
 - for the `command` event, `cmd` displays the precise location of the
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index 1a5d5ff12f8e..7681f2e0b145 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -735,9 +735,9 @@ Timing targets and performance testing
 ++++++++++++++++++++++++++++++++++++++
 
 The generated ``Makefile`` supports the generation of three kinds of
-timing data: per-file build-times, per-line times for an individual
-file, and profiling data in Google trace format for an individual
-file.
+timing data: per-file build-times, per-line times for individual
+files, and profiling data in Google trace format for individual
+files.
 
 The following targets and Makefile variables allow collection of per-
 file timing data:

From 664ec4d5e5687b5d88d21551be487944325b5084 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Fri, 15 Sep 2023 13:51:08 +0200
Subject: [PATCH 09/11] Changed NewProfile.MiniJson.t to polymorphic variants
 matching yojson

---
 lib/newProfile.ml  | 37 +++++++++++++++++++------------------
 lib/newProfile.mli | 12 +++++++-----
 toplevel/vernac.ml |  4 ++--
 3 files changed, 28 insertions(+), 25 deletions(-)

diff --git a/lib/newProfile.ml b/lib/newProfile.ml
index 4c3b05adba55..87c11db2b06b 100644
--- a/lib/newProfile.ml
+++ b/lib/newProfile.ml
@@ -27,21 +27,22 @@ let f fmt = match !accu with
   | File ch -> Printf.fprintf ch fmt
 
 module MiniJson = struct
-  type t =
-    | String of string
-    | Int of string (* string not int so that we can have large ints *)
-    | Record of (string * t) list
-    | Array of t list
-
-  let rec pr ch = function
-    | String s ->
+  type t =[
+    | `Intlit of string
+    | `String of string
+    | `Assoc of (string * t) list
+    | `List of t list
+  ]
+
+  let rec pr ch : t -> _ = function
+    | `String s ->
       let s = String.split_on_char '"' s in
       let s = String.concat "\\\"" s in
       Printf.fprintf ch "\"%s\"" s
-    | Int s -> Printf.fprintf ch "%s" s
-    | Record elts ->
+    | `Intlit s -> Printf.fprintf ch "%s" s
+    | `Assoc elts ->
       Printf.fprintf ch "{ %a }" prrecord elts
-    | Array elts ->
+    | `List elts ->
       Printf.fprintf ch "[\n%a\n]" prarray elts
 
   and prrecord ch = function
@@ -56,15 +57,15 @@ module MiniJson = struct
 
 
   let pids = string_of_int pid
-  let base = [("pid", Int pids); ("tid", Int pids)]
+  let base = [("pid", `Intlit pids); ("tid", `Intlit pids)]
 
   let duration ~name ~ph ~ts ?args () =
-    let l = ("name", String name) :: ("ph", String ph) :: ("ts", Int ts) :: base in
+    let l = ("name", `String name) :: ("ph", `String ph) :: ("ts", `Intlit ts) :: base in
     let l = match args with
       | None -> l
-      | Some args -> ("args", Record args) :: l
+      | Some args -> ("args", `Assoc args) :: l
     in
-    Record l
+    `Assoc l
 end
 
 let gettime = Unix.gettimeofday
@@ -117,11 +118,11 @@ let leave ?time name ?(args=[]) ?last () =
   let time = gettimeopt time in
   let sum, dur = leave_sums ~time name () in
   let sum = List.map (fun (name, (t, cnt)) ->
-      name, MiniJson.String
+      name, `String
         (Printf.sprintf "%.3G us, %d %s" (t *. 1E6) cnt (CString.plural cnt "call")))
       (CString.Map.bindings sum)
   in
-  let args = ("subtimes", MiniJson.Record sum) :: args in
+  let args = ("subtimes", `Assoc sum) :: args in
   duration ~time name "E" ~args ?last ()
 
 let make_mem_diff ~(mstart:Gc.stat) ~(mend:Gc.stat) =
@@ -130,7 +131,7 @@ let make_mem_diff ~(mstart:Gc.stat) ~(mend:Gc.stat) =
      in the same span vs how much survived it *)
   let major = mend.major_words -. mstart.major_words in
   let minor = mend.minor_words -. mstart.minor_words in
-  let pp tdiff = MiniJson.String (Printf.sprintf "%.3G w" tdiff) in
+  let pp tdiff = `String (Printf.sprintf "%.3G w" tdiff) in
   [("major",pp major); ("minor", pp minor)]
 
 (* NB: "process" and "init" are unconditional because they don't go
diff --git a/lib/newProfile.mli b/lib/newProfile.mli
index 28e2c07548a4..18bd57675eaf 100644
--- a/lib/newProfile.mli
+++ b/lib/newProfile.mli
@@ -9,11 +9,13 @@
 (************************************************************************)
 
 module MiniJson : sig
-  type t =
-    | String of string
-    | Int of string (* string not int so that we can have large ints *)
-    | Record of (string * t) list
-    | Array of t list
+  (** Subtype of Yojson.Safe.t *)
+  type t = [
+    | `Intlit of string
+    | `String of string
+    | `Assoc of (string * t) list
+    | `List of t list
+  ]
 end
 
 val profile : string -> ?args:(unit -> (string * MiniJson.t) list) -> (unit -> 'a) -> unit -> 'a
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index c224c360bd32..49de403e0e50 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -128,8 +128,8 @@ let load_vernac_core ~echo ~check ~state ?source file =
                      | None -> "unknown"
                      | Some loc -> string_of_int loc.line_nb
                    in
-                   [("cmd", String (Pp.string_of_ppcmds (Topfmt.pr_cmd_header ast)));
-                    ("line", String lnum)])
+                   [("cmd", `String (Pp.string_of_ppcmds (Topfmt.pr_cmd_header ast)));
+                    ("line", `String lnum)])
                (fun () ->
              Flags.silently (interp_vernac ~check ~state) ast) ())
           ()

From a06a241ebbfcd31446fbce6b4dda1d022a32872f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Fri, 15 Sep 2023 15:14:10 +0200
Subject: [PATCH 10/11] NewProfile: move file handling and at_exit calling to
 init caller

---
 lib/newProfile.ml  | 57 ++++++++++++++++++++--------------------------
 lib/newProfile.mli |  6 +++--
 sysinit/coqinit.ml |  9 +++++++-
 3 files changed, 37 insertions(+), 35 deletions(-)

diff --git a/lib/newProfile.ml b/lib/newProfile.ml
index 87c11db2b06b..313dab389a75 100644
--- a/lib/newProfile.ml
+++ b/lib/newProfile.ml
@@ -8,13 +8,9 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-type settings =
-  { file : string
-  }
-
 type accu =
   | No
-  | File of out_channel
+  | Format of { ch : Format.formatter }
 
 let accu = ref No
 
@@ -24,7 +20,7 @@ let is_profiling () = !accu <> No
 
 let f fmt = match !accu with
   | No -> assert false
-  | File ch -> Printf.fprintf ch fmt
+  | Format { ch } -> Format.fprintf ch fmt
 
 module MiniJson = struct
   type t =[
@@ -38,22 +34,22 @@ module MiniJson = struct
     | `String s ->
       let s = String.split_on_char '"' s in
       let s = String.concat "\\\"" s in
-      Printf.fprintf ch "\"%s\"" s
-    | `Intlit s -> Printf.fprintf ch "%s" s
+      Format.fprintf ch "\"%s\"" s
+    | `Intlit s -> Format.fprintf ch "%s" s
     | `Assoc elts ->
-      Printf.fprintf ch "{ %a }" prrecord elts
+      Format.fprintf ch "{ %a }" prrecord elts
     | `List elts ->
-      Printf.fprintf ch "[\n%a\n]" prarray elts
+      Format.fprintf ch "[\n%a\n]" prarray elts
 
   and prrecord ch = function
     | [] -> ()
-    | [(x,v)] -> Printf.fprintf ch "\"%s\": %a" x pr v
-    | (x,v) :: l -> Printf.fprintf ch "\"%s\": %a, %a" x pr v prrecord l
+    | [(x,v)] -> Format.fprintf ch "\"%s\": %a" x pr v
+    | (x,v) :: l -> Format.fprintf ch "\"%s\": %a, %a" x pr v prrecord l
 
   and prarray ch = function
     | [] -> ()
     | [x] -> pr ch x
-    | x :: l -> Printf.fprintf ch "%a,\n%a" pr x prarray l
+    | x :: l -> Format.fprintf ch "%a,\n%a" pr x prarray l
 
 
   let pids = string_of_int pid
@@ -75,7 +71,7 @@ let gettimeopt = function
   | None -> gettime()
 
 let prtime t =
-  Printf.sprintf "%.0f" (t *. 1E6)
+  Format.sprintf "%.0f" (t *. 1E6)
 
 let global_start = gettime()
 let global_start_stat = Gc.quick_stat()
@@ -119,7 +115,7 @@ let leave ?time name ?(args=[]) ?last () =
   let sum, dur = leave_sums ~time name () in
   let sum = List.map (fun (name, (t, cnt)) ->
       name, `String
-        (Printf.sprintf "%.3G us, %d %s" (t *. 1E6) cnt (CString.plural cnt "call")))
+        (Format.sprintf "%.3G us, %d %s" (t *. 1E6) cnt (CString.plural cnt "call")))
       (CString.Map.bindings sum)
   in
   let args = ("subtimes", `Assoc sum) :: args in
@@ -131,7 +127,7 @@ let make_mem_diff ~(mstart:Gc.stat) ~(mend:Gc.stat) =
      in the same span vs how much survived it *)
   let major = mend.major_words -. mstart.major_words in
   let minor = mend.minor_words -. mstart.minor_words in
-  let pp tdiff = `String (Printf.sprintf "%.3G w" tdiff) in
+  let pp tdiff = `String (Format.sprintf "%.3G w" tdiff) in
   [("major",pp major); ("minor", pp minor)]
 
 (* NB: "process" and "init" are unconditional because they don't go
@@ -175,27 +171,24 @@ let profile name ?args f () =
     v
   end
 
-let init opts =
+type settings =
+  { output : Format.formatter
+  }
+
+let init { output } =
   let () = assert (not (is_profiling())) in
-  match opts with
-  | None ->
-    accu := No
-  | Some { file } ->
-    let ch = open_out file in
-    accu := File ch;
-    f "{ \"traceEvents\": [\n";
-    enter ~time:global_start "process" ();
-    enter ~time:global_start "init" ();
-    leave "init" ~args:(make_mem_diff ~mstart:global_start_stat ~mend:(Gc.quick_stat())) ()
+  accu := Format { ch = output };
+  f "{ \"traceEvents\": [\n";
+  enter ~time:global_start "process" ();
+  enter ~time:global_start "init" ();
+  leave "init" ~args:(make_mem_diff ~mstart:global_start_stat ~mend:(Gc.quick_stat())) ()
 
 let finish () = match !accu with
   | No -> ()
-  | File ch ->
+  | Format { ch } ->
     leave "process"
       ~last:""
       ~args:(make_mem_diff ~mstart:global_start_stat ~mend:(Gc.quick_stat()))
       ();
-    Printf.fprintf ch "],\n\"displayTimeUnit\": \"us\" }";
-    close_out ch
-
-let () = at_exit finish
+    Format.fprintf ch "],\n\"displayTimeUnit\": \"us\" }";
+    accu := No
diff --git a/lib/newProfile.mli b/lib/newProfile.mli
index 18bd57675eaf..985a53fb976e 100644
--- a/lib/newProfile.mli
+++ b/lib/newProfile.mli
@@ -23,7 +23,9 @@ val profile : string -> ?args:(unit -> (string * MiniJson.t) list) -> (unit -> '
 val is_profiling : unit -> bool
 
 type settings =
-  { file : string
+  { output : Format.formatter
   }
 
-val init : settings option -> unit
+val init : settings -> unit
+
+val finish : unit -> unit
diff --git a/sysinit/coqinit.ml b/sysinit/coqinit.ml
index 03807750151c..5acce7d7693f 100644
--- a/sysinit/coqinit.ml
+++ b/sysinit/coqinit.ml
@@ -143,10 +143,17 @@ let init_load_paths opts =
   let env_ocamlpath = String.concat ocamlpathsep env_ocamlpath in
   Findlib.init ~env_ocamlpath ()
 
+let init_profile ~file =
+  let ch = open_out file in
+  NewProfile.init { output = Format.formatter_of_out_channel ch };
+  at_exit (fun () ->
+      NewProfile.finish ();
+      close_out ch)
+
 let init_runtime opts =
   let open Coqargs in
   Vernacextend.static_linking_done ();
-  NewProfile.init (Option.map (fun file -> { NewProfile.file }) opts.config.profile);
+  Option.iter (fun file -> init_profile ~file) opts.config.profile;
   Lib.init ();
   init_coqlib opts;
   if opts.post.memory_stat then at_exit print_memory_stat;

From a5dab76be895b28593768b6d100a68e650316a7b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Fri, 15 Sep 2023 15:30:48 +0200
Subject: [PATCH 11/11] NewProfile: pause and resumption API

---
 lib/newProfile.ml  | 86 ++++++++++++++++++++++++++--------------------
 lib/newProfile.mli | 20 +++++++++++
 2 files changed, 68 insertions(+), 38 deletions(-)

diff --git a/lib/newProfile.ml b/lib/newProfile.ml
index 313dab389a75..1499c7d9d369 100644
--- a/lib/newProfile.ml
+++ b/lib/newProfile.ml
@@ -8,20 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-type accu =
-  | No
-  | Format of { ch : Format.formatter }
-
-let accu = ref No
-
-let pid = Unix.getpid()
-
-let is_profiling () = !accu <> No
-
-let f fmt = match !accu with
-  | No -> assert false
-  | Format { ch } -> Format.fprintf ch fmt
-
 module MiniJson = struct
   type t =[
     | `Intlit of string
@@ -52,6 +38,8 @@ module MiniJson = struct
     | x :: l -> Format.fprintf ch "%a,\n%a" pr x prarray l
 
 
+  let pid = Unix.getpid()
+
   let pids = string_of_int pid
   let base = [("pid", `Intlit pids); ("tid", `Intlit pids)]
 
@@ -64,6 +52,19 @@ module MiniJson = struct
     `Assoc l
 end
 
+type accu = {
+  ch : Format.formatter;
+  mutable sums : (float * (float * int) CString.Map.t) list;
+}
+
+let accu = ref None
+
+let is_profiling () = Option.has_some !accu
+
+let f fmt = match !accu with
+  | None -> assert false
+  | Some { ch } -> Format.fprintf ch fmt
+
 let gettime = Unix.gettimeofday
 
 let gettimeopt = function
@@ -79,11 +80,10 @@ let global_start_stat = Gc.quick_stat()
 let duration ~time name ph ?args ?(last=",") () =
   f "%a%s\n" MiniJson.pr (MiniJson.duration ~name ~ph ~ts:(prtime time) ?args ()) last
 
-let sums = ref []
-
 let enter_sums ?time () =
+  let accu = Option.get !accu in
   let time = gettimeopt time in
-  sums := (time, CString.Map.empty) :: !sums
+  accu.sums <- (time, CString.Map.empty) :: accu.sums
 
 let enter ?time name ?args () =
   let time = gettimeopt time in
@@ -91,24 +91,25 @@ let enter ?time name ?args () =
   duration ~time name "B" ?args ()
 
 let leave_sums ?time name () =
+  let accu = Option.get !accu in
   let time = gettimeopt time in
-  match !sums with
-    | [] -> assert false
-    | [start,sum] -> sums := []; sum, time -. start
-    | (start, sum) :: (start', next) :: rest ->
-      let dur = time -. start in
-      let next = CString.Map.update name (function
-          | None -> Some (dur, 1)
-          | Some (dur', cnt) -> Some (dur +. dur', cnt+1))
-          next
-      in
-      let next = CString.Map.union (fun name' (l,cnt) (r,cnt') ->
-          if String.equal name name' then Some (r,cnt+cnt')
-          else Some (l +. r, cnt+cnt'))
-          sum next
-      in
-      sums := (start', next) :: rest;
-      sum, dur
+  match accu.sums with
+  | [] -> assert false
+  | [start,sum] -> accu.sums <- []; sum, time -. start
+  | (start, sum) :: (start', next) :: rest ->
+    let dur = time -. start in
+    let next = CString.Map.update name (function
+        | None -> Some (dur, 1)
+        | Some (dur', cnt) -> Some (dur +. dur', cnt+1))
+        next
+    in
+    let next = CString.Map.union (fun name' (l,cnt) (r,cnt') ->
+        if String.equal name name' then Some (r,cnt+cnt')
+        else Some (l +. r, cnt+cnt'))
+        sum next
+    in
+   accu. sums <- (start', next) :: rest;
+    sum, dur
 
 let leave ?time name ?(args=[]) ?last () =
   let time = gettimeopt time in
@@ -177,18 +178,27 @@ type settings =
 
 let init { output } =
   let () = assert (not (is_profiling())) in
-  accu := Format { ch = output };
+  accu := Some { ch = output; sums = [] };
   f "{ \"traceEvents\": [\n";
   enter ~time:global_start "process" ();
   enter ~time:global_start "init" ();
   leave "init" ~args:(make_mem_diff ~mstart:global_start_stat ~mend:(Gc.quick_stat())) ()
 
+let pause () =
+  let v = !accu in
+  accu := None;
+  v
+
+let resume v =
+  assert (not (is_profiling()));
+  accu := Some v
+
 let finish () = match !accu with
-  | No -> ()
-  | Format { ch } ->
+  | None -> assert false
+  | Some { ch } ->
     leave "process"
       ~last:""
       ~args:(make_mem_diff ~mstart:global_start_stat ~mend:(Gc.quick_stat()))
       ();
     Format.fprintf ch "],\n\"displayTimeUnit\": \"us\" }";
-    accu := No
+    accu := None
diff --git a/lib/newProfile.mli b/lib/newProfile.mli
index 985a53fb976e..954a5db363ee 100644
--- a/lib/newProfile.mli
+++ b/lib/newProfile.mli
@@ -19,6 +19,11 @@ module MiniJson : sig
 end
 
 val profile : string -> ?args:(unit -> (string * MiniJson.t) list) -> (unit -> 'a) -> unit -> 'a
+(** Profile the given function.
+
+    [args] is called only if profiling is active, it is used to
+    produce additional annotations.
+*)
 
 val is_profiling : unit -> bool
 
@@ -27,5 +32,20 @@ type settings =
   }
 
 val init : settings -> unit
+(** Profiling must not be active.
+    Activates profiling with a fresh state. *)
 
 val finish : unit -> unit
+(** Profiling must be active.
+    Deactivates profiling. *)
+
+type accu
+(** Profiling state accumulator. *)
+
+val pause : unit -> accu option
+(** Returns [None] if profiling is inactive.
+    Deactivates profiling if it is active, returning the current state. *)
+
+val resume : accu -> unit
+(** Profiling must not be active.
+    Activates profiling with the given state. *)