Merge pull request #777 from SkySkimmer/make-profiling

build: support PROFILING and TIMED like coq_makefile

.gitignore

@@ -66,6 +66,9 @@ compcert/test/
 *.vos
 *.vok
 *.glob
+*.timing
+*.prof.json
+*.prof.json.gz
 *.v.d
 .depend
 .loadpath

Makefile

@@ -334,6 +334,37 @@ DEPFLAGS:=$(COQFLAGS)
 
 COQFLAGS+=$(COQEXTRAFLAGS)
 
+PROFILING?=
+
+ifneq (,$(PROFILING))
+  # does this coq version dupport -profile ? (Coq >= 8.19)
+  ifeq (,$(shell "$(COQBIN)coqc" -profile /dev/null 2>&1))
+    PROFILE_FLAGS+=-profile $<.prof.json
+    PROFILE_ZIP = gzip -f $<.prof.json
+  else
+  endif
+endif
+PROFILE_FLAGS ?=
+PROFILE_ZIP ?= true
+
+TIMED?=
+
+# Use command time on linux, gtime on Mac OS
+TIMEFMT?="$(if $(findstring undefined, $(flavor 1)),$@,$(1)) (real: %e, user: %U, sys: %S, mem: %M ko)"
+ifneq (,$(TIMED))
+ifeq (0,$(shell command time -f "" true >/dev/null 2>/dev/null; echo $$?))
+STDTIME?=command time -f $(TIMEFMT)
+else
+ifeq (0,$(shell gtime -f "" true >/dev/null 2>/dev/null; echo $$?))
+STDTIME?=gtime -f $(TIMEFMT)
+else
+STDTIME?=command time
+endif
+endif
+else
+STDTIME?=command time -f $(TIMEFMT)
+endif
+
 # ##### Print configuration summary #####
 
 $(info ===== CONFIGURATION SUMMARY =====)
@@ -696,15 +727,15 @@ IRIS_INSTALL_FILES=$(sort $(IRIS_INSTALL_FILES_SRC) $(IRIS_INSTALL_FILES_VO))
 
 # This line sets COQF depending on the folder of the input file $<
 # If the folder name contains compcert, $(COMPCERT_R_FLAGS) is added, otherwise not.
-%.vo: COQF=$(if $(findstring $(COMPCERT_SRC_DIR), $(dir $<)), $(COMPCERT_R_FLAGS) $(COQEXTRAFLAGS), $(COQFLAGS))
+%.vo: COQF=$(if $(findstring $(COMPCERT_SRC_DIR), $(dir $<)), $(COMPCERT_R_FLAGS) $(COQEXTRAFLAGS), $(COQFLAGS) $(PROFILE_FLAGS))
 
 # If CompCert changes, all .vo files need to be recompiled
 %.vo: $(COMPCERT_CONFIG)
 
 %.vo: %.v
 	@echo COQC $*.v
 ifneq (,$(TIMING))
-	@$(COQC) $(COQF) -time $*.v > $<.timing
+	@$(if $(TIMED),$(STDTIME)) $(COQC) $(COQF) -time $*.v > $<.timing
 else ifeq ($(TIMINGS), true)
 #	bash -c "wc $*.v >>timings; date +'%s.%N before' >> timings; $(COQC) $(COQF) $*.v; date +'%s.%N after' >>timings" 2>>timings
 	@bash -c "/usr/bin/time --output=TIMINGS -a -f '%e real, %U user, %S sys %M mem, '\"$(shell wc $*.v)\" $(COQC) $(COQF) $*.v"
@@ -721,6 +752,7 @@ else
 	@$(COQC) $(COQF) $*.v
 #	@util/annotate $(COQC) $(COQF) $*.v
 endif
+	@$(PROFILE_ZIP)
 
 
 # ########## Targets ##########