# HG changeset patch
# User kleing
# Date 1173129140 -3600
# Node ID da313b67a04d833e8a032ffee1d25bb7276492c3
# Parent  5f7c9c82b05eaaa3cc1c3cfb59380ffac156ebad
moved all isatest/cron job related files to own directory

diff -r 5f7c9c82b05e -r da313b67a04d Admin/annomaly
--- 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
diff -r 5f7c9c82b05e -r da313b67a04d Admin/isatest-check
--- 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
diff -r 5f7c9c82b05e -r da313b67a04d Admin/isatest-doc
--- 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
-
diff -r 5f7c9c82b05e -r da313b67a04d Admin/isatest-lint
--- 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);
-
diff -r 5f7c9c82b05e -r da313b67a04d Admin/isatest-makeall
--- 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
diff -r 5f7c9c82b05e -r da313b67a04d Admin/isatest-makedist
--- 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
diff -r 5f7c9c82b05e -r da313b67a04d Admin/isatest-settings
--- 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
diff -r 5f7c9c82b05e -r da313b67a04d Admin/isatest-statistics
--- 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"
diff -r 5f7c9c82b05e -r da313b67a04d Admin/isatest-stats
--- 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
diff -r 5f7c9c82b05e -r da313b67a04d Admin/isatest/annomaly
--- /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
diff -r 5f7c9c82b05e -r da313b67a04d Admin/isatest/isatest-check
--- /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
diff -r 5f7c9c82b05e -r da313b67a04d Admin/isatest/isatest-doc
--- /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
+
diff -r 5f7c9c82b05e -r da313b67a04d Admin/isatest/isatest-lint
--- /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);
+
diff -r 5f7c9c82b05e -r da313b67a04d Admin/isatest/isatest-makeall
--- /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
diff -r 5f7c9c82b05e -r da313b67a04d Admin/isatest/isatest-makedist
--- /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
diff -r 5f7c9c82b05e -r da313b67a04d Admin/isatest/isatest-settings
--- /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
diff -r 5f7c9c82b05e -r da313b67a04d Admin/isatest/isatest-statistics
--- /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"
diff -r 5f7c9c82b05e -r da313b67a04d Admin/isatest/isatest-stats
--- /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
diff -r 5f7c9c82b05e -r da313b67a04d Admin/isatest/pmail
--- /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"
diff -r 5f7c9c82b05e -r da313b67a04d Admin/pmail
--- 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"