Admin/isatest-stats
author wenzelm
Tue Sep 19 23:12:21 2006 +0200 (2006-09-19)
changeset 20619 02e9b54b18fd
parent 20618 3f763be47c2f
child 20632 40abbc7c86df
permissions -rwxr-xr-x
tuned;
     1 #!/usr/bin/env bash
     2 #
     3 # $Id$
     4 # Author: Makarius
     5 #
     6 # DESCRIPTION: Standard statistics.
     7 
     8 THIS=$(cd "$(dirname "$0")"; pwd -P)
     9 
    10 PLATFORMS="at-poly at-sml-dev"
    11 SESSIONS="\
    12   HOL \
    13   HOL-Algebra \
    14   HOL-Auth \
    15   HOL-Bali \
    16   HOL-Complex \
    17   HOL-Extraction \
    18   HOL-Hoare \
    19   HOL-HoareParallel \
    20   HOL-Lambda \
    21   HOL-MicroJava \
    22   HOL-NumberTheory \
    23   HOL-SET-Protocol \
    24   HOL-UNITY \
    25   HOL-ex \
    26   ZF \
    27   ZF-Constructible"
    28 
    29 for PLATFORM in $PLATFORMS
    30 do
    31   "$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" 100 $SESSIONS
    32   cat > "stats/$PLATFORM.html" <<EOF
    33 <!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
    34 <html>
    35 <head><title> Development Snapshot -- Statistics</title></head>
    36 
    37 <body>
    38 <h1>$PLATFORM</h1>
    39 EOF
    40 
    41 for SESSION in $SESSIONS
    42 do
    43   echo "<br><img src="$PLATFORM/$SESSION.png"><br>" >> "stats/$PLATFORM.html"
    44 done
    45 
    46 echo "</body>" >> "stats/$PLATFORM.html"
    47 echo "</html>" >> "stats/$PLATFORM.html"
    48 
    49 done