Add --fuzz, --real, --user to timing scripts

- Add a `--fuzz` option to `make-both-single-timing-files.py`

  Passing `--fuzz=N` allows differences in character locations of up to
  `N` characters when matching lines in per-line timing diffs.

  The corresponding variable for `coq_makefile` is `TIMING_FUZZ=N`.

  See also the discussion at
  https://github.com/coq/coq/pull/11076#pullrequestreview-324791139

- Allow passing `--real` to per-file timing scripts and `--user` to
  per-line timing script.

  This allows easily comparing real times instead of user ones (or vice
  versa).

- Support `TIMING_SORT_BY` and `TIMING_FUZZ` in Coq's own build

- We also now use argparse rather than a hand-rolled argument parser;
  there were getting to be too many combinations of options.

- Fix the ordering of columns in Coq's build system; this is the
  equivalent of #8167 for Coq's build system.

Fixes #11301
Supersedes / closes #11022
Supersedes / closes #11230

14 files changed, 217 insertions, 4 deletions

diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/run.sh b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/run.sh
index 4a50759bdb..a6f35db17c 100755
--- a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/run.sh
+++ b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/run.sh
@@ -5,6 +5,10 @@ set -e
 
 cd "$(dirname "${BASH_SOURCE[0]}")"
 
-"$COQLIB"/tools/make-both-time-files.py time-of-build-after.log.in time-of-build-before.log.in time-of-build-both.log
+"$COQLIB"/tools/make-both-time-files.py time-of-build-after.log.in time-of-build-before.log.in time-of-build-both-user.log
 
-diff -u time-of-build-both.log.expected time-of-build-both.log || exit $?
+diff -u time-of-build-both-user.log.expected time-of-build-both-user.log || exit $?
+
+"$COQLIB"/tools/make-both-time-files.py --real time-of-build-after.log.in time-of-build-before.log.in time-of-build-both-real.log
+
+diff -u time-of-build-both-real.log.expected time-of-build-both-real.log || exit $?
diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real.log.expected
new file mode 100644
index 0000000000..ea600b000e
--- /dev/null
+++ b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real.log.expected
@@ -0,0 +1,26 @@
+After     | File Name                                      | Before    || Change    | % Change
+----------------------------------------------------------------------------------------------
+20m46.07s | Total                                          | 23m06.30s || -2m20.23s | -10.11% 
+----------------------------------------------------------------------------------------------
+4m16.77s  | Specific/X25519/C64/ladderstep                 | 5m16.83s  || -1m00.06s | -18.95% 
+3m01.77s  | Specific/solinas32_2e255m765_13limbs/femul     | 3m27.94s  || -0m26.16s | -12.58% 
+2m35.79s  | Specific/solinas32_2e255m765_12limbs/femul     | 2m59.21s  || -0m23.42s | -13.06% 
+3m22.96s  | Specific/NISTP256/AMD64/femul                  | 3m37.80s  || -0m14.84s | -6.81%  
+0m39.72s  | Specific/X25519/C64/femul                      | 0m42.98s  || -0m03.25s | -7.58%  
+0m38.19s  | Specific/NISTP256/AMD64/feadd                  | 0m40.48s  || -0m02.28s | -5.65%  
+0m34.35s  | Specific/X25519/C64/freeze                     | 0m36.42s  || -0m02.07s | -5.68%  
+0m33.08s  | Specific/X25519/C64/fesquare                   | 0m35.23s  || -0m02.14s | -6.10%  
+0m31.00s  | Specific/NISTP256/AMD64/feopp                  | 0m32.08s  || -0m01.07s | -3.36%  
+0m27.81s  | Specific/NISTP256/AMD64/fenz                   | 0m28.91s  || -0m01.10s | -3.80%  
+0m27.11s  | Specific/X25519/C64/fecarry                    | 0m28.85s  || -0m01.74s | -6.03%  
+0m24.71s  | Specific/X25519/C64/fesub                      | 0m26.11s  || -0m01.39s | -5.36%  
+0m49.44s  | Specific/solinas32_2e255m765_13limbs/Synthesis | 0m49.50s  || -0m00.06s | -0.12%  
+0m43.34s  | Specific/NISTP256/AMD64/fesub                  | 0m43.78s  || -0m00.43s | -1.00%  
+0m40.13s  | Specific/solinas32_2e255m765_12limbs/Synthesis | 0m39.53s  || +0m00.60s | +1.51%  
+0m22.81s  | Specific/X25519/C64/feadd                      | 0m23.43s  || -0m00.62s | -2.64%  
+0m13.45s  | Specific/NISTP256/AMD64/Synthesis              | 0m13.74s  || -0m00.29s | -2.11%  
+0m11.15s  | Specific/X25519/C64/Synthesis                  | 0m11.23s  || -0m00.08s | -0.71%  
+0m07.33s  | Compilers/Z/Bounds/Pipeline/Definition         | 0m07.40s  || -0m00.07s | -0.94%  
+0m01.93s  | Compilers/Z/Bounds/Pipeline/ReflectiveTactics  | 0m01.73s  || +0m00.19s | +11.56% 
+0m01.85s  | Specific/Framework/SynthesisFramework          | 0m01.95s  || -0m00.09s | -5.12%  
+0m01.38s  | Compilers/Z/Bounds/Pipeline                    | 0m01.18s  || +0m00.19s | +16.94% 
\ No newline at end of file
diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user.log.expected
index 159e645512..159e645512 100644
--- a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both.log.expected
+++ b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user.log.expected
diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/run.sh b/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/run.sh
index 4f39b3ce7e..d4614749e7 100755
--- a/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/run.sh
+++ b/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/run.sh
@@ -5,6 +5,10 @@ set -e
 
 cd "$(dirname "${BASH_SOURCE[0]}")"
 
-"$COQLIB"/tools/make-one-time-file.py time-of-build.log.in time-of-build-pretty.log
+"$COQLIB"/tools/make-one-time-file.py time-of-build.log.in time-of-build-pretty-user.log
 
-diff -u time-of-build-pretty.log.expected time-of-build-pretty.log || exit $?
+diff -u time-of-build-pretty-user.log.expected time-of-build-pretty-user.log || exit $?
+
+"$COQLIB"/tools/make-one-time-file.py time-of-build.log.in time-of-build-pretty-real.log
+
+diff -u time-of-build-pretty-real.log.expected time-of-build-pretty-real.log || exit $?
diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty-real.log.expected
index b9739ddb1d..b9739ddb1d 100644
--- a/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty.log.expected
+++ b/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty-real.log.expected
diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty-user.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty-user.log.expected
new file mode 100644
index 0000000000..b9739ddb1d
--- /dev/null
+++ b/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty-user.log.expected
@@ -0,0 +1,26 @@
+Time      | File Name                                     
+----------------------------------------------------------
+19m16.04s | Total                                         
+----------------------------------------------------------
+4m01.34s  | Specific/X25519/C64/ladderstep                
+3m09.62s  | Specific/NISTP256/AMD64/femul                 
+2m48.52s  | Specific/solinas32_2e255m765_13limbs/femul    
+2m23.70s  | Specific/solinas32_2e255m765_12limbs/femul    
+0m45.75s  | Specific/solinas32_2e255m765_13limbs/Synthesis
+0m39.59s  | Specific/NISTP256/AMD64/fesub                 
+0m36.92s  | Specific/solinas32_2e255m765_12limbs/Synthesis
+0m36.32s  | Specific/X25519/C64/femul                     
+0m35.40s  | Specific/NISTP256/AMD64/feadd                 
+0m31.50s  | Specific/X25519/C64/freeze                    
+0m30.13s  | Specific/X25519/C64/fesquare                  
+0m28.51s  | Specific/NISTP256/AMD64/feopp                 
+0m25.50s  | Specific/NISTP256/AMD64/fenz                  
+0m24.99s  | Specific/X25519/C64/fecarry                   
+0m22.65s  | Specific/X25519/C64/fesub                     
+0m20.93s  | Specific/X25519/C64/feadd                     
+0m12.55s  | Specific/NISTP256/AMD64/Synthesis             
+0m10.37s  | Specific/X25519/C64/Synthesis                 
+0m07.18s  | Compilers/Z/Bounds/Pipeline/Definition        
+0m01.72s  | Compilers/Z/Bounds/Pipeline/ReflectiveTactics 
+0m01.67s  | Specific/Framework/SynthesisFramework         
+0m01.19s  | Compilers/Z/Bounds/Pipeline                   
\ No newline at end of file
diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo-real.v.timing.diff.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo-real.v.timing.diff.expected
new file mode 100644
index 0000000000..726c19a2e2
--- /dev/null
+++ b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo-real.v.timing.diff.expected
@@ -0,0 +1,29 @@
+After     | Code                                                        | Before    || Change    | % Change
+-----------------------------------------------------------------------------------------------------------
+0m01.23s  | Total                                                       | 0m01.28s  || -0m00.04s | -3.50%  
+-----------------------------------------------------------------------------------------------------------
+0m00.53s  | Chars 260-284 ~ 280-304 [(vm_compute;~reflexivity).]        | 0m00.566s || -0m00.03s | -6.36%  
+0m00.4s   | Chars 285-289 ~ 305-309 [Qed.]                              | 0m00.411s || -0m00.01s | -2.67%  
+0m00.194s | Chars 031-064 ~ 031-064 [Require~Import~Coq.ZArith.ZArith.] | 0m00.192s || +0m00.00s | +1.04%  
+0m00.114s | Chars 000-030 ~ 000-030 [Require~Import~Coq.Lists.List.]    | 0m00.114s || +0m00.00s | +0.00%  
+0m00.s    | Chars 065-075 ~ 065-075 [Goal~_~True.]                      | 0m00.s    || +0m00.00s | N/A     
+0m00.s    | Chars 078-086 ~ 078-086 [exact~I.]                          |    N/A    || +0m00.00s | N/A     
+   N/A    | Chars 078-090 ~ 078-090 [constructor.]                      | 0m00.s    || +0m00.00s | N/A     
+0m00.s    | Chars 087-091 ~ 091-095 [Qed.]                              | 0m00.s    || +0m00.00s | N/A     
+0m00.s    | Chars 092-102 ~ 096-106 [Goal~_~True.]                      | 0m00.s    || +0m00.00s | N/A     
+0m00.s    | Chars 105-113 ~ 109-117 [exact~I.]                          |    N/A    || +0m00.00s | N/A     
+   N/A    | Chars 105-117 ~ 109-121 [constructor.]                      | 0m00.s    || +0m00.00s | N/A     
+0m00.s    | Chars 114-118 ~ 122-126 [Qed.]                              | 0m00.s    || +0m00.00s | N/A     
+0m00.s    | Chars 119-129 ~ 127-137 [Goal~_~True.]                      | 0m00.s    || +0m00.00s | N/A     
+0m00.s    | Chars 132-140 ~ 140-148 [exact~I.]                          |    N/A    || +0m00.00s | N/A     
+   N/A    | Chars 132-144 ~ 140-152 [constructor.]                      | 0m00.s    || +0m00.00s | N/A     
+0m00.s    | Chars 141-145 ~ 153-157 [Qed.]                              | 0m00.s    || +0m00.00s | N/A     
+0m00.s    | Chars 146-156 ~ 158-168 [Goal~_~True.]                      | 0m00.s    || +0m00.00s | N/A     
+0m00.s    | Chars 159-167 ~ 171-179 [exact~I.]                          |    N/A    || +0m00.00s | N/A     
+   N/A    | Chars 159-171 ~ 171-183 [constructor.]                      | 0m00.s    || +0m00.00s | N/A     
+0m00.s    | Chars 168-172 ~ 184-188 [Qed.]                              | 0m00.s    || +0m00.00s | N/A     
+0m00.s    | Chars 173-183 ~ 189-199 [Goal~_~True.]                      | 0m00.s    || +0m00.00s | N/A     
+0m00.s    | Chars 186-194 ~ 202-210 [exact~I.]                          |    N/A    || +0m00.00s | N/A     
+   N/A    | Chars 186-198 ~ 202-214 [constructor.]                      | 0m00.s    || +0m00.00s | N/A     
+0m00.s    | Chars 195-199 ~ 215-219 [Qed.]                              | 0m00.s    || +0m00.00s | N/A     
+0m00.s    | Chars 200-257 ~ 220-277 [Goal~_~List.repeat~Z.div_eucl~...] | 0m00.s    || +0m00.00s | N/A     
\ No newline at end of file
diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo-user.v.timing.diff.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo-user.v.timing.diff.expected
new file mode 100644
index 0000000000..f6be1d936d
--- /dev/null
+++ b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo-user.v.timing.diff.expected
@@ -0,0 +1,29 @@
+After     | Code                                                        | Before    || Change    | % Change
+-----------------------------------------------------------------------------------------------------------
+0m01.14s  | Total                                                       | 0m01.15s  || -0m00.00s | -0.77%  
+-----------------------------------------------------------------------------------------------------------
+0m00.504s | Chars 260-284 ~ 280-304 [(vm_compute;~reflexivity).]        | 0m00.528s || -0m00.02s | -4.54%  
+0m00.384s | Chars 285-289 ~ 305-309 [Qed.]                              | 0m00.4s   || -0m00.01s | -4.00%  
+0m00.172s | Chars 031-064 ~ 031-064 [Require~Import~Coq.ZArith.ZArith.] | 0m00.156s || +0m00.01s | +10.25% 
+0m00.083s | Chars 000-030 ~ 000-030 [Require~Import~Coq.Lists.List.]    | 0m00.072s || +0m00.01s | +15.27% 
+0m00.004s | Chars 200-257 ~ 220-277 [Goal~_~List.repeat~Z.div_eucl~...] | 0m00.s    || +0m00.00s | ∞       
+0m00.s    | Chars 065-075 ~ 065-075 [Goal~_~True.]                      | 0m00.s    || +0m00.00s | N/A     
+0m00.s    | Chars 078-086 ~ 078-086 [exact~I.]                          |    N/A    || +0m00.00s | N/A     
+   N/A    | Chars 078-090 ~ 078-090 [constructor.]                      | 0m00.s    || +0m00.00s | N/A     
+0m00.s    | Chars 087-091 ~ 091-095 [Qed.]                              | 0m00.s    || +0m00.00s | N/A     
+0m00.s    | Chars 092-102 ~ 096-106 [Goal~_~True.]                      | 0m00.s    || +0m00.00s | N/A     
+0m00.s    | Chars 105-113 ~ 109-117 [exact~I.]                          |    N/A    || +0m00.00s | N/A     
+   N/A    | Chars 105-117 ~ 109-121 [constructor.]                      | 0m00.s    || +0m00.00s | N/A     
+0m00.s    | Chars 114-118 ~ 122-126 [Qed.]                              | 0m00.s    || +0m00.00s | N/A     
+0m00.s    | Chars 119-129 ~ 127-137 [Goal~_~True.]                      | 0m00.s    || +0m00.00s | N/A     
+0m00.s    | Chars 132-140 ~ 140-148 [exact~I.]                          |    N/A    || +0m00.00s | N/A     
+   N/A    | Chars 132-144 ~ 140-152 [constructor.]                      | 0m00.s    || +0m00.00s | N/A     
+0m00.s    | Chars 141-145 ~ 153-157 [Qed.]                              | 0m00.s    || +0m00.00s | N/A     
+0m00.s    | Chars 146-156 ~ 158-168 [Goal~_~True.]                      | 0m00.s    || +0m00.00s | N/A     
+0m00.s    | Chars 159-167 ~ 171-179 [exact~I.]                          |    N/A    || +0m00.00s | N/A     
+   N/A    | Chars 159-171 ~ 171-183 [constructor.]                      | 0m00.s    || +0m00.00s | N/A     
+0m00.s    | Chars 168-172 ~ 184-188 [Qed.]                              | 0m00.s    || +0m00.00s | N/A     
+0m00.s    | Chars 173-183 ~ 189-199 [Goal~_~True.]                      | 0m00.s    || +0m00.00s | N/A     
+0m00.s    | Chars 186-194 ~ 202-210 [exact~I.]                          |    N/A    || +0m00.00s | N/A     
+   N/A    | Chars 186-198 ~ 202-214 [constructor.]                      | 0m00.s    || +0m00.00s | N/A     
+0m00.s    | Chars 195-199 ~ 215-219 [Qed.]                              | 0m00.s    || +0m00.00s | N/A     
\ No newline at end of file
diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo.v.after-timing.in b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo.v.after-timing.in
new file mode 100644
index 0000000000..c58e7d82d1
--- /dev/null
+++ b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo.v.after-timing.in
@@ -0,0 +1,20 @@
+Chars 0 - 30 [Require~Import~Coq.Lists.List.] 0.114 secs (0.083u,0.032s)
+Chars 31 - 64 [Require~Import~Coq.ZArith.ZArith.] 0.194 secs (0.172u,0.023s)
+Chars 65 - 75 [Goal~_~True.] 0. secs (0.u,0.s)
+Chars 78 - 86 [exact~I.] 0. secs (0.u,0.s)
+Chars 87 - 91 [Qed.] 0. secs (0.u,0.s)
+Chars 92 - 102 [Goal~_~True.] 0. secs (0.u,0.s)
+Chars 105 - 113 [exact~I.] 0. secs (0.u,0.s)
+Chars 114 - 118 [Qed.] 0. secs (0.u,0.s)
+Chars 119 - 129 [Goal~_~True.] 0. secs (0.u,0.s)
+Chars 132 - 140 [exact~I.] 0. secs (0.u,0.s)
+Chars 141 - 145 [Qed.] 0. secs (0.u,0.s)
+Chars 146 - 156 [Goal~_~True.] 0. secs (0.u,0.s)
+Chars 159 - 167 [exact~I.] 0. secs (0.u,0.s)
+Chars 168 - 172 [Qed.] 0. secs (0.u,0.s)
+Chars 173 - 183 [Goal~_~True.] 0. secs (0.u,0.s)
+Chars 186 - 194 [exact~I.] 0. secs (0.u,0.s)
+Chars 195 - 199 [Qed.] 0. secs (0.u,0.s)
+Chars 200 - 257 [Goal~_~List.repeat~Z.div_eucl~...] 0. secs (0.004u,0.s)
+Chars 260 - 284 [(vm_compute;~reflexivity).] 0.53 secs (0.504u,0.024s)
+Chars 285 - 289 [Qed.] 0.4 secs (0.384u,0.016s)
diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo.v.before-timing.in b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo.v.before-timing.in
new file mode 100644
index 0000000000..b49c1b1cb7
--- /dev/null
+++ b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo.v.before-timing.in
@@ -0,0 +1,20 @@
+Chars 0 - 30 [Require~Import~Coq.Lists.List.] 0.114 secs (0.072u,0.044s)
+Chars 31 - 64 [Require~Import~Coq.ZArith.ZArith.] 0.192 secs (0.156u,0.035s)
+Chars 65 - 75 [Goal~_~True.] 0. secs (0.u,0.s)
+Chars 78 - 90 [constructor.] 0. secs (0.u,0.s)
+Chars 91 - 95 [Qed.] 0. secs (0.u,0.s)
+Chars 96 - 106 [Goal~_~True.] 0. secs (0.u,0.s)
+Chars 109 - 121 [constructor.] 0. secs (0.u,0.s)
+Chars 122 - 126 [Qed.] 0. secs (0.u,0.s)
+Chars 127 - 137 [Goal~_~True.] 0. secs (0.u,0.s)
+Chars 140 - 152 [constructor.] 0. secs (0.u,0.004s)
+Chars 153 - 157 [Qed.] 0. secs (0.u,0.s)
+Chars 158 - 168 [Goal~_~True.] 0. secs (0.u,0.s)
+Chars 171 - 183 [constructor.] 0. secs (0.u,0.s)
+Chars 184 - 188 [Qed.] 0. secs (0.u,0.s)
+Chars 189 - 199 [Goal~_~True.] 0. secs (0.u,0.s)
+Chars 202 - 214 [constructor.] 0. secs (0.u,0.s)
+Chars 215 - 219 [Qed.] 0. secs (0.u,0.s)
+Chars 220 - 277 [Goal~_~List.repeat~Z.div_eucl~...] 0. secs (0.u,0.s)
+Chars 280 - 304 [(vm_compute;~reflexivity).] 0.566 secs (0.528u,0.039s)
+Chars 305 - 309 [Qed.] 0.411 secs (0.4u,0.008s)
diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo_after.v b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo_after.v
new file mode 100644
index 0000000000..7141065b52
--- /dev/null
+++ b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo_after.v
@@ -0,0 +1,20 @@
+Require Import Coq.Lists.List.
+Require Import Coq.ZArith.ZArith.
+Goal True.
+  exact I.
+Qed.
+Goal True.
+  exact I.
+Qed.
+Goal True.
+  exact I.
+Qed.
+Goal True.
+  exact I.
+Qed.
+Goal True.
+  exact I.
+Qed.
+Goal List.repeat Z.div_eucl 5 = List.repeat Z.div_eucl 5.
+  vm_compute; reflexivity.
+Qed.
diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo_before.v b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo_before.v
new file mode 100644
index 0000000000..e152689ee4
--- /dev/null
+++ b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo_before.v
@@ -0,0 +1,20 @@
+Require Import Coq.Lists.List.
+Require Import Coq.ZArith.ZArith.
+Goal True.
+  constructor.
+Qed.
+Goal True.
+  constructor.
+Qed.
+Goal True.
+  constructor.
+Qed.
+Goal True.
+  constructor.
+Qed.
+Goal True.
+  constructor.
+Qed.
+Goal List.repeat Z.div_eucl 5 = List.repeat Z.div_eucl 5.
+  vm_compute; reflexivity.
+Qed.
diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/run.sh b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/run.sh
new file mode 100755
index 0000000000..980bf9cf01
--- /dev/null
+++ b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/run.sh
@@ -0,0 +1,14 @@
+#!/usr/bin/env bash
+
+set -x
+set -e
+
+cd "$(dirname "${BASH_SOURCE[0]}")"
+
+"$COQLIB"/tools/make-both-single-timing-files.py --fuzz=20 foo.v.after-timing.in foo.v.before-timing.in foo-real.v.timing.diff || exit $?
+
+diff -u foo-real.v.timing.diff.expected foo-real.v.timing.diff || exit $?
+
+"$COQLIB"/tools/make-both-single-timing-files.py --fuzz=20 --user foo.v.after-timing.in foo.v.before-timing.in foo-user.v.timing.diff || exit $?
+
+diff -u foo-user.v.timing.diff.expected foo-user.v.timing.diff || exit $?
diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh b/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh
index cfacf738a3..4b5acb9168 100755
--- a/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh
+++ b/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh
@@ -10,3 +10,4 @@ export COQLIB
 ./001-correct-diff-sorting-order/run.sh
 ./002-single-file-sorting/run.sh
 ./003-non-utf8/run.sh
+./004-per-file-fuzz/run.sh