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

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

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

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
@@ -796,7 +804,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
@@ -807,7 +815,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) $@