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 index c64826700c8b..e4ad46cfdfe5 100644 --- 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 index 6d62e896b5a1..6ab2fadc2dae 100644 --- 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 index 284da3bc2b66..0c41d40048bd 100644 --- 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 index 958dc1140c7b..689abd52310e 100644 --- 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 ########################################################################