Admin/isatest-stats
author haftmann
Fri, 20 Oct 2006 17:07:27 +0200
changeset 21079 747d716e98d0
parent 20683 3d07617c8bf3
child 21166 2075d9027004
permissions -rwxr-xr-x
added reserved words for Haskell

#!/usr/bin/env bash
#
# $Id$
# Author: Makarius
#
# DESCRIPTION: Standard statistics.

THIS=$(cd "$(dirname "$0")"; pwd -P)

PLATFORMS="at-poly at-sml-dev"
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" 100 $SESSIONS
  cat > "stats/$PLATFORM.html" <<EOF
<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
<html>
<head><title>Development Snapshot -- Performance Statistics</title></head>

<body>
<h1>$PLATFORM</h1>
EOF

for SESSION in $SESSIONS
do
  echo "<br><img src="$PLATFORM/$SESSION.png"><br>" >> "stats/$PLATFORM.html"
done

echo "</body>" >> "stats/$PLATFORM.html"
echo "</html>" >> "stats/$PLATFORM.html"

done