From d768015a3f7667525fd3daa8d5a83122b9d8dcaa Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 2 Apr 2018 15:22:26 -0400 Subject: Update coq_makefile timing test This fixes #5675 (in yet another way). The issue was that `$` (end of string regex) was not properly escaped in `"`s. This handles the issue that is displayed in ``` cat A.v.timing.diff After | Code | Before || Change | % Change --------------------------------------------------------------------------------------------------- 0m01.44s | Total | 0m01.56s || -0m00.12s | -7.92% --------------------------------------------------------------------------------------------------- 0m00.609s | Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] | 0m00.627s || -0m00.01s | -2.87% 0m00.527s | Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] | 0m00.552s || -0m00.02s | -4.52% 0m00.304s | Chars 000 - 026 [Require~Coq.ZArith.BinInt.] | 0m00.379s || -0m00.07s | -19.78% N/A | Chars 027 - 068 [Declare~Reduction~comp~:=~nati...] | 0m00.006s || -0m00.00s | -100.00% 0m00.s | Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] | N/A || +0m00.00s | N/A --- A.v.timing.diff.desired.processed 2018-03-23 22:22:19.000000000 +0000 +++ A.v.timing.diff.processed 2018-03-23 22:22:19.000000000 +0000 @@ -1,4 +1,4 @@ - N/A | Chars 27 - 68 [Declare~Reduction~comp~:=~nati] | ms || -ms | N/A + N/A | Chars 27 - 68 [Declare~Reduction~comp~:=~nati] | ms || -ms | -% ------ ------ After | Code | Before || Change | % Change ``` where, because `Declare Reduction` takes 0.006s rather than 0s, the % change shows up as -100% rather than N/A. --- test-suite/coq-makefile/timing/run.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test-suite/coq-makefile') diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh index aa6b0a9a4..43c83e412 100755 --- a/test-suite/coq-makefile/timing/run.sh +++ b/test-suite/coq-makefile/timing/run.sh @@ -40,7 +40,7 @@ INFINITY_REPLACEMENT="+.%" # assume that if the before time is zero, we expected TO_SED_IN_BOTH=( -e s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" # Whether or not something shows up as ∞ depends on whether a time registers as 0.s or as 0.001s, so we can't rely on this being consistent - -e s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" # Whether or not something shows up as N/A depends on whether a time registers as 0.s or as 0.001s, so we can't rely on this being consistent + -e s':|\s*N/A\s*$:| '"${INFINITY_REPLACEMENT}"':g' # Whether or not something shows up as N/A depends on whether a time registers as 0.s or as 0.001s, so we can't rely on this being consistent -e s'/ *$//g' # the number of trailing spaces depends on how many digits percentages end up being; since this varies across runs, we remove trailing spaces -e s'/[0-9]*\.[0-9]*//g' # the precise timing numbers vary, so we strip them out -e s'/^-*$/------/g' # When none of the numbers get over 100 (or 1000, in per-file), the width of the table is different, so we normalize the number of dashes for table separators -- cgit v1.2.3