Admin/isatest/isatest-stats
author wenzelm
Wed Oct 08 19:30:15 2008 +0200 (2008-10-08)
changeset 28530 843b35caa8c4
parent 27478 ac3b0f881d89
child 28602 a79582c29bd5
permissions -rwxr-xr-x
added HOL-Main;
     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 at64-poly at-poly-5.1-para-e at64-poly-5.1-para at-mac-poly-5.1-para afp"
    11 
    12 ISABELLE_SESSIONS="\
    13   HOL-Plain \
    14   HOL-Main \
    15   HOL \
    16   HOL-Algebra \
    17   HOL-Auth \
    18   HOL-Bali \
    19   HOL-Complex \
    20   HOL-Complex-ex \
    21   HOL-Extraction \
    22   HOL-Hoare \
    23   HOL-HoareParallel \
    24   HOL-Lambda \
    25   HOL-Library \
    26   HOL-MetisExamples \
    27   HOL-MicroJava \
    28   HOL-NSA \
    29   HOL-Nominal-Examples \
    30   HOL-NumberTheory \
    31   HOL-SET-Protocol \
    32   HOL-UNITY \
    33   HOL-Word \
    34   HOL-ex \
    35   ZF \
    36   ZF-Constructible\
    37   ZF-UNITY"
    38 
    39 AFP_SESSIONS="\
    40   CoreC++\
    41   LinearQuantifierElim\
    42   HOL-DiskPaxos\
    43   HOL-Fermat3_4\
    44   HOL-Flyspeck-Tame\
    45   HOL-Group-Ring-Module\
    46   HOL-JinjaThreads\
    47   HOL-Jinja\
    48   HOL-JiveDataStoreModel\
    49   HOL-POPLmark-deBruijn\
    50   HOL-Program-Conflict-Analysis\
    51   HOL-RSAPSS\
    52   HOL-Recursion-Theory-I\
    53   HOL-SumSquares\
    54   HOL-Topology\
    55   HOL-Valuation\
    56   Simpl-BDD\
    57   Simpl"
    58 
    59 for PLATFORM in $PLATFORMS
    60 do
    61   if [ "$PLATFORM" = afp ]; then
    62     SESSIONS="$AFP_SESSIONS"
    63   else
    64     SESSIONS="$ISABELLE_SESSIONS"
    65   fi
    66 
    67   "$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" ${1:-100} $SESSIONS
    68   cat > "stats/$PLATFORM.html" <<EOF
    69 <!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
    70 <html>
    71 <head><title>Development Snapshot -- Performance Statistics</title></head>
    72 
    73 <body>
    74 <h1>$PLATFORM</h1>
    75 EOF
    76 
    77 for SESSION in $SESSIONS
    78 do
    79   echo "<br><img src="$PLATFORM/$SESSION.png"><br>" >> "stats/$PLATFORM.html"
    80 done
    81 
    82 echo "</body>" >> "stats/$PLATFORM.html"
    83 echo "</html>" >> "stats/$PLATFORM.html"
    84 
    85 done