Fix ordering of before/after in print-pretty-timed-*

Fixes #8158

5 files changed, 25 insertions, 16 deletions

diff --git a/CHANGES b/CHANGES
index df4a1df176..d7be066690 100644
--- a/CHANGES
+++ b/CHANGES
@@ -76,6 +76,11 @@ Tools
   please open an issue. We can help set up external maintenance as part
   of Proof-General, or independently as part of coq-community.
 
+- The targets `print-pretty-timed`, `print-pretty-timed-diff`, and
+  `print-pretty-single-time-diff` now correctly label the "before" and
+  "after" columns, rather than swapping them.
+
+
 Vernacular Commands
 
 - Removed deprecated commands Arguments Scope and Implicit Arguments
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 56815d241e..72c520218c 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
@@ -1,6 +1,6 @@
 After    | File Name | Before   || Change    | % Change 
 --------------------------------------------------------
-0m00.38s | Total     | 0m00.39s || -0m00.01s | -2.56%   
+0m00.34s | Total     | 0m00.49s || -0m00.14s | -30.61%  
 --------------------------------------------------------
-0m00.35s | Slow      | 0m00.02s || +0m00.32s | +1649.99%
-0m00.03s | Fast      | 0m00.37s || -0m00.34s | -91.89%  
\ No newline at end of file
+0m00.32s | Fast      | 0m00.02s || +0m00.30s | +1500.00%
+0m00.02s | Slow      | 0m00.47s || -0m00.44s | -95.74%  
\ No newline at end of file
diff --git a/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired b/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired
index 18f0f34b28..74dad73332 100644
--- a/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired
+++ b/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired
@@ -1,9 +1,9 @@
-After     | Code                                                | Before    || Change    | % Change
----------------------------------------------------------------------------------------------------
-0m00.50s  | Total                                               | 0m04.17s  || -0m03.66s | -87.96% 
----------------------------------------------------------------------------------------------------
-0m00.145s | Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] | 0m00.192s || -0m00.04s | -24.47% 
-0m00.126s | Chars 000 - 026 [Require~Coq.ZArith.BinInt.]        | 0m00.143s || -0m00.01s | -11.88% 
-   N/A    | Chars 027 - 068 [Declare~Reduction~comp~:=~nati...] | 0m00.s    || +0m00.00s | N/A     
-0m00.s    | Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] |    N/A    || +0m00.00s | N/A     
-0m00.231s | Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] | 0m03.836s || -0m03.60s | -93.97% 
\ No newline at end of file
+After     | Code                                                | Before    || Change    | % Change 
+----------------------------------------------------------------------------------------------------
+0m04.35s  | Total                                               | 0m00.58s  || +0m03.77s | +649.05% 
+----------------------------------------------------------------------------------------------------
+0m03.87s  | Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] | 0m00.246s || +0m03.62s | +1473.17%
+0m00.322s | Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] | 0m00.189s || +0m00.13s | +70.37%  
+0m00.16s  | Chars 000 - 026 [Require~Coq.ZArith.BinInt.]        | 0m00.146s || +0m00.01s | +9.58%   
+0m00.s    | Chars 027 - 068 [Declare~Reduction~comp~:=~nati...] |    N/A    || +0m00.00s | N/A      
+   N/A    | Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] | 0m00.s    || +0m00.00s | N/A      
\ No newline at end of file
diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh
index 6737197ee4..78a3f7c63a 100755
--- a/test-suite/coq-makefile/timing/run.sh
+++ b/test-suite/coq-makefile/timing/run.sh
@@ -5,6 +5,10 @@ set -e
 
 . ../template/path-init.sh
 
+# reset MAKEFLAGS so that, e.g., `make -C test-suite -B coq-makefile` doesn't give us issues
+
+MAKEFLAGS=
+
 cd precomputed-time-tests
 ./run.sh || exit $?
 
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 8b6822a4ed..403ad61798 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -343,19 +343,19 @@ make-pretty-timed make-pretty-timed-before make-pretty-timed-after::
 print-pretty-timed::
 	$(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
 print-pretty-timed-diff::
-	$(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
+	$(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
 ifeq (,$(BEFORE))
 print-pretty-single-time-diff::
-	@echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing'
+	@echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing'
 	$(HIDE)false
 else
 ifeq (,$(AFTER))
 print-pretty-single-time-diff::
-	@echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing'
+	@echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing'
 	$(HIDE)false
 else
 print-pretty-single-time-diff::
-	$(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --sort-by=$(TIMING_SORT_BY) $(BEFORE) $(AFTER) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
+	$(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --sort-by=$(TIMING_SORT_BY) $(AFTER) $(BEFORE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
 endif
 endif
 pretty-timed: