Update TimeFileMaker.py to correctly sort timing diffs #6149
Conversation
JasonGross
added
kind: fix
JasonGross
force-pushed
the
fix-timing-sorting-order
branch
2 times, most recently
from
09a4b85
to
ffa60a7
Compare
|
The test suite fails. |
|
Okay, hopefully it'll work now. |
JasonGross
force-pushed
the
fix-timing-sorting-order
branch
2 times, most recently
from
c6bca0a
to
9b51cb2
Compare
|
Test-suite now builds on my machine |
|
I haven't really looked at the timing tests that were there before nor those that are added by this PR but I'm a bit worried about the potential for non-deterministic results, given our past experience with these. |
|
@Zimmi48 The ones that were there before are unchanged. The ones I added do not invoke the time command. I checked in the output of |
|
Strange failure on AppVeyor. Rebuilding. |
| @@ -0,0 +1,4 @@ | |||
| set -e | |||
| set -o pipefail | |||
There was a problem hiding this comment.
Why do you need both set invocations?
There was a problem hiding this comment.
Actually this is dead code, I'll remove the file.
|
I think the strange AppVeyor failure still occurred. The linter also reports some problems. |
|
But the linter error should probably be ignored because they probably concern only test-suite output files. If these files had a |
|
Argh, the AppVeyor failure is because, on Windows, we're compiling a version of Coq that's incompatible with command-line tools, such as |
|
@Zimmi48 What should I do about the linter? They concern test-suite output files, but naming them |
|
You may adapt the AppVeyor script to install more commands, @maximedenes may help here. You can just ignore the linter or ask @SkySkimmer his advice. |
|
You could have a .gitattributes in a subdirectory with only the output files, containing |
|
@Zimmi48 Huh? The issue is that |
|
@SkySkimmer like ff03258 ? (to capture all |
|
Hum OK I hadn't correctly understood the issue. |
Yes, but you need to rebase it to the beginning of your branch so that your commits happen with it already existing. |
Previously, it was reverse-ordering timing diffs.
These work on precomputed build logs (in this case, from a recent partial build of fiat-crypto). They are meant to serve as human-readable sanity checks of output format. Separate out the sane bits of template/init.sh from the ones messing with directory structure (which are fragile and make assumptions about where the calling script is sourcing it from). N.B. The test-suite removes all *.log files, so we use *.log.in. N.B. We set COQLIB in precomputed-time-tests/run.sh, not the Makefile, because coqc, on Windows, doesn't handle cygwin paths passed via -coqlib, and `pwd` gives cygwin paths. N.B. We have .gitattributes to satisfy the linter (as per coq#6149 (comment))
JasonGross
force-pushed
the
fix-timing-sorting-order
branch
from
ff03258
to
e87c3f9
Compare
|
Rebased and squashed |
SkySkimmer
added
kind: tests
kind: infrastructure
|
This seems Ok [travis failed on vst timeout] |
These work on precomputed build logs (in this case, from a recent partial build of fiat-crypto). They are meant to serve as human-readable sanity checks of output format. Separate out the sane bits of template/init.sh from the ones messing with directory structure (which are fragile and make assumptions about where the calling script is sourcing it from). N.B. The test-suite removes all *.log files, so we use *.log.in. N.B. We set COQLIB in precomputed-time-tests/run.sh, not the Makefile, because coqc, on Windows, doesn't handle cygwin paths passed via -coqlib, and `pwd` gives cygwin paths. N.B. We have .gitattributes to satisfy the linter (as per coq#6149 (comment)) (cherry picked from commit e87c3f9)
Previously, it was reverse-ordering timing diffs.
Also add some tests on precomputed logs (from fiat-crypto) as a human-readable sanity-check.