diff options
| author | Hugo Herbelin | 2019-11-28 20:42:11 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-01-04 13:18:16 +0100 |
| commit | 4541dab0cfc3389dee7440b147108d91a7b32840 (patch) | |
| tree | cd6698fde2a9299c71fb7d0f35322183506cd96f /test-suite | |
| parent | 793bddef6b4f615297e9f9088cd0b603c56b2014 (diff) | |
Fixing status reporting for complexity tests.
The regexp parsing the time needed an update to support the case
"Finished failing translation". Also, not all cases of failures were
reported.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/Makefile | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index b3a633e528..1d21b4b5e0 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -530,14 +530,16 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v $(PREREQUISITELOG) $(HIDE){ \ echo $(call log_intro,$<); \ true "extract effective user time"; \ - res=`$(coqc_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 | sed -n -e "s/Finished transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1 | sed "s/\r//g"`; \ + res=`$(coqc_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 | sed -n -e "s/Finished .*transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1 | sed "s/\r//g"`; \ R=$$?; times; \ if [ $$R != 0 ]; then \ echo $(log_failure); \ echo " $<...Error! (should be accepted)" ; \ + $(FAIL); \ elif [ "$$res" = "" ]; then \ echo $(log_failure); \ echo " $<...Error! (couldn't find a time measure)"; \ + $(FAIL); \ else \ true "express effective time in centiseconds"; \ resorig="$$res"; \ |