From 2f4b474295699936bb80f864711ea31a6d24ae38 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 19 Oct 2017 11:59:51 -0400 Subject: Handle ∞ in coq-makefile timing test-suite MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This should (hopefully) fix #5675. --- test-suite/coq-makefile/timing/run.sh | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'test-suite/coq-makefile') diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh index 9786af10a..7e0baaa8f 100755 --- a/test-suite/coq-makefile/timing/run.sh +++ b/test-suite/coq-makefile/timing/run.sh @@ -32,9 +32,12 @@ make print-pretty-timed-diff TIME_OF_BUILD_BEFORE_FILE=../before/time-of-build-b cp ../before/time-of-build-before.log ./ make print-pretty-timed-diff || exit $? +INFINITY="∞" +INFINITY_REPLACEMENT="+.%" # assume that if the before time is zero, we expected the time to increase + for ext in "" .desired; do for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do - cat ${file}${ext} | grep -v 'warning: undefined variable' | sed s'/[0-9]//g' | sed s'/ *$//g' | sed s'/^-*$/------/g' | sed s'/ */ /g' | sed s'/\(Total.*\)-\(.*\)-/\1+\2+/g' > ${file}${ext}.processed + cat ${file}${ext} | grep -v 'warning: undefined variable' | sed s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" | sed s'/[0-9]//g' | sed s'/ *$//g' | sed s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" | sed s'/^-*$/------/g' | sed s'/ */ /g' | sed s'/\(Total.*\)-\(.*\)-/\1+\2+/g' > ${file}${ext}.processed done done for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do @@ -58,7 +61,7 @@ echo for ext in "" .desired; do for file in A.v.timing.diff; do - cat ${file}${ext} | sed s'/[0-9]*\.[0-9]*//g' | sed s'/0//g' | sed s'/ */ /g' | sed s'/+/-/g' | sort > ${file}${ext}.processed + cat ${file}${ext} | sed s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" | sed s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" | sed s'/[0-9]*\.[0-9]*//g' | sed s'/0//g' | sed s'/ */ /g' | sed s'/+/-/g' | sort > ${file}${ext}.processed done done for file in A.v.timing.diff; do -- cgit v1.2.3