Merge PR coq#19938: coq_makefile produce timing info for coqdep

Reviewed-by: ppedrot Reviewed-by: gares Co-authored-by: ppedrot <[email protected]>
SkySkimmer · Dec 19, 2024 · f64f690 · f64f690
2 parents 734ec43 + 093dd6e
commit f64f690
Show file tree

Hide file tree

Showing 4 changed files with 13 additions and 1 deletion.
diff --git a/test-suite/coq-makefile/timing-per-file/after/time-of-build-after.log.desired b/test-suite/coq-makefile/timing-per-file/after/time-of-build-after.log.desired
@@ -1,4 +1,5 @@
 ROCQ DEP VFILES
+.Makefile.d (ignored)
 ROCQ compile Slow.v
 Slow.vo (real: 0.04, user: 0.02, sys: 0.01, mem: 45512 ko)
 ROCQ compile Fast.v

diff --git a/test-suite/coq-makefile/timing-per-file/after/time-of-build-before.log.desired b/test-suite/coq-makefile/timing-per-file/after/time-of-build-before.log.desired
@@ -1,4 +1,5 @@
 ROCQ DEP VFILES
+.Makefile.d (ignored)
 ROCQ compile Slow.v
 Slow.vo (real: 0.40, user: 0.35, sys: 0.04, mem: 394968 ko)
 ROCQ compile Fast.v

diff --git a/test-suite/coq-makefile/timing-per-file/run.sh b/test-suite/coq-makefile/timing-per-file/run.sh
@@ -2,10 +2,19 @@
 
 . ../timing-template/init.sh
 
+rm -rf _test
+mkdir _test
+find . -maxdepth 1 -not -name . -not -name _test -exec cp -r '{}' -t _test ';'
+cd _test
+
+# we delete the timings for coqdep because they're too close to 0
+# so testing them is hard
+
 cd before/
 rocq makefile -f _CoqProject -o Makefile
 make cleanall
 make make-pretty-timed-before TGTS="all" -j1 || exit $?
+sed -i.bak 's/.Makefile.d .*/.Makefile.d (ignored)/' time-of-build-before.log
 
 cd ../after/
 
@@ -14,6 +23,7 @@ make cleanall
 
 make make-pretty-timed-after TGTS="all" -j1 || exit $?
 rm -f time-of-build-before.log
+sed -i.bak 's/.Makefile.d .*/.Makefile.d (ignored)/' time-of-build-after.log
 
 make print-pretty-timed-diff TIMING_SORT_BY=diff TIME_OF_BUILD_BEFORE_FILE=../before/time-of-build-before.log
 cp ../before/time-of-build-before.log ./

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
@@ -892,7 +892,7 @@ VDFILE_FLAGS:=$(if @PROJECT_FILE@,-f @PROJECT_FILE@,) $(CMDLINE_COQLIBS) $(CMDLI
 
 $(VDFILE): @PROJECT_FILE@ $(VFILES)
 	$(SHOW)'ROCQ DEP VFILES'
-	$(HIDE)$(COQDEP) -vos -dyndep var $(VDFILE_FLAGS) $(redir_if_ok)
+	$(HIDE)$(TIMER) $(COQDEP) -vos -dyndep var $(VDFILE_FLAGS) $(redir_if_ok)
 
 # Misc ########################################################################