From 9d8e81db720417f58591ea42f72c6750b886a83d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 24 Jun 2005 08:35:26 +0000 Subject: [PATCH] first snapshot of the night-profiling --- helm/matita/Makefile.in | 10 +++++--- helm/matita/scripts/bench.sql | 17 +++++++++++++ helm/matita/scripts/do_tests.sh | 40 +++++++++++++++++++++++++++++ helm/matita/scripts/insert.awk | 18 +++++++++++++ helm/matita/scripts/profile_cvs.sh | 41 ++++++++++++++++++++++++++++++ 5 files changed, 122 insertions(+), 4 deletions(-) create mode 100644 helm/matita/scripts/bench.sql create mode 100755 helm/matita/scripts/do_tests.sh create mode 100644 helm/matita/scripts/insert.awk create mode 100755 helm/matita/scripts/profile_cvs.sh 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 + -- 2.39.2