nigth-bench snapshot

diff --git a/helm/matita/scripts/bench.sql b/helm/matita/scripts/bench.sql
index 9b5c1e3cd72c9d4eacd183d0a96a9f122fa4c427..b7e1bef7eb4239cab043504e976d388c59a86525 100644 (file)
--- a/helm/matita/scripts/bench.sql
+++ b/helm/matita/scripts/bench.sql
@@ -3,15 +3,11 @@ DROP TABLE bench;
 CREATE TABLE bench (
        mark VARCHAR(100) NOT NULL,
        time TIME NOT NULL,
+       timeuser TIME NOT NULL,
        compilation ENUM('byte','opt') NOT NULL,
        test VARCHAR(100) NOT NULL,
        result ENUM('ok','fail') NOT NULL,
-       options SET('no-gc')
+       options SET('gc-off','gc-on')
 );
 
 DESCRIBE bench; 
-
-select mark, SEC_TO_TIME(SUM(TIME_TO_SEC(time))) from bench where options = '' group by mark;
-select mark, SEC_TO_TIME(SUM(TIME_TO_SEC(time))) from bench where test LIKE '%uto.ma' and options = '' group by mark;
-select mark, SEC_TO_TIME(SUM(TIME_TO_SEC(time))) from bench where options = 'no-gc' group by mark;
-select mark, SEC_TO_TIME(SUM(TIME_TO_SEC(time))) from bench where test LIKE '%uto.ma' and options = 'no-gc' group by mark;

diff --git a/helm/matita/scripts/insert.awk b/helm/matita/scripts/insert.awk
index 267e893e2b967aa1a301179753af6ba8d0da2ac1..e38f341edb0a3122f09b2f5ad48077d768e138a4 100644 (file)
--- a/helm/matita/scripts/insert.awk
+++ b/helm/matita/scripts/insert.awk
@@ -1,18 +1,17 @@
-
-
-/^[^#]/ {
-       result=tolower($1);
-       if( $2 ~ "\.opt$" )
+ {
+       result=tolower($3);
+       if( $1 ~ "\.opt$" )
                compilation="opt"
        else
                compilation="byte"
-       test=$3 
+       test=$2 
        time="0:" $4
+       timeuser="0:0:" $5
        mark=$7
-       if ( $8 ~ "^GC=off$") 
-               options="'no-gc'"
-       else
-               options="''"
+       if ( $8 ~ "^gc-off$") 
+               options="'gc-off'";
+       if ( $8 ~ "^gc-on$") 
+               options="'gc-on'"
                
-       printf "INSERT bench (result, compilation, test, time, mark, options) VALUES ('%s', '%s', '%s', '%s', '%s', %s);\n", result, compilation, test, time, mark, options;
+       printf "INSERT bench (result, compilation, test, time, timeuser, mark, options) VALUES ('%s', '%s', '%s', '%s', '%s', '%s', %s);\n", result, compilation, test, time, timeuser, mark, options;
        }

diff --git a/helm/matita/scripts/profile_cvs.sh b/helm/matita/scripts/profile_cvs.sh
index 8659223236015e2bd71f8a08b795c23db30f4fc8..7b41cb943505dd5401944be8ed2759f37b1d86fa 100755 (executable)
--- a/helm/matita/scripts/profile_cvs.sh
+++ b/helm/matita/scripts/profile_cvs.sh
@@ -7,7 +7,7 @@ function testit {
   MARK=`date +%Y%m%d`
   LOGTOOPT=/dev/null
   LOGTOBYTE=/dev/null
-  export DO_TESTS_EXTRA="$MARK\t$n"
+  export DO_TESTS_EXTRA="$MARK\t$2"
   ls
   scripts/do_tests.sh -no-color ./matitac.opt $LOGTOOPT tests/*.ma
   #scripts/do_tests.sh -nocolor ./matitac $LOGTOBYTE tests/*.ma
@@ -32,11 +32,11 @@ function run_tests {
   OLD=$PWD
   cd $1
   export OCAMLRUNPARAM='o=1000000'
-  #testit $IMPL "off" 1>/dev/null 2>/dev/null
-  testit $IMPL "off"
+  testit $IMPL "gc-off" 1>/dev/null 2>/dev/null
+  testit $IMPL "gc-off"
   export OCAMLRUNPARAM=''
-  #testit $IMPL "on" 1>/dev/null 2>/dev/null
-  #testit $IMPL "on"
+  testit $IMPL "gc-on" 1>/dev/null 2>/dev/null
+  testit $IMPL "gc-on"
   cd $OLD
 }
 
@@ -46,6 +46,8 @@ cd $TMPDIRNAME
 cvs -d $CVSROOT co helm/ocaml 1>/dev/null 2>/dev/null
 cvs -d $CVSROOT co helm/matita 1>/dev/null 2>/dev/null
 compile $PWD/helm/ocaml $PWD/helm/matita
-run_tests $PWD/helm/matita #> LOG
+run_tests $PWD/helm/matita > LOG
+cat LOG | awk -f $PWD/helm/matita/scripts/insert.awk > INSERT.sql
+cat INSERT.sql | mysql -u helm matita
 #rm -rf $TMPDIRNAME