Merge PR coq#17702: Produce profiles in google trace format

Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: jfehrle
Ack-by: rlepigre
Co-authored-by: ejgallego <[email protected]>

dev/bench/bench.sh

@@ -458,6 +458,8 @@ 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
 

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

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).

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:
+
+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.
+
+Component names 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
+---------
+
+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 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 :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 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.
+
+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 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
+  command and a compressed representation of it (like the `-time` header),
+  and `line` is the start line of the command.
 
 .. _compiled-interfaces:
 

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 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:
@@ -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``
 ++++++++++++++++++++++++++++++++++++++++++++

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                    *)

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

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

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)
+    ()

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
+    ()