From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 24 Jun 2005 09:21:00 +0000 (+0000)
Subject: nigth-bench snapshot
X-Git-Tag: INDEXING_NO_PROOFS~80
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b4f330cf034e930d06aa7bfccb1cecf76f13d069;p=helm.git

nigth-bench snapshot
---

diff --git a/helm/matita/scripts/bench.sql b/helm/matita/scripts/bench.sql
index 9b5c1e3cd..b7e1bef7e 100644
--- 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 267e893e2..e38f341ed 100644
--- 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 865922323..7b41cb943 100755
--- 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