coq_makefile timing tests are too fragile #5675
Assignees
Labels
help wanted
kind: ci-failure
Information about unexpected and random CI failures.
part: tools
Coqdoc, coq_makefile, etc.
Projects
Milestone
Comments
|
Comment author: @maximedenes Sometimes, tests measure a time of 0.00s, which leads to something like: The infinity symbol is not recognized by the regexp, and the test fails. |
|
Comment author: @JasonGross Would it be sufficient to replace ∞ with the right string (is it .%, or %, or something like that)? |
|
Comment author: @maximedenes Jason, could you have a look at this one? These random failures are annoying. An example here: https://ci.appveyor.com/project/coq/coq/build/master~451/job/nsa1a0712407yijj Thanks! |
|
@JasonGross ping |
|
This is destroying my workflow. Can we please disable this on |
Zimmi48
added this to Non-deterministic test-suite files
in Fix non-deterministic tests
JasonGross
added a commit
to JasonGross/coq
that referenced
this issue
Oct 19, 2017
This should (hopefully) fix coq#5675.
|
Still the tests always fail when |
|
This is really a pain for me. Can we make these tests optional until the issue is fixed? I'll submit a PR, thanks. |
|
@ejgallego if you replace all |
Note that the lines are swapped, will that help?
That looks more promising I think. |
|
The first one seems to be just that the output has changed since coqdep is being run for all files at once in that PR. |
|
Ah well, the other one being related to the timing scripts, that might be a similar issue of the output having changed. |
|
Yes, the first one just needs an update in the output invoking coqdep. The second one fails with which is an error message from |
|
Without doing any debugging, I expect my most recent commit on #6149, d0da687, will fix the second issue, because it removes the directory-structure-mangling from the timing tests (and splits up |
|
Here is another example of random failures due to coq-makefile timing tests: https://travis-ci.org/Zimmi48/coq/jobs/303541424. |
|
@Zimmi48 That log confuses me, and looks like it might actually be a bug in the scripts somewhere. Alas, the log doesn't contain enough info for me to diagnose, so I'm submitting a PR to have the log give more info. |
JasonGross
added a commit
to JasonGross/coq
that referenced
this issue
Nov 17, 2017
This should help debug things like coq#5675 (comment) if they ever show up again.
ejgallego
pushed a commit
to ejgallego/coq
that referenced
this issue
Nov 22, 2017
This should help debug things like coq#5675 (comment) if they ever show up again.
|
Example failure since the printing change https://gitlab.com/SkySkimmer/coq/-/jobs/43401950/artifacts/download |
|
This happened again! |
JasonGross
added a commit
to JasonGross/coq
that referenced
this issue
Apr 2, 2018
This fixes coq#5675 (in yet another way). 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.
JasonGross
added a commit
to JasonGross/coq
that referenced
this issue
Apr 2, 2018
This fixes coq#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.
|
I figured it out. The issue is that in -e s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g"the first |
JasonGross
added a commit
to JasonGross/coq
that referenced
this issue
Apr 2, 2018
This fixes coq#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.
|
Two recent occurrences of |
|
I am starting to think that this code is inherently fragile and is gonna need a full replacement. |
Zimmi48
pushed a commit
to Zimmi48/coq
that referenced
this issue
Apr 10, 2018
This fixes coq#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. (cherry picked from commit d768015)
|
Yet another, very similar failure. We definitely need to reopen this: |
|
New occurrence noticed by @MSoegtropIMC: https://travis-ci.org/coq/coq/jobs/420496623#L4830 |
MSoegtropIMC
added
the
kind: ci-failure
|
@Zimmi48 @MSoegtropIMC I am rather confused by this one. The diff --- A.v.timing.diff.desired.processed 2018-08-25 14:16:28.000000000 +0000
+++ A.v.timing.diff.processed 2018-08-25 14:16:28.000000000 +0000
@@ -4,6 +4,6 @@
After | Code | Before || Change | % Change
ms | Chars - 26 [Require~CoqZArithBinInt] | ms || -ms | -%
ms | Chars 163 - 28 [Definition~foo1~:=~Eval~comp~i] | ms || -ms | -%
-ms | Chars 27 - 68 [Declare~Reduction~comp~:=~vm_c] | N/A || -ms | N/A
+ms | Chars 27 - 68 [Declare~Reduction~comp~:=~vm_c] | N/A || -ms | -%
ms | Chars 69 - 162 [Definition~foo~:=~Eval~comp~i] | ms || -ms | -%
ms | Total | ms || -ms | -%claims that In particular, the line -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 consistentis supposed to catch exactly this case, so I am baffled. This is the case with both https://travis-ci.org/coq/coq/jobs/364720830#L6222 and https://travis-ci.org/coq/coq/jobs/420496623#L4830. #7154 fixed a related thing (at least have fixed it locally)...... |
|
Has this been fixed? |
|
I don't remember seeing a recent occurrence. Let's close this in a few weeks if we don't report new occurrences in the meantime. |
|
New occurrence in: https://gitlab.com/coq/coq/-/jobs/203628478 Test file log: |
|
@Zimmi48, I'm not in front of a computer, but I think you can fix that one with: TO_SED_IN_PER_LINE=(
- -e s'/0//g' # unclear whether this is actually needed above and beyond s'/[0-9]*\.[0-9]*//g'; it's been here from the start
+ -e s'/[0-9]//g' # sometimes the time is under 1 minute, sometimes it's over 1 minute, so we want to remove/normalize both instances; see https://github.com/coq/coq/issues/5675#issuecomment-487378622
-e s'/ */ /g' # Sometimes 0 will show up as 0m00.s, sometimes it'll end up being more like 0m00.001s; we must strip out the spaces that result from left-aligning numbers of different widths based on how many digits Coq's [-time] gives
) |
|
This is at coq/test-suite/coq-makefile/timing/run.sh Line 60 in ae4239d Feel free to combine this replacement rule with the one in 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'/ *$//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
-e s'/+/-/g' # some code lines don't really change, but this can show up as either -0m00.01s or +0m00.01s, so we need to normalize the signs; additionally, some N/A's show up where we expect to get -∞ on the per-line file, and so the ∞-replacement gets the sign wrong, so we must correct it
+ -e s'/[0-9]//g' # sometimes the time is under 1 minute, sometimes it's over 1 minute, so we want to remove/normalize both instances; see https://github.com/coq/coq/issues/5675#issuecomment-487378622
)
TO_SED_IN_PER_FILE=(
- -e s'/[0-9]//g' # unclear whether this is actually needed above and beyond s'/[0-9]*\.[0-9]*//g'; it's been here from the start
-e s'/ */ /g' # unclear whether this is actually needed for per-file timing; it's been here from the start
-e s'/\(Total.*\)-\(.*\)-/\1+\2+/g' # Overall time in the per-file timing diff should be around 0; if it comes out negative, we remove the sign
)
TO_SED_IN_PER_LINE=(
- -e s'/0//g' # unclear whether this is actually needed above and beyond s'/[0-9]*\.[0-9]*//g'; it's been here from the start
-e s'/ */ /g' # Sometimes 0 will show up as 0m00.s, sometimes it'll end up being more like 0m00.001s; we must strip out the spaces that result from left-aligning numbers of different widths based on how many digits Coq's [-time] gives
) |
|
I think we can consider this fixed for now. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Note: the issue was created automatically with bugzilla2github tool
Original bug ID: BZ#5675
From: @maximedenes
Reported version: 8.8+alpha
CC: coq-bugs-redist@lists.gforge.inria.fr
The text was updated successfully, but these errors were encountered: