simple html output;
authorwenzelm
Tue Sep 19 23:01:52 2006 +0200 (2006-09-19)
changeset 206183f763be47c2f
parent 20617 ca59894f70dc
child 20619 02e9b54b18fd
simple html output;
Admin/isatest-stats
     1.1 --- a/Admin/isatest-stats	Tue Sep 19 22:04:38 2006 +0200
     1.2 +++ b/Admin/isatest-stats	Tue Sep 19 23:01:52 2006 +0200
     1.3 @@ -7,23 +7,43 @@
     1.4  
     1.5  THIS=$(cd "$(dirname "$0")"; pwd -P)
     1.6  
     1.7 -for PLATFORM in at-poly at-sml-dev
     1.8 +PLATFORMS="at-poly at-sml-dev"
     1.9 +SESSIONS="\
    1.10 +  HOL \
    1.11 +  HOL-Algebra \
    1.12 +  HOL-Auth \
    1.13 +  HOL-Bali \
    1.14 +  HOL-Complex \
    1.15 +  HOL-Extraction \
    1.16 +  HOL-Hoare \
    1.17 +  HOL-HoareParallel \
    1.18 +  HOL-Lambda \
    1.19 +  HOL-MicroJava \
    1.20 +  HOL-NumberTheory \
    1.21 +  HOL-SET-Protocol \
    1.22 +  HOL-UNITY \
    1.23 +  HOL-ex \
    1.24 +  ZF \
    1.25 +  ZF-Constructible"
    1.26 +
    1.27 +for PLATFORM in $PLATFORMS
    1.28  do
    1.29 -  "$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" 100 \
    1.30 -    HOL \
    1.31 -    HOL-Algebra \
    1.32 -    HOL-Auth \
    1.33 -    HOL-Bali \
    1.34 -    HOL-Complex \
    1.35 -    HOL-Extraction \
    1.36 -    HOL-Hoare \
    1.37 -    HOL-HoareParallel \
    1.38 -    HOL-Lambda \
    1.39 -    HOL-MicroJava \
    1.40 -    HOL-NumberTheory \
    1.41 -    HOL-SET-Protocol \
    1.42 -    HOL-UNITY \
    1.43 -    HOL-ex \
    1.44 -    ZF \
    1.45 -    ZF-Constructible
    1.46 +  "$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" 100 $SESSIONS
    1.47 +  cat > "stats/$PLATFORM.html" <<EOF
    1.48 +<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
    1.49 +<html>
    1.50 +<head><title> Development Snapshot -- Statistics</title></head>
    1.51 +
    1.52 +<body>
    1.53 +<h1>$PLATFORM</h1>
    1.54 +EOF
    1.55 +
    1.56 +for SESSION in $SESSIONS
    1.57 +do
    1.58 +  echo "<br><img src="$PLATFORM/$SESSION.png">" >> "stats/$PLATFORM.html"
    1.59  done
    1.60 +
    1.61 +echo "</body>" >> "stats/$PLATFORM.html"
    1.62 +echo "</html>" >> "stats/$PLATFORM.html"
    1.63 +
    1.64 +done