From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 24 Jun 2005 08:35:26 +0000 (+0000)
Subject: first snapshot of the night-profiling
X-Git-Tag: INDEXING_NO_PROOFS~84
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9d8e81db720417f58591ea42f72c6750b886a83d;p=helm.git

first snapshot of the night-profiling
---

diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in
index 1ace35ca4..428492209 100644
--- a/helm/matita/Makefile.in
+++ b/helm/matita/Makefile.in
@@ -63,7 +63,7 @@ matita.opt: $(LIBX_DEPS) $(CMXS) matita.ml
 
 matitac: $(LIB_DEPS) $(CCMOS) matitac.ml
 	$(OCAMLC) $(CPKGS) -linkpkg -o $@ $(CCMOS) matitac.ml
-matitac.opt: $(LIBX_DEPS) $(CMXS) matitac.ml
+matitac.opt: $(LIBX_DEPS) $(CCMXS) matitac.ml
 	$(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) matitac.ml
 
 cicbrowser: matita
@@ -94,9 +94,11 @@ distclean: clean
 	rm -f matita.glade.bak matita.gladep.bak
 	rm -rf autom4te.cache/
 
-tests: matitac
-	for i in tests/*.ma; do (./matitac $$i 2> /dev/null > /dev/null && echo "[OK] $$i") || echo "[KO] $$i"; done
-.PHONY: tests
+tests: matita
+	@scripts/do_tests.sh ./matitac /dev/null tests/*.ma
+tests.opt: matitac.opt
+	@scripts/do_tests.sh ./matitac.opt /dev/null tests/*.ma
+.PHONY: tests tests.opt
 
 tags: TAGS
 .PHONY: TAGS
diff --git a/helm/matita/scripts/bench.sql b/helm/matita/scripts/bench.sql
new file mode 100644
index 000000000..9b5c1e3cd
--- /dev/null
+++ b/helm/matita/scripts/bench.sql
@@ -0,0 +1,17 @@
+DROP TABLE bench;
+
+CREATE TABLE bench (
+	mark VARCHAR(100) NOT NULL,
+	time TIME NOT NULL,
+	compilation ENUM('byte','opt') NOT NULL,
+	test VARCHAR(100) NOT NULL,
+	result ENUM('ok','fail') NOT NULL,
+	options SET('no-gc')
+);
+
+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/do_tests.sh b/helm/matita/scripts/do_tests.sh
new file mode 100755
index 000000000..b95ca578c
--- /dev/null
+++ b/helm/matita/scripts/do_tests.sh
@@ -0,0 +1,40 @@
+#!/bin/bash
+
+OK="\e[32mOK\e[0m"
+FAIL="\e[31mFAIL\e[0m"
+
+if [ "$1" = "-no-color" ]; then
+  shift
+  OK="OK"
+  FAIL="FAIL"
+fi
+
+COMPILER=$1
+shift
+LOGFILE=$1
+shift
+TODO="$@"
+
+if [ -z "$COMPILER" -o -z "$LOGFILE" -o -z "$TODO" ]; then
+  echo
+  echo "usage: "
+  echo "  do_tests.sh [-no-color] ./compiler logfile tests.ma ..."
+  echo
+  echo "The value of the DO_TESTS_EXTRA evironment variable"
+  echo "will be appended to each line."
+  exit 1
+fi
+
+TMP=.__temp.txt
+
+for T in $TODO; do
+  echo -en "$COMPILER\t$T\t"
+  /usr/bin/time -o $TMP -f "%E\t%U\t%S" $COMPILER $T >> $LOGFILE 2>&1
+  if [ $? = 0 ]; then
+    echo -e "$OK\t`cat $TMP`\t$DO_TESTS_EXTRA"
+  else
+    echo -e "$FAIL\t`cat $TMP`\t$DO_TESTS_EXTRA"
+  fi
+done
+
+rm $TMP
diff --git a/helm/matita/scripts/insert.awk b/helm/matita/scripts/insert.awk
new file mode 100644
index 000000000..267e893e2
--- /dev/null
+++ b/helm/matita/scripts/insert.awk
@@ -0,0 +1,18 @@
+
+
+/^[^#]/ {
+	result=tolower($1);
+	if( $2 ~ "\.opt$" )
+		compilation="opt"
+	else
+		compilation="byte"
+	test=$3	
+	time="0:" $4
+	mark=$7
+	if ( $8 ~ "^GC=off$") 
+		options="'no-gc'"
+	else
+		options="''"
+		
+	printf "INSERT bench (result, compilation, test, time, mark, options) VALUES ('%s', '%s', '%s', '%s', '%s', %s);\n", result, compilation, test, time, mark, options;
+	}
diff --git a/helm/matita/scripts/profile_cvs.sh b/helm/matita/scripts/profile_cvs.sh
new file mode 100755
index 000000000..63eeee22d
--- /dev/null
+++ b/helm/matita/scripts/profile_cvs.sh
@@ -0,0 +1,41 @@
+#!/bin/bash
+MARK=`date +%Y%m%d`
+TMPDIRNAME=.__$MARK
+CVSROOT=":ext:$USER@marcello.cs.unibo.it:/home/faculty/PROJECTS/cvs/helm"
+
+function testit {
+  MARK=`date +%Y%m%d`
+  LOGTOOPT=/dev/null
+  LOGTOBYTE=/dev/null
+  export DO_TESTS_EXTRA="$MARK\t$n"
+  ls
+  scripts/do_tests.sh -nocolor ./matitac.opt $LOGTOOPT tests/*.ma
+  scripts/do_tests.sh -nocolor ./matitac $LOGTOBYTE tests/*.ma
+}
+
+function compile {
+  make -C $1 all opt 1>/dev/null 2>/dev/null
+  make -C $2 matitac matitac.opt 1>/dev/null 2>/dev/null
+}
+
+function run_tests {
+  OLD=`pwd`
+  cd $1
+  export OCAMLRUNPARAM='o=1000000'
+  testit $IMPL "off" 1>/dev/null 2>/dev/null
+  testit $IMPL "off"
+  export OCAMLRUNPARAM=''
+  testit $IMPL "on" 1>/dev/null 2>/dev/null
+  testit $IMPL "on"
+  cd $OLD
+}
+
+rm -rf $TMPDIRNAME
+mkdir $TMPDIRNAME
+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
+