diff options
| author | Jason Gross | 2019-12-18 20:39:06 -0500 |
|---|---|---|
| committer | Jason Gross | 2019-12-19 09:13:20 -0500 |
| commit | baab1c01b22d754df64a09be436d350663cc1c28 (patch) | |
| tree | ea36da8ff129456033af7f62d209b9ee26f3d110 /test-suite | |
| parent | 6b309b4297f28fcc6774ac3a19ab830713ec5e62 (diff) | |
Better error reporting when res is not what is expected
c.f. https://dev.azure.com/coq/coq/_build/results?buildId=6485&view=logs&jobId=2d2b3007-3c5c-5840-9bb0-2b1ea49925f3&j=2d2b3007-3c5c-5840-9bb0-2b1ea49925f3&t=77aad734-2057-5694-9ae2-ee1f5f26eae8
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/Makefile | 28 |
1 files changed, 17 insertions, 11 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 7e2ef3bc75..1546b7cf62 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -540,19 +540,25 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v $(PREREQUISITELOG) echo " $<...Error! (couldn't find a time measure)"; \ else \ true "express effective time in centiseconds"; \ + resorig="$$res"; \ res=`echo "$$res"00 | sed -n -e "s/\([0-9]*\)\.\([0-9][0-9]\).*/\1\2/p"`; \ - true "find expected time * 100"; \ - exp=`sed -n -e "s/(\*.*Expected time < \([0-9]\).\([0-9][0-9]\)s.*\*)/\1\2/p" "$<"`; \ - true "compute corrected effective time, rounded up"; \ - rescorrected=`expr \( $$res \* $(bogomips) + 6120 - 1 \) / 6120`; \ - ok=`expr \( $$res \* $(bogomips) \) "<" \( $$exp \* 6120 \)`; \ - if [ "$$ok" = 1 ]; then \ - echo $(log_success); \ - echo " $<...Ok"; \ - else \ + if [ "$$res" = "" ]; then \ echo $(log_failure); \ - echo " $<...Error! (should run faster ($$rescorrected >= $$exp))"; \ - $(FAIL); \ + echo " $<...Error! (invalid time measure: $$resorig)"; \ + else \ + true "find expected time * 100"; \ + exp=`sed -n -e "s/(\*.*Expected time < \([0-9]\).\([0-9][0-9]\)s.*\*)/\1\2/p" "$<"`; \ + true "compute corrected effective time, rounded up"; \ + rescorrected=`expr \( $$res \* $(bogomips) + 6120 - 1 \) / 6120`; \ + ok=`expr \( $$res \* $(bogomips) \) "<" \( $$exp \* 6120 \)`; \ + if [ "$$ok" = 1 ]; then \ + echo $(log_success); \ + echo " $<...Ok"; \ + else \ + echo $(log_failure); \ + echo " $<...Error! (should run faster ($$rescorrected >= $$exp))"; \ + $(FAIL); \ + fi; \ fi; \ fi; \ } > "$@" |