From: Claudio Sacerdoti Coen Date: Fri, 28 Oct 2005 16:28:24 +0000 (+0000) Subject: New format for benches (with much more precision). X-Git-Tag: V_0_7_2_3~174 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dc9506be01f197dd60900f10ae2875240e26b761;p=helm.git New format for benches (with much more precision). --- diff --git a/helm/matita/scripts/bench.sql b/helm/matita/scripts/bench.sql index b7e1bef7e..a45508548 100644 --- a/helm/matita/scripts/bench.sql +++ b/helm/matita/scripts/bench.sql @@ -2,8 +2,8 @@ DROP TABLE bench; CREATE TABLE bench ( mark VARCHAR(100) NOT NULL, - time TIME NOT NULL, - timeuser TIME NOT NULL, + time VARCHAR(8) NOT NULL, + timeuser VARCHAR(8) NOT NULL, compilation ENUM('byte','opt') NOT NULL, test VARCHAR(100) NOT NULL, result ENUM('ok','fail') NOT NULL, diff --git a/helm/matita/scripts/do_tests.sh b/helm/matita/scripts/do_tests.sh index a195b9cf0..5e8b0d583 100755 --- a/helm/matita/scripts/do_tests.sh +++ b/helm/matita/scripts/do_tests.sh @@ -37,6 +37,7 @@ fi TMP=.__temp.txt +export TIMEFORMAT="%2lR %2lU %2lS" for T in $TODO; do printf "$COMPILER\t%-30s " $T if [ "$TWICE" = "1" ]; then @@ -44,14 +45,12 @@ for T in $TODO; do $COMPILER $T 1>/dev/null 2>/dev/null fi $CLEANER $T 1>/dev/null 2>/dev/null - /usr/bin/time --quiet -o $TMP -f "%E %U %S" $COMPILER $T >> $LOGFILE 2>&1 + TIMES=`(time $COMPILER $T >> $LOGFILE 2>&1) 2>&1` RC=$?; if [ $RC = 0 ]; then - printf "$OK\t`cat $TMP`\t$DO_TESTS_EXTRA\n" - rm $TMP + printf "$OK\t$TIMES\t$DO_TESTS_EXTRA\n" else - printf "$FAIL\t`cat $TMP`\t$DO_TESTS_EXTRA\n"; - rm $TMP + printf "$FAIL\t$TIMES\t$DO_TESTS_EXTRA\n"; exit $RC fi done diff --git a/helm/matita/scripts/insert.awk b/helm/matita/scripts/insert.awk index c881c0966..d62a6a3ec 100644 --- a/helm/matita/scripts/insert.awk +++ b/helm/matita/scripts/insert.awk @@ -5,8 +5,8 @@ else compilation="byte" test=$2 - time="0:" $4 - timeuser="0:0:" $5 + time=$4 + timeuser=$5 mark=$7 if ( $8 ~ "^gc-off$") options="'gc-off'"; diff --git a/helm/matita/scripts/profile_cvs.sh b/helm/matita/scripts/profile_cvs.sh index dc6c5215b..8f55fcdd8 100755 --- a/helm/matita/scripts/profile_cvs.sh +++ b/helm/matita/scripts/profile_cvs.sh @@ -1,5 +1,5 @@ #!/bin/bash -MARK=`date +%Y%m%d` +MARK=`date +%Y%m%d%H%M` TMPDIRNAME=.__$MARK CVSROOT=":ext:$USER@marcello.cs.unibo.it:/home/faculty/PROJECTS/cvs/helm"