--- a/Admin/annomaly Mon Mar 05 10:14:32 2007 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,70 +0,0 @@
-#!/bin/sh
-
-# Create AnnoMaLy documentation for Isabelle
-# See http://martin.von-gagern.net/projects/annomaly/
-# 2007 Martin von Gagern (martin@von-gagern.net)
-
-# Abort on any error
-set -e -o pipefail
-
-ISABELLE_CVS="$(cd "$HOME/isabelle.cvs"; pwd -P)"
-ISABELLE_HOME="$ISABELLE_CVS/Distribution"
-HTML_DIR="$HOME/html-data/isabelle-doc"
-export CVS_RSH=ssh
-export SMLNJ_HOME="$HOME/annomaly"
-export PATH="$SMLNJ_HOME/bin:$PATH"
-export SML_DOC_DIR="$HTML_DIR.tmp"
-export SML_DOC_REWRITE="isabelle=$ISABELLE_CVS"
-# export SML_DOC_DEBUG="all"
-TARGET=HOL
-CVSUP=true
-
-# Parse command line
-for ARG in "$@"; do case "$ARG" in
- -p) TARGET=Pure ;;
- -n) CVSUP=false ;;
- -l) export SML_LOG_DIR="$HOME/logs" ;;
-esac; done
-
-# Create clean output directory
-rm -rf "$SML_DOC_DIR"
-mkdir "$SML_DOC_DIR"
-cp "$SMLNJ_HOME/annomaly/resources/"* "$SML_DOC_DIR"
-cat > "$SML_DOC_DIR/.htaccess" <<EOF
-DirectoryIndex index.html source.html
-<IfModule mod_deflate>
-SetOutputFilter DEFLATE
-</IfModule>
-AddType text/plain .dot
-EOF
-
-# Update CVS
-cd "$ISABELLE_CVS"
-if $CVSUP; then
- echo "Updating CVS"
- cvs -q up -d
-fi
-
-# Build isabelle
-cd "$ISABELLE_HOME"
-rm -rf heaps/*
-./build -b $TARGET
-
-# Postprocess created files
-cd $SML_DOC_DIR
-dot -Tsvg depGraph.dot \
- | perl -pe 's/(width|height)="(\d+)/sprintf("%s=\"%.2f",$1,$2*0.6)/ge' \
- > depGraph.svg
-dot -Tps2 depGraph.dot > depGraph.ps
-ps2pdf depGraph.ps depGraph.pdf
-grep -rl "$ISABELLE_HOME" . | xargs sed -i "s@$ISABELLE_HOME@\$ISABELLE_HOME@g"
-
-# Install result by renaming to be almost atomic
-rm -rf "$HTML_DIR.bac"
-if [[ -d $HTML_DIR ]]; then mv "$HTML_DIR" "$HTML_DIR.bac"; fi
-mv "$SML_DOC_DIR" "$HTML_DIR"
-rm -rf "$HTML_DIR.bac"
-
-# Done
-echo "Completed successfully"
-exit 0
--- a/Admin/isatest-check Mon Mar 05 10:14:32 2007 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,105 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-# Author: Gerwin Klein, TU Muenchen
-#
-# DESCRIPTION: sends email for failed tests, checks for error.log,
-# generates development snapshot if test ok
-
-## global settings
-. ~/admin/isatest-settings
-
-# produce empty list for patterns like isatest-*.log if no
-# such file exists
-shopt -s nullglob
-
-# mail program
-MAIL=$HOME/bin/pmail
-
-# tmp file for sending mail
-TMP=/tmp/isatest-makedist.$$
-
-export DISTPREFIX
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: $PRG"
- echo
- echo " sends email for failed tests, checks for error.log,"
- echo " generates development snapshot if test ok."
- echo " To be called by cron."
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-## main
-
-# check if tests are still running, wait for them a couple of hours
-i=0
-while [ -n "$(ls $RUNNING)" -a $i -lt 8 ]; do
- sleep 3600
- let "i = i+1"
-done
-
-FAIL=0
-
-# still running -> give up
-if [ -n "$(ls $RUNNING)" ]; then
- echo "Giving up waiting for test to finish at $(date)." > $TMP
- echo >> $TMP
- echo "Sessions still running:" >> $TMP
- echo "$(ls $RUNNING)" >> $TMP
- echo >> $TMP
- echo "Attaching all error logs collected so far." >> $TMP
- echo >> $TMP
-
- if [ -e $ERRORLOG ]; then
- cat $ERRORLOG >> $TMP
- fi
-
- echo "Have a nice day," >> $TMP
- echo " isatest" >> $TMP
-
- for R in $MAILTO; do
- LOGS=$ERRORDIR/isatest*.log
- $MAIL "isabelle test taking too long" $R $TMP $LOGS
- done
-
- rm $TMP
-
- FAIL=1
-elif [ -e $ERRORLOG ]; then
- # no tests running, check if there were errors
- cat $ERRORLOG > $TMP
- echo "Have a nice day," >> $TMP
- echo " isatest" >> $TMP
-
- for R in $MAILTO; do
- LOGS=$ERRORDIR/isatest*.log
- $MAIL "isabelle test failed" $R $TMP $LOGS
- done
-
- rm $TMP
-fi
-
-# generate development snapshot page only for successful tests
-# (failures in experimental sessions ok)
-if [ "$FAIL"=="0" -a "$(echo $ERRORDIR/isatest*[^e].log)" == "$(echo)" ]; then
- (cd $HOME/devel-page; env DISTNAME=`$DISTPREFIX/Isabelle/bin/isatool version` make)
- echo "$(date) $HOSTNAME $PRG: generated development snapshot web page." >> $MASTERLOG
-fi
-
-exit 0
-## end
--- a/Admin/isatest-doc Mon Mar 05 10:14:32 2007 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,127 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-# Author: Gerwin Klein, NICTA
-#
-# Run IsaMakefile for every Doc/ subdirectory.
-#
-# Relies on being run in the isatest environment on sunbroy2.
-#
-
-. ~/.bashrc
-
-## global settings
-. ~/admin/isatest-settings
-
-DOCDIR=$HOME/Doc
-
-MAXTIME=1800
-
-ISABELLE_DEVEL=$DISTPREFIX/Isabelle
-DATE=$(date "+%Y-%m-%d")
-
-LOG=$LOGPREFIX/isatest-doc-$DATE.log
-
-SHORT=sun-poly
-SETTINGS=~/settings/$SHORT
-
-ISATOOL=$ISABELLE_DEVEL/bin/isatool
-
-
-MAIL=~/afp/release/admin/mail-attach
-
-TMP=/tmp/isatest-doc.mail.tmp
-while [ -e $TMP ]; do TMP=$TMP.x; done
-
-#
-PRG="$(basename "$0")"
-
-## functions
-
-function usage()
-{
- echo
- echo "Usage: $PRG"
- echo
- echo " Run IsaMakefile for every Doc/ subdirectory"
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-##
-
-[ "$#" != "0" ] && usage
-
-if [ -f "$RUNNING/$SHORT.running" -o -e $ERRORLOG ]; then
- echo "$(date) $HOSTNAME $PRG: Skipped test. Isabelle devel version broken." >> $MASTERLOG
- exit 1
-fi
-cat $SETTINGS >> $ISABELLE_DEVEL/etc/settings
-
-
-echo "Start test at `date`" > $LOG
-echo >> $LOG
-echo "begin cvs update" >> $LOG
-
-# cvs update to newest version
-cd $DOCDIR || fail "could not cd to $DOCDIR"
-cvs -q up -A -P -d >> $LOG 2>&1 || fail "could not CVS update."
-
-echo "end cvs update" >> $LOG
-echo >> $LOG
-
-# run test
-FAIL="";
-
-cd $DOCDIR
-for DIR in */; do
- if [ -f "$DIR/IsaMakefile" ]; then
- echo "Testing [$DIR]" >> $LOG
- (
- cd $DIR
- ulimit -t $MAXTIME
- nice $ISATOOL make >> $LOG 2>&1
- ) || FAIL="${FAIL}${DIR} "
- echo "Finished [$DIR]" >> $LOG
- echo >> $LOG
- fi
-done
-
-ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
-
-echo >> $LOG
-echo "End test on `date`, elapsed time: $ELAPSED" >> $LOG
-
-# send email if there was a problem
-if [ "$FAIL" != "" ]; then
- echo >> $LOG
- echo "Failed sessions: ${FAIL}" >> $LOG
-
- echo "$(date) $HOSTNAME $PRG: doc test FAILED for ${FAIL}, elapsed time $ELAPSED." >> $MASTERLOG
-
- cat > $TMP <<EOF
-Session(s) ${FAIL} in the documentation test failed (log attached).
-Test ended on: $HOSTNAME, `date`.
-
-Have a nice day,
- isatest
-
-EOF
-
- for R in $MAILTO; do
- $MAIL 'doc test failed' "$R" $TMP $LOG
- done
-
- rm -f $TMP
-
- exit 1
-else
- echo "$(date) $HOSTNAME $PRG: doc test successful, elapsed time $ELAPSED." >> $MASTERLOG
-fi
-
--- a/Admin/isatest-lint Mon Mar 05 10:14:32 2007 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-#!/usr/bin/env perl
-#
-# $Id$
-# Author: Florian Haftmann, TUM
-#
-# Do consistency and quality checks on the isabelle sources
-#
-
-use strict;
-use File::Find;
-use File::Basename;
-
-# configuration
-my $isabelleRoot = $ENV{'HOME'} . "/isabelle";
-my @suffices = ('\.thy', '\.ml', '\.ML');
-
-# lint main procedure
-sub lint() {
- my ($basename, $dirname, $ext) = fileparse($File::Find::name, @suffices);
- if ($ext) {
- open ISTREAM, $File::Find::name or die("error opening $File::Find::name");
- my $found = 0;
- while (<ISTREAM>) {
- $found ||= m/\$Id[^\$]*\$/;
- last if $found;
- }
- close ISTREAM;
- my $relname = substr($File::Find::name, (length $isabelleRoot) + 1);
- if (! $found) {
- print "Found no CVS id in $relname\n";
- }
- }
-}
-
-# first argument =^= isabelle repository root
-if (@ARGV) {
- $isabelleRoot = $ARGV[0];
-}
-
-find(\&lint, $isabelleRoot);
-
--- a/Admin/isatest-makeall Mon Mar 05 10:14:32 2007 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,134 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-# Author: Gerwin Klein, TU Muenchen
-#
-# DESCRIPTION: Run isatool makeall from specified distribution and settings.
-
-## global settings
-. ~/admin/isatest-settings
-
-# max time until test is aborted (in sec)
-MAXTIME=28800
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: $PRG settings1 [settings2 ...]"
- echo
- echo " Runs isatool makeall for specified settings."
- echo " Leaves messages in ${ERRORLOG} and ${LOGPREFIX} if it fails."
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- echo "$(date) $HOSTNAME $PRG: FAILED, $1" >> $MASTERLOG
- exit 2
-}
-
-## main
-
-# argument checking
-
-[ "$1" = "-?" ] && usage
-[ "$#" -lt "1" ] && usage
-
-[ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
-
-# make file flags and nice setup for different target platforms
-case $HOSTNAME in
- atbroy51)
- # 2 processors
- MFLAGS="-j 2"
- # MFLAGS=""
- NICE=""
- ;;
-
- atbroy31)
- # cluster
- MFLAGS="-j 5"
- ;;
-
- sunbroy2)
- MFLAGS="-j 6"
- NICE="nice"
- ;;
-
- sunbroy1)
- MFLAGS="-j 2"
- NICE="nice"
- ;;
-
- macbroy5)
- MFLAGS="" # -j 2 does not work on poly/macos 10.4.1
- NICE=""
- ;;
-
- *)
- MFLAGS=""
- # be nice by default
- NICE=nice
- ;;
-esac
-
-# main test loop
-
-for SETTINGS in $@; do
-
- [ -r $SETTINGS ] || fail "Cannot read $SETTINGS."
-
- # logfile setup
-
- DATE=$(date "+%Y-%m-%d")
- SHORT=${SETTINGS##*/}
- TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log
-
- # the test
-
- touch $RUNNING/$SHORT.running
-
- echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
-
- cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
- (ulimit -t $MAXTIME; $NICE $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1)
-
- if [ $? -eq 0 ]
- then
- # test log and cleanup
- echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
- gzip -f $TESTLOG
- else
- # test log
- echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
-
- # error log
- echo "Test for platform ${SHORT} failed. Log file attached." >> $ERRORLOG
- echo "[...]" >> $ERRORLOG
- tail -3 $TESTLOG >> $ERRORLOG
- echo >> $ERRORLOG
-
- FAIL="$FAIL$SHORT "
- (cd $ERRORDIR; ln -s $TESTLOG)
- fi
-
- rm -f $RUNNING/$SHORT.running
-done
-
-# time and success/failure to master log
-ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
-
-if [ -z "$FAIL" ]; then
- echo "$(date) $HOSTNAME $PRG: all tests successful, elapsed time $ELAPSED." >> $MASTERLOG
-else
- echo "$(date) $HOSTNAME $PRG: targets ${FAIL}FAILED, elapsed time $ELAPSED." >> $MASTERLOG
- exit 1
-fi
-
-# end
--- a/Admin/isatest-makedist Mon Mar 05 10:14:32 2007 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,112 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-# Author: Gerwin Klein, TU Muenchen
-#
-# DESCRIPTION: Build distribution and run isatest-make for lots of platforms.
-
-## global settings
-. ~/admin/isatest-settings
-
-TMP=/tmp/isatest-makedist.$$
-MAIL=$HOME/bin/pmail
-
-MAKEDIST=$HOME/bin/makedist
-MAKEALL=$HOME/bin/isatest-makeall
-TAR=gtar
-CVS2CL="$HOME/bin/cvs2cl --follow-only TRUNK"
-
-SSH="ssh -f"
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: $PRG"
- echo
- echo " Build distribution and run isatest-make for lots of platforms."
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-## main
-
-# cleanup old error log and test-still-running files
-rm -f $ERRORLOG
-rm -f $ERRORDIR/isatest-*.log
-rm -f $RUNNING/*.runnning
-
-export DISTPREFIX
-export CVS2CL
-
-DATE=$(date "+%Y-%m-%d")
-DISTLOG=$LOGPREFIX/isatest-makedist-$DATE.log
-
-echo ------------------- preparing test release --- `date` --- $HOSTNAME > $DISTLOG 2>&1
-
-echo "### cleaning up old dist directory" >> $DISTLOG 2>&1
-rm -rf $DISTPREFIX >> $DISTLOG 2>&1
-
-echo "### cleaning up old isabelle-* directories" >> $DISTLOG 2>&1
-rm -rf $HOME/isabelle-*
-
-echo "### building distribution" >> $DISTLOG 2>&1
-mkdir -p $DISTPREFIX
-$MAKEDIST - >> $DISTLOG 2>&1
-
-if [ $? -ne 0 ]
-then
- echo ------------------- DIST BUILD FAILED --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
- ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
- echo "$(date) $HOSTNAME $PRG: dist build FAILED, elapsed time $ELAPSED." >> $MASTERLOG
-
- echo "Could not build isabelle distribution. Log file available at" > $TMP
- echo "$HOSTNAME:$DISTLOG" >> $TMP
-
- for R in $MAILTO; do
- $MAIL "isabelle dist build failed" $R $TMP
- done
-
- rm $TMP
-
- exit 1
-fi
-
-cd $DISTPREFIX >> $DISTLOG 2>&1
-$TAR xvzf `cat $DISTPREFIX/ISABELLE_DIST` >> $DISTLOG 2>&1
-
-echo ------------------- prepared test successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
-
-ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
-echo "$(date) $HOSTNAME $PRG: dist build successful, elapsed time $ELAPSED." >> $MASTERLOG
-
-
-## spawn test runs
-
-$SSH sunbroy2 "$MAKEALL $HOME/settings/sun-poly"
-# give test some time to copy settings and start
-sleep 5
-$SSH atbroy51 "$MAKEALL $HOME/settings/at-poly $HOME/settings/at-poly-e"
-sleep 5
-$SSH atbroy10 "$MAKEALL $HOME/settings/at-sml-dev"
-sleep 5
-$SSH atbroy101 "$MAKEALL $HOME/settings/at64-poly-e"
-sleep 5
-$SSH macbroy5 "$MAKEALL $HOME/settings/mac-poly $HOME/settings/mac-sml-dev"
-sleep 5
-$SSH macbroy6 "/usr/stud/isatest/bin/isatest-makeall $HOME/settings/at-mac-poly-e"
-
-echo ------------------- spawned tests successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
-
-gzip -f $DISTLOG
-
-## end
--- a/Admin/isatest-settings Mon Mar 05 10:14:32 2007 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-# -*- shell-script -*-
-# $Id$
-# Author: Gerwin Klein, NICTA
-#
-# DESCRIPTION: common settings for the isatest-* scripts
-
-# source bashrc, we're called by cron
-. ~/.bashrc
-
-# canoncical home for all platforms
-HOME=/home/isatest
-
-## send email on failure to
-MAILTO="kleing@cse.unsw.edu.au nipkow@in.tum.de berghofe@in.tum.de schirmer@in.tum.de lp15@cam.ac.uk makarius@sketis.net haftmann@in.tum.de"
-
-LOGPREFIX=$HOME/log
-MASTERLOG=$LOGPREFIX/isatest.log
-
-ERRORDIR=$HOME/var
-ERRORLOG=$ERRORDIR/error.log
-
-RUNNING=$HOME/var/running
-
-DISTPREFIX=$HOME/tmp/isadist
--- a/Admin/isatest-statistics Mon Mar 05 10:14:32 2007 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,91 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-# Author: Makarius
-#
-# DESCRIPTION: Produce statistics from isatest session logs.
-
-ISATEST_LOG=~isatest/log
-
-## platform settings
-
-case $(uname) in
- SunOS)
- ZGREP=xgrep
- TE="png color"
- ;;
- *)
- ZGREP=zgrep
- TE="png"
- ;;
-esac
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: $PRG DIR PLATFORM TIMESPAN SESSIONS..."
- echo
- echo " Produce statistics from isatest session logs, looking TIMESPAN"
- echo " days into the past. Outputs .png files into DIR."
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-
-## arguments
-
-[ "$1" = "-?" ] && usage
-[ "$#" -lt "4" ] && usage
-
-DIR="$1"; shift
-PLATFORM="$1"; shift
-TIMESPAN="$1"; shift
-SESSIONS="$@"
-
-
-## main
-
-ALL_DATA="/tmp/isatest-all$$.dat"
-SESSION_DATA="/tmp/isatest$$.dat"
-mkdir -p "$DIR" || fail "Bad directory: $DIR"
-
-$ZGREP "^Finished .*elapsed" \
- $(find "$ISATEST_LOG" -name "isatest-makeall-${PLATFORM}*" -ctime "-${TIMESPAN}") | \
-perl -e '
- while (<>) {
- if (m/isatest-makeall-.*-(\d+)-(\d+)-(\d+)-.*:Finished (\S+) \(.*, (\d+):(\d+):(\d+) cpu time\)/) {
- my $year = $1;
- my $month = $2;
- my $day = $3;
- my $name = $4;
- my $time = ($5 * 3600 + $6 * 60 + $7) / 60;
-
- printf "$name $year-$month-$day %.2f\n", $time;
- }
- }' > "$ALL_DATA"
-
-for SESSION in $SESSIONS
-do
- fgrep "$SESSION " "$ALL_DATA" > "$SESSION_DATA"
- gnuplot <<EOF
-set terminal $TE
-set output "$DIR/${SESSION}.png"
-set xdata time
-set timefmt "%Y-%m-%d"
-set format x "%d-%b"
-set xlabel "$SESSION"
-plot [] [0:] "$SESSION_DATA" using 2:3 smooth sbezier notitle, "$SESSION_DATA" using 2:3 smooth csplines notitle
-EOF
-done
-
-rm -f "$ALL_DATA" "$SESSION_DATA"
--- a/Admin/isatest-stats Mon Mar 05 10:14:32 2007 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,51 +0,0 @@
-#!/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" <<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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/isatest/annomaly Mon Mar 05 22:12:20 2007 +0100
@@ -0,0 +1,70 @@
+#!/bin/sh
+
+# Create AnnoMaLy documentation for Isabelle
+# See http://martin.von-gagern.net/projects/annomaly/
+# 2007 Martin von Gagern (martin@von-gagern.net)
+
+# Abort on any error
+set -e -o pipefail
+
+ISABELLE_CVS="$(cd "$HOME/isabelle.cvs"; pwd -P)"
+ISABELLE_HOME="$ISABELLE_CVS/Distribution"
+HTML_DIR="$HOME/html-data/isabelle-doc"
+export CVS_RSH=ssh
+export SMLNJ_HOME="$HOME/annomaly"
+export PATH="$SMLNJ_HOME/bin:$PATH"
+export SML_DOC_DIR="$HTML_DIR.tmp"
+export SML_DOC_REWRITE="isabelle=$ISABELLE_CVS"
+# export SML_DOC_DEBUG="all"
+TARGET=HOL
+CVSUP=true
+
+# Parse command line
+for ARG in "$@"; do case "$ARG" in
+ -p) TARGET=Pure ;;
+ -n) CVSUP=false ;;
+ -l) export SML_LOG_DIR="$HOME/logs" ;;
+esac; done
+
+# Create clean output directory
+rm -rf "$SML_DOC_DIR"
+mkdir "$SML_DOC_DIR"
+cp "$SMLNJ_HOME/annomaly/resources/"* "$SML_DOC_DIR"
+cat > "$SML_DOC_DIR/.htaccess" <<EOF
+DirectoryIndex index.html source.html
+<IfModule mod_deflate>
+SetOutputFilter DEFLATE
+</IfModule>
+AddType text/plain .dot
+EOF
+
+# Update CVS
+cd "$ISABELLE_CVS"
+if $CVSUP; then
+ echo "Updating CVS"
+ cvs -q up -d
+fi
+
+# Build isabelle
+cd "$ISABELLE_HOME"
+rm -rf heaps/*
+./build -b $TARGET
+
+# Postprocess created files
+cd $SML_DOC_DIR
+dot -Tsvg depGraph.dot \
+ | perl -pe 's/(width|height)="(\d+)/sprintf("%s=\"%.2f",$1,$2*0.6)/ge' \
+ > depGraph.svg
+dot -Tps2 depGraph.dot > depGraph.ps
+ps2pdf depGraph.ps depGraph.pdf
+grep -rl "$ISABELLE_HOME" . | xargs sed -i "s@$ISABELLE_HOME@\$ISABELLE_HOME@g"
+
+# Install result by renaming to be almost atomic
+rm -rf "$HTML_DIR.bac"
+if [[ -d $HTML_DIR ]]; then mv "$HTML_DIR" "$HTML_DIR.bac"; fi
+mv "$SML_DOC_DIR" "$HTML_DIR"
+rm -rf "$HTML_DIR.bac"
+
+# Done
+echo "Completed successfully"
+exit 0
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/isatest/isatest-check Mon Mar 05 22:12:20 2007 +0100
@@ -0,0 +1,105 @@
+#!/usr/bin/env bash
+#
+# $Id$
+# Author: Gerwin Klein, TU Muenchen
+#
+# DESCRIPTION: sends email for failed tests, checks for error.log,
+# generates development snapshot if test ok
+
+## global settings
+. ~/admin/isatest-settings
+
+# produce empty list for patterns like isatest-*.log if no
+# such file exists
+shopt -s nullglob
+
+# mail program
+MAIL=$HOME/bin/pmail
+
+# tmp file for sending mail
+TMP=/tmp/isatest-makedist.$$
+
+export DISTPREFIX
+
+
+## diagnostics
+
+PRG="$(basename "$0")"
+
+function usage()
+{
+ echo
+ echo "Usage: $PRG"
+ echo
+ echo " sends email for failed tests, checks for error.log,"
+ echo " generates development snapshot if test ok."
+ echo " To be called by cron."
+ echo
+ exit 1
+}
+
+function fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
+## main
+
+# check if tests are still running, wait for them a couple of hours
+i=0
+while [ -n "$(ls $RUNNING)" -a $i -lt 8 ]; do
+ sleep 3600
+ let "i = i+1"
+done
+
+FAIL=0
+
+# still running -> give up
+if [ -n "$(ls $RUNNING)" ]; then
+ echo "Giving up waiting for test to finish at $(date)." > $TMP
+ echo >> $TMP
+ echo "Sessions still running:" >> $TMP
+ echo "$(ls $RUNNING)" >> $TMP
+ echo >> $TMP
+ echo "Attaching all error logs collected so far." >> $TMP
+ echo >> $TMP
+
+ if [ -e $ERRORLOG ]; then
+ cat $ERRORLOG >> $TMP
+ fi
+
+ echo "Have a nice day," >> $TMP
+ echo " isatest" >> $TMP
+
+ for R in $MAILTO; do
+ LOGS=$ERRORDIR/isatest*.log
+ $MAIL "isabelle test taking too long" $R $TMP $LOGS
+ done
+
+ rm $TMP
+
+ FAIL=1
+elif [ -e $ERRORLOG ]; then
+ # no tests running, check if there were errors
+ cat $ERRORLOG > $TMP
+ echo "Have a nice day," >> $TMP
+ echo " isatest" >> $TMP
+
+ for R in $MAILTO; do
+ LOGS=$ERRORDIR/isatest*.log
+ $MAIL "isabelle test failed" $R $TMP $LOGS
+ done
+
+ rm $TMP
+fi
+
+# generate development snapshot page only for successful tests
+# (failures in experimental sessions ok)
+if [ "$FAIL"=="0" -a "$(echo $ERRORDIR/isatest*[^e].log)" == "$(echo)" ]; then
+ (cd $HOME/devel-page; env DISTNAME=`$DISTPREFIX/Isabelle/bin/isatool version` make)
+ echo "$(date) $HOSTNAME $PRG: generated development snapshot web page." >> $MASTERLOG
+fi
+
+exit 0
+## end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/isatest/isatest-doc Mon Mar 05 22:12:20 2007 +0100
@@ -0,0 +1,127 @@
+#!/usr/bin/env bash
+#
+# $Id$
+# Author: Gerwin Klein, NICTA
+#
+# Run IsaMakefile for every Doc/ subdirectory.
+#
+# Relies on being run in the isatest environment on sunbroy2.
+#
+
+. ~/.bashrc
+
+## global settings
+. ~/admin/isatest-settings
+
+DOCDIR=$HOME/Doc
+
+MAXTIME=1800
+
+ISABELLE_DEVEL=$DISTPREFIX/Isabelle
+DATE=$(date "+%Y-%m-%d")
+
+LOG=$LOGPREFIX/isatest-doc-$DATE.log
+
+SHORT=sun-poly
+SETTINGS=~/settings/$SHORT
+
+ISATOOL=$ISABELLE_DEVEL/bin/isatool
+
+
+MAIL=~/afp/release/admin/mail-attach
+
+TMP=/tmp/isatest-doc.mail.tmp
+while [ -e $TMP ]; do TMP=$TMP.x; done
+
+#
+PRG="$(basename "$0")"
+
+## functions
+
+function usage()
+{
+ echo
+ echo "Usage: $PRG"
+ echo
+ echo " Run IsaMakefile for every Doc/ subdirectory"
+ echo
+ exit 1
+}
+
+function fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
+##
+
+[ "$#" != "0" ] && usage
+
+if [ -f "$RUNNING/$SHORT.running" -o -e $ERRORLOG ]; then
+ echo "$(date) $HOSTNAME $PRG: Skipped test. Isabelle devel version broken." >> $MASTERLOG
+ exit 1
+fi
+cat $SETTINGS >> $ISABELLE_DEVEL/etc/settings
+
+
+echo "Start test at `date`" > $LOG
+echo >> $LOG
+echo "begin cvs update" >> $LOG
+
+# cvs update to newest version
+cd $DOCDIR || fail "could not cd to $DOCDIR"
+cvs -q up -A -P -d >> $LOG 2>&1 || fail "could not CVS update."
+
+echo "end cvs update" >> $LOG
+echo >> $LOG
+
+# run test
+FAIL="";
+
+cd $DOCDIR
+for DIR in */; do
+ if [ -f "$DIR/IsaMakefile" ]; then
+ echo "Testing [$DIR]" >> $LOG
+ (
+ cd $DIR
+ ulimit -t $MAXTIME
+ nice $ISATOOL make >> $LOG 2>&1
+ ) || FAIL="${FAIL}${DIR} "
+ echo "Finished [$DIR]" >> $LOG
+ echo >> $LOG
+ fi
+done
+
+ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
+
+echo >> $LOG
+echo "End test on `date`, elapsed time: $ELAPSED" >> $LOG
+
+# send email if there was a problem
+if [ "$FAIL" != "" ]; then
+ echo >> $LOG
+ echo "Failed sessions: ${FAIL}" >> $LOG
+
+ echo "$(date) $HOSTNAME $PRG: doc test FAILED for ${FAIL}, elapsed time $ELAPSED." >> $MASTERLOG
+
+ cat > $TMP <<EOF
+Session(s) ${FAIL} in the documentation test failed (log attached).
+Test ended on: $HOSTNAME, `date`.
+
+Have a nice day,
+ isatest
+
+EOF
+
+ for R in $MAILTO; do
+ $MAIL 'doc test failed' "$R" $TMP $LOG
+ done
+
+ rm -f $TMP
+
+ exit 1
+else
+ echo "$(date) $HOSTNAME $PRG: doc test successful, elapsed time $ELAPSED." >> $MASTERLOG
+fi
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/isatest/isatest-lint Mon Mar 05 22:12:20 2007 +0100
@@ -0,0 +1,41 @@
+#!/usr/bin/env perl
+#
+# $Id$
+# Author: Florian Haftmann, TUM
+#
+# Do consistency and quality checks on the isabelle sources
+#
+
+use strict;
+use File::Find;
+use File::Basename;
+
+# configuration
+my $isabelleRoot = $ENV{'HOME'} . "/isabelle";
+my @suffices = ('\.thy', '\.ml', '\.ML');
+
+# lint main procedure
+sub lint() {
+ my ($basename, $dirname, $ext) = fileparse($File::Find::name, @suffices);
+ if ($ext) {
+ open ISTREAM, $File::Find::name or die("error opening $File::Find::name");
+ my $found = 0;
+ while (<ISTREAM>) {
+ $found ||= m/\$Id[^\$]*\$/;
+ last if $found;
+ }
+ close ISTREAM;
+ my $relname = substr($File::Find::name, (length $isabelleRoot) + 1);
+ if (! $found) {
+ print "Found no CVS id in $relname\n";
+ }
+ }
+}
+
+# first argument =^= isabelle repository root
+if (@ARGV) {
+ $isabelleRoot = $ARGV[0];
+}
+
+find(\&lint, $isabelleRoot);
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/isatest/isatest-makeall Mon Mar 05 22:12:20 2007 +0100
@@ -0,0 +1,134 @@
+#!/usr/bin/env bash
+#
+# $Id$
+# Author: Gerwin Klein, TU Muenchen
+#
+# DESCRIPTION: Run isatool makeall from specified distribution and settings.
+
+## global settings
+. ~/admin/isatest-settings
+
+# max time until test is aborted (in sec)
+MAXTIME=28800
+
+## diagnostics
+
+PRG="$(basename "$0")"
+
+function usage()
+{
+ echo
+ echo "Usage: $PRG settings1 [settings2 ...]"
+ echo
+ echo " Runs isatool makeall for specified settings."
+ echo " Leaves messages in ${ERRORLOG} and ${LOGPREFIX} if it fails."
+ echo
+ exit 1
+}
+
+function fail()
+{
+ echo "$1" >&2
+ echo "$(date) $HOSTNAME $PRG: FAILED, $1" >> $MASTERLOG
+ exit 2
+}
+
+## main
+
+# argument checking
+
+[ "$1" = "-?" ] && usage
+[ "$#" -lt "1" ] && usage
+
+[ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
+
+# make file flags and nice setup for different target platforms
+case $HOSTNAME in
+ atbroy51)
+ # 2 processors
+ MFLAGS="-j 2"
+ # MFLAGS=""
+ NICE=""
+ ;;
+
+ atbroy31)
+ # cluster
+ MFLAGS="-j 5"
+ ;;
+
+ sunbroy2)
+ MFLAGS="-j 6"
+ NICE="nice"
+ ;;
+
+ sunbroy1)
+ MFLAGS="-j 2"
+ NICE="nice"
+ ;;
+
+ macbroy5)
+ MFLAGS="" # -j 2 does not work on poly/macos 10.4.1
+ NICE=""
+ ;;
+
+ *)
+ MFLAGS=""
+ # be nice by default
+ NICE=nice
+ ;;
+esac
+
+# main test loop
+
+for SETTINGS in $@; do
+
+ [ -r $SETTINGS ] || fail "Cannot read $SETTINGS."
+
+ # logfile setup
+
+ DATE=$(date "+%Y-%m-%d")
+ SHORT=${SETTINGS##*/}
+ TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log
+
+ # the test
+
+ touch $RUNNING/$SHORT.running
+
+ echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
+
+ cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
+ (ulimit -t $MAXTIME; $NICE $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1)
+
+ if [ $? -eq 0 ]
+ then
+ # test log and cleanup
+ echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
+ gzip -f $TESTLOG
+ else
+ # test log
+ echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
+
+ # error log
+ echo "Test for platform ${SHORT} failed. Log file attached." >> $ERRORLOG
+ echo "[...]" >> $ERRORLOG
+ tail -3 $TESTLOG >> $ERRORLOG
+ echo >> $ERRORLOG
+
+ FAIL="$FAIL$SHORT "
+ (cd $ERRORDIR; ln -s $TESTLOG)
+ fi
+
+ rm -f $RUNNING/$SHORT.running
+done
+
+# time and success/failure to master log
+ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
+
+if [ -z "$FAIL" ]; then
+ echo "$(date) $HOSTNAME $PRG: all tests successful, elapsed time $ELAPSED." >> $MASTERLOG
+else
+ echo "$(date) $HOSTNAME $PRG: targets ${FAIL}FAILED, elapsed time $ELAPSED." >> $MASTERLOG
+ exit 1
+fi
+
+# end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/isatest/isatest-makedist Mon Mar 05 22:12:20 2007 +0100
@@ -0,0 +1,112 @@
+#!/usr/bin/env bash
+#
+# $Id$
+# Author: Gerwin Klein, TU Muenchen
+#
+# DESCRIPTION: Build distribution and run isatest-make for lots of platforms.
+
+## global settings
+. ~/admin/isatest-settings
+
+TMP=/tmp/isatest-makedist.$$
+MAIL=$HOME/bin/pmail
+
+MAKEDIST=$HOME/bin/makedist
+MAKEALL=$HOME/bin/isatest-makeall
+TAR=gtar
+CVS2CL="$HOME/bin/cvs2cl --follow-only TRUNK"
+
+SSH="ssh -f"
+
+## diagnostics
+
+PRG="$(basename "$0")"
+
+function usage()
+{
+ echo
+ echo "Usage: $PRG"
+ echo
+ echo " Build distribution and run isatest-make for lots of platforms."
+ echo
+ exit 1
+}
+
+function fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
+## main
+
+# cleanup old error log and test-still-running files
+rm -f $ERRORLOG
+rm -f $ERRORDIR/isatest-*.log
+rm -f $RUNNING/*.runnning
+
+export DISTPREFIX
+export CVS2CL
+
+DATE=$(date "+%Y-%m-%d")
+DISTLOG=$LOGPREFIX/isatest-makedist-$DATE.log
+
+echo ------------------- preparing test release --- `date` --- $HOSTNAME > $DISTLOG 2>&1
+
+echo "### cleaning up old dist directory" >> $DISTLOG 2>&1
+rm -rf $DISTPREFIX >> $DISTLOG 2>&1
+
+echo "### cleaning up old isabelle-* directories" >> $DISTLOG 2>&1
+rm -rf $HOME/isabelle-*
+
+echo "### building distribution" >> $DISTLOG 2>&1
+mkdir -p $DISTPREFIX
+$MAKEDIST - >> $DISTLOG 2>&1
+
+if [ $? -ne 0 ]
+then
+ echo ------------------- DIST BUILD FAILED --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
+ ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
+ echo "$(date) $HOSTNAME $PRG: dist build FAILED, elapsed time $ELAPSED." >> $MASTERLOG
+
+ echo "Could not build isabelle distribution. Log file available at" > $TMP
+ echo "$HOSTNAME:$DISTLOG" >> $TMP
+
+ for R in $MAILTO; do
+ $MAIL "isabelle dist build failed" $R $TMP
+ done
+
+ rm $TMP
+
+ exit 1
+fi
+
+cd $DISTPREFIX >> $DISTLOG 2>&1
+$TAR xvzf `cat $DISTPREFIX/ISABELLE_DIST` >> $DISTLOG 2>&1
+
+echo ------------------- prepared test successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
+
+ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
+echo "$(date) $HOSTNAME $PRG: dist build successful, elapsed time $ELAPSED." >> $MASTERLOG
+
+
+## spawn test runs
+
+$SSH sunbroy2 "$MAKEALL $HOME/settings/sun-poly"
+# give test some time to copy settings and start
+sleep 5
+$SSH atbroy51 "$MAKEALL $HOME/settings/at-poly $HOME/settings/at-poly-e"
+sleep 5
+$SSH atbroy10 "$MAKEALL $HOME/settings/at-sml-dev"
+sleep 5
+$SSH atbroy101 "$MAKEALL $HOME/settings/at64-poly-e"
+sleep 5
+$SSH macbroy5 "$MAKEALL $HOME/settings/mac-poly $HOME/settings/mac-sml-dev"
+sleep 5
+$SSH macbroy6 "/usr/stud/isatest/bin/isatest-makeall $HOME/settings/at-mac-poly-e"
+
+echo ------------------- spawned tests successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
+
+gzip -f $DISTLOG
+
+## end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/isatest/isatest-settings Mon Mar 05 22:12:20 2007 +0100
@@ -0,0 +1,24 @@
+# -*- shell-script -*-
+# $Id$
+# Author: Gerwin Klein, NICTA
+#
+# DESCRIPTION: common settings for the isatest-* scripts
+
+# source bashrc, we're called by cron
+. ~/.bashrc
+
+# canoncical home for all platforms
+HOME=/home/isatest
+
+## send email on failure to
+MAILTO="kleing@cse.unsw.edu.au nipkow@in.tum.de berghofe@in.tum.de schirmer@in.tum.de lp15@cam.ac.uk makarius@sketis.net haftmann@in.tum.de"
+
+LOGPREFIX=$HOME/log
+MASTERLOG=$LOGPREFIX/isatest.log
+
+ERRORDIR=$HOME/var
+ERRORLOG=$ERRORDIR/error.log
+
+RUNNING=$HOME/var/running
+
+DISTPREFIX=$HOME/tmp/isadist
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/isatest/isatest-statistics Mon Mar 05 22:12:20 2007 +0100
@@ -0,0 +1,91 @@
+#!/usr/bin/env bash
+#
+# $Id$
+# Author: Makarius
+#
+# DESCRIPTION: Produce statistics from isatest session logs.
+
+ISATEST_LOG=~isatest/log
+
+## platform settings
+
+case $(uname) in
+ SunOS)
+ ZGREP=xgrep
+ TE="png color"
+ ;;
+ *)
+ ZGREP=zgrep
+ TE="png"
+ ;;
+esac
+
+## diagnostics
+
+PRG="$(basename "$0")"
+
+function usage()
+{
+ echo
+ echo "Usage: $PRG DIR PLATFORM TIMESPAN SESSIONS..."
+ echo
+ echo " Produce statistics from isatest session logs, looking TIMESPAN"
+ echo " days into the past. Outputs .png files into DIR."
+ echo
+ exit 1
+}
+
+function fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
+
+## arguments
+
+[ "$1" = "-?" ] && usage
+[ "$#" -lt "4" ] && usage
+
+DIR="$1"; shift
+PLATFORM="$1"; shift
+TIMESPAN="$1"; shift
+SESSIONS="$@"
+
+
+## main
+
+ALL_DATA="/tmp/isatest-all$$.dat"
+SESSION_DATA="/tmp/isatest$$.dat"
+mkdir -p "$DIR" || fail "Bad directory: $DIR"
+
+$ZGREP "^Finished .*elapsed" \
+ $(find "$ISATEST_LOG" -name "isatest-makeall-${PLATFORM}*" -ctime "-${TIMESPAN}") | \
+perl -e '
+ while (<>) {
+ if (m/isatest-makeall-.*-(\d+)-(\d+)-(\d+)-.*:Finished (\S+) \(.*, (\d+):(\d+):(\d+) cpu time\)/) {
+ my $year = $1;
+ my $month = $2;
+ my $day = $3;
+ my $name = $4;
+ my $time = ($5 * 3600 + $6 * 60 + $7) / 60;
+
+ printf "$name $year-$month-$day %.2f\n", $time;
+ }
+ }' > "$ALL_DATA"
+
+for SESSION in $SESSIONS
+do
+ fgrep "$SESSION " "$ALL_DATA" > "$SESSION_DATA"
+ gnuplot <<EOF
+set terminal $TE
+set output "$DIR/${SESSION}.png"
+set xdata time
+set timefmt "%Y-%m-%d"
+set format x "%d-%b"
+set xlabel "$SESSION"
+plot [] [0:] "$SESSION_DATA" using 2:3 smooth sbezier notitle, "$SESSION_DATA" using 2:3 smooth csplines notitle
+EOF
+done
+
+rm -f "$ALL_DATA" "$SESSION_DATA"
--- /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" <<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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/isatest/pmail Mon Mar 05 22:12:20 2007 +0100
@@ -0,0 +1,97 @@
+#!/usr/bin/env bash
+#
+# $Id$
+# Author: Gerwin Klein, TU Muenchen
+#
+# DESCRIPTION: send email with text attachments.
+# (works for "mail" command of SunOS 5.8)
+#
+
+PRG="$(basename "$0")"
+
+MIME_BOUNDARY="==PM_=_37427935"
+
+function usage()
+{
+ echo
+ echo "Usage: $PRG subject recipient <body> [<attachments>]"
+ echo
+ echo " Send email with text attachments. <body> is a file."
+ echo
+ exit 1
+}
+
+function fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
+#
+# print_attachment <file>
+#
+# print mime "encoded" <file> to stdout (text/plain, 8bit)
+#
+function print_attachment()
+{
+ local FILE=$1
+ local NAME=${FILE##*/}
+
+ cat <<EOF
+--$MIME_BOUNDARY
+Content-Type: text/plain
+Content-Transfer-Encoding: 8bit
+Content-Disposition: attachment; filename="$NAME"
+
+EOF
+ cat $FILE
+ echo
+}
+
+
+#
+# print_body subject <message-file> [<attachments>]
+#
+# prints mime "encoded" message with text attachments to stdout
+#
+function print_body()
+{
+ local SUBJECT=$1
+ local BODY=$2
+ shift 2
+
+ cat <<EOF
+Subject: $SUBJECT
+Mime-Version: 1.0
+Content-Type: multipart/mixed; boundary="$MIME_BOUNDARY"
+
+--$MIME_BOUNDARY
+Content-Type: text/plain
+Content-Transfer-Encoding: 8bit
+
+EOF
+ cat $BODY
+ echo
+
+ for a in $@; do print_attachment $a; done
+
+ echo "--$MIME_BOUNDARY--"
+ echo
+}
+
+## main
+
+# argument checking
+
+[ "$1" = "-?" ] && usage
+[ "$#" -lt "3" ] && usage
+
+SUBJECT="$1"
+TO="$2"
+BODY="$3"
+
+shift 3
+
+[ -r "$BODY" ] || fail "could not read $BODY"
+
+print_body "$SUBJECT" "$BODY" $@ | mail -t "$TO"
--- a/Admin/pmail Mon Mar 05 10:14:32 2007 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,97 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-# Author: Gerwin Klein, TU Muenchen
-#
-# DESCRIPTION: send email with text attachments.
-# (works for "mail" command of SunOS 5.8)
-#
-
-PRG="$(basename "$0")"
-
-MIME_BOUNDARY="==PM_=_37427935"
-
-function usage()
-{
- echo
- echo "Usage: $PRG subject recipient <body> [<attachments>]"
- echo
- echo " Send email with text attachments. <body> is a file."
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-#
-# print_attachment <file>
-#
-# print mime "encoded" <file> to stdout (text/plain, 8bit)
-#
-function print_attachment()
-{
- local FILE=$1
- local NAME=${FILE##*/}
-
- cat <<EOF
---$MIME_BOUNDARY
-Content-Type: text/plain
-Content-Transfer-Encoding: 8bit
-Content-Disposition: attachment; filename="$NAME"
-
-EOF
- cat $FILE
- echo
-}
-
-
-#
-# print_body subject <message-file> [<attachments>]
-#
-# prints mime "encoded" message with text attachments to stdout
-#
-function print_body()
-{
- local SUBJECT=$1
- local BODY=$2
- shift 2
-
- cat <<EOF
-Subject: $SUBJECT
-Mime-Version: 1.0
-Content-Type: multipart/mixed; boundary="$MIME_BOUNDARY"
-
---$MIME_BOUNDARY
-Content-Type: text/plain
-Content-Transfer-Encoding: 8bit
-
-EOF
- cat $BODY
- echo
-
- for a in $@; do print_attachment $a; done
-
- echo "--$MIME_BOUNDARY--"
- echo
-}
-
-## main
-
-# argument checking
-
-[ "$1" = "-?" ] && usage
-[ "$#" -lt "3" ] && usage
-
-SUBJECT="$1"
-TO="$2"
-BODY="$3"
-
-shift 3
-
-[ -r "$BODY" ] || fail "could not read $BODY"
-
-print_body "$SUBJECT" "$BODY" $@ | mail -t "$TO"