Merge PR #12126: TIMEFMT: Display the output file name

Reviewed-by: SkySkimmer

7 files changed, 24 insertions, 16 deletions

diff --git a/Makefile.build b/Makefile.build
index 7879580e18..8a8500ba1a 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -201,7 +201,7 @@ DEPENDENCIES := \
 
 # Default timing command
 # Use /usr/bin/env time on linux, gtime on Mac OS
-TIMEFMT?="$* (real: %e, user: %U, sys: %S, mem: %M ko)"
+TIMEFMT?="$@ (real: %e, user: %U, sys: %S, mem: %M ko)"
 ifneq (,$(TIMED))
 ifeq (0,$(shell /usr/bin/env time -f "" true >/dev/null 2>/dev/null; echo $$?))
 STDTIME?=/usr/bin/env time -f $(TIMEFMT)
diff --git a/doc/changelog/08-tools/12126-adjust-timed-name.rst b/doc/changelog/08-tools/12126-adjust-timed-name.rst
new file mode 100644
index 0000000000..c305b384d9
--- /dev/null
+++ b/doc/changelog/08-tools/12126-adjust-timed-name.rst
@@ -0,0 +1,8 @@
+- **Changed:**
+  The output of ``make TIMED=1`` (and therefore the timing targets
+  such as ``print-pretty-timed`` and ``print-pretty-timed-diff``) now
+  displays the full name of the output file being built, rather than
+  the stem of the rule (which was usually the filename without the
+  extension, but in general could be anything for user-defined rules
+  involving ``%``) (`#12126
+  <https://github.com/coq/coq/pull/12126>`_, by Jason Gross).
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index 921c7bbbf7..bc77e2e58c 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -245,9 +245,9 @@ file timing data:
           COQDEP Fast.v
           COQDEP Slow.v
           COQC Slow.v
-          Slow (user: 0.34 mem: 395448 ko)
+          Slow.vo (user: 0.34 mem: 395448 ko)
           COQC Fast.v
-          Fast (user: 0.01 mem: 45184 ko)
+          Fast.vo (user: 0.01 mem: 45184 ko)
 
 + ``pretty-timed``
     this target stores the output of ``make TIMED=1`` into
@@ -280,15 +280,15 @@ file timing data:
         COQDEP Fast.v
         COQDEP Slow.v
         COQC Slow.v
-        Slow (user: 0.36 mem: 393912 ko)
+        Slow.vo (user: 0.36 mem: 393912 ko)
         COQC Fast.v
-        Fast (user: 0.05 mem: 45992 ko)
+        Fast.vo (user: 0.05 mem: 45992 ko)
         Time     | File Name
         --------------------
         0m00.41s | Total
         --------------------
-        0m00.36s | Slow
-        0m00.05s | Fast
+        0m00.36s | Slow.vo
+        0m00.05s | Fast.vo
 
 
 + ``print-pretty-timed-diff``
@@ -338,8 +338,8 @@ file timing data:
           --------------------------------------------------------
           0m00.39s | Total     | 0m00.35s || +0m00.03s | +11.42%
           --------------------------------------------------------
-          0m00.37s | Slow      | 0m00.01s || +0m00.36s | +3600.00%
-          0m00.02s | Fast      | 0m00.34s || -0m00.32s | -94.11%
+          0m00.37s | Slow.vo   | 0m00.01s || +0m00.36s | +3600.00%
+          0m00.02s | Fast.vo   | 0m00.34s || -0m00.32s | -94.11%
 
 
 The following targets and ``Makefile`` variables allow collection of per-
diff --git a/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired
index 4381160a4e..ebe44f3548 100644
--- a/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired
+++ b/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired
@@ -1,5 +1,5 @@
 COQDEP VFILES
 COQC Slow.v
-Slow (real: 0.04, user: 0.02, sys: 0.01, mem: 45512 ko)
+Slow.vo (real: 0.04, user: 0.02, sys: 0.01, mem: 45512 ko)
 COQC Fast.v
-Fast (real: 0.41, user: 0.37, sys: 0.04, mem: 395200 ko)
+Fast.vo (real: 0.41, user: 0.37, sys: 0.04, mem: 395200 ko)
diff --git a/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired
index e6af909268..bf17a3e95c 100644
--- a/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired
+++ b/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired
@@ -1,5 +1,5 @@
 COQDEP VFILES
 COQC Slow.v
-Slow (real: 0.40, user: 0.35, sys: 0.04, mem: 394968 ko)
+Slow.vo (real: 0.40, user: 0.35, sys: 0.04, mem: 394968 ko)
 COQC Fast.v
-Fast (real: 0.04, user: 0.03, sys: 0.00, mem: 46564 ko)
+Fast.vo (real: 0.04, user: 0.03, sys: 0.00, mem: 46564 ko)
diff --git a/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired
index 72c520218c..c8f35dc1e4 100644
--- a/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired
+++ b/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired
@@ -2,5 +2,5 @@ After    | File Name | Before   || Change    | % Change
 --------------------------------------------------------
 0m00.34s | Total     | 0m00.49s || -0m00.14s | -30.61%  
 --------------------------------------------------------
-0m00.32s | Fast      | 0m00.02s || +0m00.30s | +1500.00%
-0m00.02s | Slow      | 0m00.47s || -0m00.44s | -95.74%  
\ No newline at end of file
+0m00.32s | Fast.vo   | 0m00.02s || +0m00.30s | +1500.00%
+0m00.02s | Slow.vo   | 0m00.47s || -0m00.44s | -95.74%  
\ No newline at end of file
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 0202b3136b..745bbb7e55 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -66,7 +66,7 @@ VERBOSE ?=
 TIMED?=
 TIMECMD?=
 # Use command time on linux, gtime on Mac OS
-TIMEFMT?="$* (real: %e, user: %U, sys: %S, mem: %M ko)"
+TIMEFMT?="$@ (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)