first snapshot of the night-profiling

diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in
index 1ace35ca4daf58b7044a7fdb22e563422265c1e2..428492209c6f4baacd421db3541c560eec715636 100644 (file)
--- 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 "\e[0;32m[OK]\e[0m $$i") || echo "\e[0;31m[KO]\e[0m $$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 (file)
index 0000000..9b5c1e3
--- /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 (executable)
index 0000000..b95ca57
--- /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 (file)
index 0000000..267e893
--- /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 (executable)
index 0000000..63eeee2
--- /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
+