New format for benches (with much more precision).

diff --git a/helm/matita/scripts/bench.sql b/helm/matita/scripts/bench.sql
index b7e1bef7eb4239cab043504e976d388c59a86525..a45508548bab6b7ba929cb3e624332234ba597cf 100644 (file)
--- 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 a195b9cf0ee4ba816e29bbe917e3d2101db7c8de..5e8b0d583bda5f1cd31f768fc61f609089fc38e7 100755 (executable)
--- 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 c881c0966520b9e5b8aa22c9f7f16af7f1dd4c89..d62a6a3ecdc2aef395833e1a6a04dc068c017288 100644 (file)
--- 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 dc6c5215b91fd2edf4fdae74bf98e3a2409352aa..8f55fcdd8f722aa5f53fdca227f364ae5fb37013 100755 (executable)
--- 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"