X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fscripts%2Fprofile_cvs.sh;h=9b1065c127b01493f05de644b9f7d9fe81e8236c;hb=f981a524748846acc29b76b6e616af110b4ee13d;hp=8659223236015e2bd71f8a08b795c23db30f4fc8;hpb=1f6509593d89bf91237cceb1ace0be4fdbf4335c;p=helm.git diff --git a/helm/matita/scripts/profile_cvs.sh b/helm/matita/scripts/profile_cvs.sh index 865922323..9b1065c12 100755 --- a/helm/matita/scripts/profile_cvs.sh +++ b/helm/matita/scripts/profile_cvs.sh @@ -7,14 +7,13 @@ 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 -no-color ./matitac.opt $LOGTOOPT tests/*.ma - #scripts/do_tests.sh -nocolor ./matitac $LOGTOBYTE tests/*.ma + export DO_TESTS_EXTRA="$MARK\t$@" + make tests DO_TESTS_OPTS="-no-color -twice" + make tests.opt DO_TESTS_OPTS="-no-color -twice" } function compile { - OLD=$PWD + LOCALOLD=$PWD cd $1 autoconf 1>/dev/null ./configure 1>/dev/null @@ -22,30 +21,32 @@ function compile { cd $2 autoconf 1>/dev/null ./configure 1>/dev/null - make matitac matitac.opt updater 1>/dev/null - sed "s/@@OWNER@@/profiler/" matita.conf.xml.sample > matita.conf.xml - ./updater - cd $OLD + cp matita.conf.xml.sample matita.conf.xml + make all opt 1>/dev/null + cd $LOCALOLD } function run_tests { - OLD=$PWD + LOCALOLD=$PWD cd $1 + ./matitaclean all + mkdir .matita export OCAMLRUNPARAM='o=1000000' - #testit $IMPL "off" 1>/dev/null 2>/dev/null - testit $IMPL "off" + testit "gc-off" export OCAMLRUNPARAM='' - #testit $IMPL "on" 1>/dev/null 2>/dev/null - #testit $IMPL "on" - cd $OLD + testit "gc-on" + cd $LOCALOLD } +OLD=$PWD 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 -#rm -rf $TMPDIRNAME - +run_tests $PWD/helm/matita > LOG 2>/dev/null +cat LOG | grep -v "^.......Debug:" | grep -v "^make[1]: " | awk -f $PWD/helm/matita/scripts/insert.awk > INSERT.sql +cat INSERT.sql | mysql -u helm -h mowgli.cs.unibo.it matita +cd $OLD +rm -rf $TMPDIRNAME