TIMEFMT: Display the output file name

We now use `$@` rather than `$*` so that we display the output target
rather than the stem of the rule.  This is more consistent for rules
that users add (where the pattern variable might be something
insufficiently identifying), and also generalizes more nicely to mixing
multiple compilers (we get a clear difference between producing OCaml
files and producing .vo files, even if the filename is the same up to
the suffix).  The result is that it's easy to describe what the timing
information of the build log records: each time comes with a label which
is a file name, and the time is the time it takes to produce that file.

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)