diff -r 5f7c9c82b05e -r da313b67a04d Admin/isatest/isatest-stats --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/isatest/isatest-stats Mon Mar 05 22:12:20 2007 +0100 @@ -0,0 +1,51 @@ +#!/usr/bin/env bash +# +# $Id$ +# Author: Makarius +# +# DESCRIPTION: Standard statistics. + +THIS=$(cd "$(dirname "$0")"; pwd -P) + +PLATFORMS="at-poly at-sml-dev at-mac-poly-e at64-poly-e" +SESSIONS="\ + HOL \ + HOL-Algebra \ + HOL-Auth \ + HOL-Bali \ + HOL-Complex \ + HOL-Complex-ex \ + HOL-Extraction \ + HOL-Hoare \ + HOL-HoareParallel \ + HOL-Lambda \ + HOL-MicroJava \ + HOL-NumberTheory \ + HOL-SET-Protocol \ + HOL-UNITY \ + HOL-ex \ + ZF \ + ZF-Constructible\ + ZF-UNITY" + +for PLATFORM in $PLATFORMS +do + "$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" ${1:-100} $SESSIONS + cat > "stats/$PLATFORM.html" < + +Development Snapshot -- Performance Statistics + + +

$PLATFORM

+EOF + +for SESSION in $SESSIONS +do + echo "

" >> "stats/$PLATFORM.html" +done + +echo "" >> "stats/$PLATFORM.html" +echo "" >> "stats/$PLATFORM.html" + +done