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 | |
| 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.
| -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"; \ |