moved all isatest/cron job related files to own directory
authorkleing
Mon Mar 05 22:12:20 2007 +0100 (2007-03-05)
changeset 22410da313b67a04d
parent 22409 5f7c9c82b05e
child 22411 1956d895a4ed
moved all isatest/cron job related files to own directory
Admin/annomaly
Admin/isatest-check
Admin/isatest-doc
Admin/isatest-lint
Admin/isatest-makeall
Admin/isatest-makedist
Admin/isatest-settings
Admin/isatest-statistics
Admin/isatest-stats
Admin/isatest/annomaly
Admin/isatest/isatest-check
Admin/isatest/isatest-doc
Admin/isatest/isatest-lint
Admin/isatest/isatest-makeall
Admin/isatest/isatest-makedist
Admin/isatest/isatest-settings
Admin/isatest/isatest-statistics
Admin/isatest/isatest-stats
Admin/isatest/pmail
Admin/pmail
     1.1 --- a/Admin/annomaly	Mon Mar 05 10:14:32 2007 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,70 +0,0 @@
     1.4 -#!/bin/sh
     1.5 -
     1.6 -# Create AnnoMaLy documentation for Isabelle
     1.7 -# See http://martin.von-gagern.net/projects/annomaly/
     1.8 -#   2007  Martin von Gagern (martin@von-gagern.net)
     1.9 -
    1.10 -# Abort on any error
    1.11 -set -e -o pipefail
    1.12 -
    1.13 -ISABELLE_CVS="$(cd "$HOME/isabelle.cvs"; pwd -P)"
    1.14 -ISABELLE_HOME="$ISABELLE_CVS/Distribution"
    1.15 -HTML_DIR="$HOME/html-data/isabelle-doc"
    1.16 -export CVS_RSH=ssh
    1.17 -export SMLNJ_HOME="$HOME/annomaly"
    1.18 -export PATH="$SMLNJ_HOME/bin:$PATH"
    1.19 -export SML_DOC_DIR="$HTML_DIR.tmp"
    1.20 -export SML_DOC_REWRITE="isabelle=$ISABELLE_CVS"
    1.21 -# export SML_DOC_DEBUG="all"
    1.22 -TARGET=HOL
    1.23 -CVSUP=true
    1.24 -
    1.25 -# Parse command line
    1.26 -for ARG in "$@"; do case "$ARG" in
    1.27 -	-p) TARGET=Pure ;;
    1.28 -	-n) CVSUP=false ;;
    1.29 -	-l) export SML_LOG_DIR="$HOME/logs" ;;
    1.30 -esac; done
    1.31 -
    1.32 -# Create clean output directory
    1.33 -rm -rf "$SML_DOC_DIR"
    1.34 -mkdir "$SML_DOC_DIR"
    1.35 -cp "$SMLNJ_HOME/annomaly/resources/"* "$SML_DOC_DIR"
    1.36 -cat > "$SML_DOC_DIR/.htaccess" <<EOF
    1.37 -DirectoryIndex index.html source.html
    1.38 -<IfModule mod_deflate>
    1.39 -SetOutputFilter DEFLATE 
    1.40 -</IfModule>
    1.41 -AddType text/plain .dot
    1.42 -EOF
    1.43 -
    1.44 -# Update CVS
    1.45 -cd "$ISABELLE_CVS"
    1.46 -if $CVSUP; then
    1.47 -  echo "Updating CVS"
    1.48 -  cvs -q up -d
    1.49 -fi
    1.50 -
    1.51 -# Build isabelle
    1.52 -cd "$ISABELLE_HOME"
    1.53 -rm -rf heaps/*
    1.54 -./build -b $TARGET
    1.55 -
    1.56 -# Postprocess created files
    1.57 -cd $SML_DOC_DIR
    1.58 -dot -Tsvg depGraph.dot \
    1.59 -  | perl -pe 's/(width|height)="(\d+)/sprintf("%s=\"%.2f",$1,$2*0.6)/ge' \
    1.60 -  > depGraph.svg
    1.61 -dot -Tps2 depGraph.dot > depGraph.ps
    1.62 -ps2pdf depGraph.ps depGraph.pdf
    1.63 -grep -rl "$ISABELLE_HOME" . | xargs sed -i "s@$ISABELLE_HOME@\$ISABELLE_HOME@g"
    1.64 -
    1.65 -# Install result by renaming to be almost atomic
    1.66 -rm -rf "$HTML_DIR.bac"
    1.67 -if [[ -d $HTML_DIR ]]; then mv "$HTML_DIR" "$HTML_DIR.bac"; fi
    1.68 -mv "$SML_DOC_DIR" "$HTML_DIR"
    1.69 -rm -rf "$HTML_DIR.bac"
    1.70 -
    1.71 -# Done
    1.72 -echo "Completed successfully"
    1.73 -exit 0
     2.1 --- a/Admin/isatest-check	Mon Mar 05 10:14:32 2007 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,105 +0,0 @@
     2.4 -#!/usr/bin/env bash
     2.5 -#
     2.6 -# $Id$
     2.7 -# Author: Gerwin Klein, TU Muenchen
     2.8 -#
     2.9 -# DESCRIPTION: sends email for failed tests, checks for error.log,
    2.10 -#              generates development snapshot if test ok
    2.11 -
    2.12 -## global settings
    2.13 -. ~/admin/isatest-settings
    2.14 -
    2.15 -# produce empty list for patterns like isatest-*.log if no 
    2.16 -# such file exists 
    2.17 -shopt -s nullglob
    2.18 -
    2.19 -# mail program
    2.20 -MAIL=$HOME/bin/pmail
    2.21 -
    2.22 -# tmp file for sending mail
    2.23 -TMP=/tmp/isatest-makedist.$$
    2.24 -
    2.25 -export DISTPREFIX
    2.26 -
    2.27 -
    2.28 -## diagnostics
    2.29 -
    2.30 -PRG="$(basename "$0")"
    2.31 -
    2.32 -function usage()
    2.33 -{
    2.34 -  echo
    2.35 -  echo "Usage: $PRG"
    2.36 -  echo
    2.37 -  echo "   sends email for failed tests, checks for error.log,"
    2.38 -  echo "   generates development snapshot if test ok."
    2.39 -  echo "   To be called by cron."
    2.40 -  echo
    2.41 -  exit 1
    2.42 -}
    2.43 -
    2.44 -function fail()
    2.45 -{
    2.46 -  echo "$1" >&2
    2.47 -  exit 2
    2.48 -}
    2.49 -
    2.50 -## main
    2.51 -
    2.52 -# check if tests are still running, wait for them a couple of hours
    2.53 -i=0
    2.54 -while [ -n "$(ls $RUNNING)" -a $i -lt 8 ]; do 
    2.55 -    sleep 3600
    2.56 -    let "i = i+1"
    2.57 -done
    2.58 -
    2.59 -FAIL=0
    2.60 -
    2.61 -# still running -> give up
    2.62 -if [ -n "$(ls $RUNNING)" ]; then
    2.63 -    echo "Giving up waiting for test to finish at $(date)." > $TMP
    2.64 -    echo >> $TMP
    2.65 -    echo "Sessions still running:" >> $TMP
    2.66 -    echo "$(ls $RUNNING)" >> $TMP
    2.67 -    echo >> $TMP
    2.68 -    echo "Attaching all error logs collected so far." >> $TMP
    2.69 -    echo >> $TMP
    2.70 -
    2.71 -    if [ -e $ERRORLOG ]; then
    2.72 -        cat $ERRORLOG >> $TMP
    2.73 -    fi
    2.74 -
    2.75 -    echo "Have a nice day," >> $TMP
    2.76 -    echo "  isatest" >> $TMP
    2.77 -
    2.78 -    for R in $MAILTO; do
    2.79 -        LOGS=$ERRORDIR/isatest*.log
    2.80 -        $MAIL "isabelle test taking too long" $R $TMP $LOGS
    2.81 -    done
    2.82 -
    2.83 -    rm $TMP
    2.84 -    
    2.85 -    FAIL=1
    2.86 -elif [ -e $ERRORLOG ]; then
    2.87 -  # no tests running, check if there were errors
    2.88 -    cat $ERRORLOG > $TMP
    2.89 -    echo "Have a nice day," >> $TMP
    2.90 -    echo "  isatest" >> $TMP
    2.91 -
    2.92 -    for R in $MAILTO; do
    2.93 -        LOGS=$ERRORDIR/isatest*.log
    2.94 -        $MAIL "isabelle test failed" $R $TMP $LOGS
    2.95 -    done
    2.96 -    
    2.97 -    rm $TMP
    2.98 -fi
    2.99 -
   2.100 -# generate development snapshot page only for successful tests
   2.101 -# (failures in experimental sessions ok)
   2.102 -if [ "$FAIL"=="0" -a "$(echo $ERRORDIR/isatest*[^e].log)" == "$(echo)" ]; then
   2.103 -  (cd $HOME/devel-page; env DISTNAME=`$DISTPREFIX/Isabelle/bin/isatool version` make)
   2.104 -  echo "$(date) $HOSTNAME $PRG: generated development snapshot web page." >> $MASTERLOG
   2.105 -fi
   2.106 -
   2.107 -exit 0
   2.108 -## end
     3.1 --- a/Admin/isatest-doc	Mon Mar 05 10:14:32 2007 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,127 +0,0 @@
     3.4 -#!/usr/bin/env bash
     3.5 -#
     3.6 -# $Id$
     3.7 -# Author: Gerwin Klein, NICTA
     3.8 -#
     3.9 -# Run IsaMakefile for every Doc/ subdirectory.
    3.10 -#
    3.11 -# Relies on being run in the isatest environment on sunbroy2.
    3.12 -# 
    3.13 -
    3.14 -. ~/.bashrc
    3.15 -
    3.16 -## global settings
    3.17 -. ~/admin/isatest-settings
    3.18 -
    3.19 -DOCDIR=$HOME/Doc
    3.20 -
    3.21 -MAXTIME=1800
    3.22 -
    3.23 -ISABELLE_DEVEL=$DISTPREFIX/Isabelle
    3.24 -DATE=$(date "+%Y-%m-%d")
    3.25 -
    3.26 -LOG=$LOGPREFIX/isatest-doc-$DATE.log
    3.27 -
    3.28 -SHORT=sun-poly
    3.29 -SETTINGS=~/settings/$SHORT
    3.30 -
    3.31 -ISATOOL=$ISABELLE_DEVEL/bin/isatool
    3.32 -    
    3.33 -
    3.34 -MAIL=~/afp/release/admin/mail-attach
    3.35 -
    3.36 -TMP=/tmp/isatest-doc.mail.tmp
    3.37 -while [ -e $TMP ]; do TMP=$TMP.x; done
    3.38 -
    3.39 -#
    3.40 -PRG="$(basename "$0")"
    3.41 -
    3.42 -## functions
    3.43 -
    3.44 -function usage()
    3.45 -{
    3.46 -  echo
    3.47 -  echo "Usage: $PRG"
    3.48 -  echo
    3.49 -  echo "  Run IsaMakefile for every Doc/ subdirectory"
    3.50 -  echo 
    3.51 -  exit 1
    3.52 -}
    3.53 -
    3.54 -function fail()
    3.55 -{
    3.56 -  echo "$1" >&2
    3.57 -  exit 2
    3.58 -}
    3.59 -
    3.60 -## 
    3.61 -
    3.62 -[ "$#" != "0" ] && usage
    3.63 -
    3.64 -if [ -f "$RUNNING/$SHORT.running" -o -e $ERRORLOG ]; then
    3.65 -  echo "$(date) $HOSTNAME $PRG: Skipped test. Isabelle devel version broken." >> $MASTERLOG
    3.66 -  exit 1
    3.67 -fi
    3.68 -cat $SETTINGS >> $ISABELLE_DEVEL/etc/settings
    3.69 -
    3.70 -
    3.71 -echo "Start test at `date`" > $LOG
    3.72 -echo >> $LOG
    3.73 -echo "begin cvs update" >> $LOG
    3.74 -
    3.75 -# cvs update to newest version 
    3.76 -cd $DOCDIR || fail "could not cd to $DOCDIR"
    3.77 -cvs -q up -A -P -d >> $LOG 2>&1 || fail "could not CVS update."
    3.78 -
    3.79 -echo "end cvs update" >> $LOG
    3.80 -echo >> $LOG
    3.81 -
    3.82 -# run test
    3.83 -FAIL="";
    3.84 -
    3.85 -cd $DOCDIR
    3.86 -for DIR in */; do
    3.87 -  if [ -f "$DIR/IsaMakefile" ]; then
    3.88 -    echo "Testing [$DIR]" >> $LOG
    3.89 -    (
    3.90 -      cd $DIR
    3.91 -      ulimit -t $MAXTIME 
    3.92 -      nice $ISATOOL make >> $LOG 2>&1
    3.93 -    ) || FAIL="${FAIL}${DIR} "    
    3.94 -    echo "Finished [$DIR]" >> $LOG
    3.95 -    echo >> $LOG
    3.96 -  fi
    3.97 -done
    3.98 -
    3.99 -ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
   3.100 -
   3.101 -echo >> $LOG
   3.102 -echo "End test on `date`, elapsed time: $ELAPSED" >> $LOG
   3.103 -
   3.104 -# send email if there was a problem
   3.105 -if [ "$FAIL" != "" ]; then
   3.106 -  echo >> $LOG
   3.107 -  echo "Failed sessions: ${FAIL}" >> $LOG
   3.108 -
   3.109 -  echo "$(date) $HOSTNAME $PRG: doc test FAILED for ${FAIL}, elapsed time $ELAPSED." >> $MASTERLOG
   3.110 -
   3.111 -  cat > $TMP <<EOF
   3.112 -Session(s) ${FAIL} in the documentation test failed (log attached).
   3.113 -Test ended on: $HOSTNAME, `date`.
   3.114 -
   3.115 -Have a nice day,
   3.116 -  isatest
   3.117 -
   3.118 -EOF
   3.119 -
   3.120 -  for R in $MAILTO; do
   3.121 -    $MAIL 'doc test failed' "$R" $TMP $LOG
   3.122 -  done
   3.123 -
   3.124 -  rm -f $TMP
   3.125 -
   3.126 -  exit 1
   3.127 -else
   3.128 -  echo "$(date) $HOSTNAME $PRG: doc test successful, elapsed time $ELAPSED." >> $MASTERLOG
   3.129 -fi
   3.130 -
     4.1 --- a/Admin/isatest-lint	Mon Mar 05 10:14:32 2007 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,41 +0,0 @@
     4.4 -#!/usr/bin/env perl
     4.5 -#
     4.6 -# $Id$
     4.7 -# Author: Florian Haftmann, TUM
     4.8 -#
     4.9 -# Do consistency and quality checks on the isabelle sources
    4.10 -#
    4.11 -
    4.12 -use strict;
    4.13 -use File::Find;
    4.14 -use File::Basename;
    4.15 -
    4.16 -# configuration
    4.17 -my $isabelleRoot = $ENV{'HOME'} . "/isabelle";
    4.18 -my @suffices = ('\.thy', '\.ml', '\.ML');
    4.19 -
    4.20 -# lint main procedure
    4.21 -sub lint() {
    4.22 -    my ($basename, $dirname, $ext) = fileparse($File::Find::name, @suffices);
    4.23 -    if ($ext) {
    4.24 -        open ISTREAM, $File::Find::name or die("error opening $File::Find::name");
    4.25 -        my $found = 0;
    4.26 -        while (<ISTREAM>) {
    4.27 -            $found ||= m/\$Id[^\$]*\$/;
    4.28 -            last if $found;
    4.29 -        }
    4.30 -        close ISTREAM;
    4.31 -        my $relname = substr($File::Find::name, (length $isabelleRoot) + 1);
    4.32 -        if (! $found) {
    4.33 -            print "Found no CVS id in $relname\n";
    4.34 -        }
    4.35 -    }
    4.36 -}
    4.37 -
    4.38 -# first argument =^= isabelle repository root
    4.39 -if (@ARGV) {
    4.40 -    $isabelleRoot = $ARGV[0];
    4.41 -}
    4.42 -
    4.43 -find(\&lint, $isabelleRoot);
    4.44 -
     5.1 --- a/Admin/isatest-makeall	Mon Mar 05 10:14:32 2007 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,134 +0,0 @@
     5.4 -#!/usr/bin/env bash
     5.5 -#
     5.6 -# $Id$
     5.7 -# Author: Gerwin Klein, TU Muenchen
     5.8 -#
     5.9 -# DESCRIPTION: Run isatool makeall from specified distribution and settings.
    5.10 -
    5.11 -## global settings
    5.12 -. ~/admin/isatest-settings
    5.13 -
    5.14 -# max time until test is aborted (in sec)
    5.15 -MAXTIME=28800
    5.16 -
    5.17 -## diagnostics
    5.18 -
    5.19 -PRG="$(basename "$0")"
    5.20 -
    5.21 -function usage()
    5.22 -{
    5.23 -  echo
    5.24 -  echo "Usage: $PRG settings1 [settings2 ...]"
    5.25 -  echo
    5.26 -  echo "  Runs isatool makeall for specified settings."
    5.27 -  echo "  Leaves messages in ${ERRORLOG} and ${LOGPREFIX} if it fails."
    5.28 -  echo
    5.29 -  exit 1
    5.30 -}
    5.31 -
    5.32 -function fail()
    5.33 -{
    5.34 -  echo "$1" >&2
    5.35 -  echo "$(date) $HOSTNAME $PRG: FAILED, $1" >> $MASTERLOG
    5.36 -  exit 2
    5.37 -}
    5.38 -
    5.39 -## main
    5.40 -
    5.41 -# argument checking
    5.42 -
    5.43 -[ "$1" = "-?" ] && usage
    5.44 -[ "$#" -lt "1" ] && usage
    5.45 -
    5.46 -[ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
    5.47 -
    5.48 -# make file flags and nice setup for different target platforms
    5.49 -case $HOSTNAME in
    5.50 -    atbroy51)
    5.51 -        # 2 processors
    5.52 -        MFLAGS="-j 2"
    5.53 -        # MFLAGS=""
    5.54 -        NICE=""
    5.55 -        ;;
    5.56 -
    5.57 -    atbroy31)
    5.58 -        # cluster
    5.59 -        MFLAGS="-j 5"
    5.60 -        ;;
    5.61 -  
    5.62 -    sunbroy2)
    5.63 -        MFLAGS="-j 6"
    5.64 -        NICE="nice"
    5.65 -        ;;
    5.66 -
    5.67 -    sunbroy1)
    5.68 -        MFLAGS="-j 2"
    5.69 -        NICE="nice"
    5.70 -        ;;
    5.71 -
    5.72 -    macbroy5)
    5.73 -        MFLAGS="" # -j 2 does not work on poly/macos 10.4.1
    5.74 -        NICE=""
    5.75 -        ;;
    5.76 -
    5.77 -    *)
    5.78 -        MFLAGS=""
    5.79 -        # be nice by default
    5.80 -        NICE=nice
    5.81 -        ;;
    5.82 -esac
    5.83 -
    5.84 -# main test loop
    5.85 -
    5.86 -for SETTINGS in $@; do
    5.87 -
    5.88 -    [ -r $SETTINGS ] || fail "Cannot read $SETTINGS."
    5.89 -
    5.90 -    # logfile setup
    5.91 -
    5.92 -    DATE=$(date "+%Y-%m-%d")
    5.93 -    SHORT=${SETTINGS##*/}
    5.94 -    TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log
    5.95 -
    5.96 -    # the test
    5.97 -
    5.98 -    touch $RUNNING/$SHORT.running
    5.99 -
   5.100 -    echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
   5.101 -
   5.102 -    cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
   5.103 -    (ulimit -t $MAXTIME; $NICE $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1)
   5.104 -
   5.105 -    if [ $? -eq 0 ]
   5.106 -    then
   5.107 -        # test log and cleanup
   5.108 -        echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
   5.109 -        gzip -f $TESTLOG
   5.110 -    else
   5.111 -        # test log
   5.112 -        echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
   5.113 -
   5.114 -        # error log
   5.115 -        echo "Test for platform ${SHORT} failed. Log file attached." >> $ERRORLOG
   5.116 -        echo "[...]" >> $ERRORLOG
   5.117 -        tail -3 $TESTLOG >> $ERRORLOG
   5.118 -        echo >> $ERRORLOG
   5.119 -
   5.120 -        FAIL="$FAIL$SHORT "
   5.121 -        (cd $ERRORDIR; ln -s $TESTLOG)
   5.122 -    fi
   5.123 -
   5.124 -    rm -f $RUNNING/$SHORT.running
   5.125 -done
   5.126 -
   5.127 -# time and success/failure to master log
   5.128 -ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
   5.129 -
   5.130 -if [ -z "$FAIL" ]; then
   5.131 -    echo "$(date) $HOSTNAME $PRG: all tests successful, elapsed time $ELAPSED." >> $MASTERLOG
   5.132 -else
   5.133 -    echo "$(date) $HOSTNAME $PRG: targets ${FAIL}FAILED, elapsed time $ELAPSED." >> $MASTERLOG
   5.134 -    exit 1
   5.135 -fi
   5.136 -
   5.137 -# end
     6.1 --- a/Admin/isatest-makedist	Mon Mar 05 10:14:32 2007 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,112 +0,0 @@
     6.4 -#!/usr/bin/env bash
     6.5 -#
     6.6 -# $Id$
     6.7 -# Author: Gerwin Klein, TU Muenchen
     6.8 -#
     6.9 -# DESCRIPTION: Build distribution and run isatest-make for lots of platforms.
    6.10 -
    6.11 -## global settings
    6.12 -. ~/admin/isatest-settings
    6.13 -
    6.14 -TMP=/tmp/isatest-makedist.$$
    6.15 -MAIL=$HOME/bin/pmail
    6.16 -
    6.17 -MAKEDIST=$HOME/bin/makedist
    6.18 -MAKEALL=$HOME/bin/isatest-makeall
    6.19 -TAR=gtar
    6.20 -CVS2CL="$HOME/bin/cvs2cl --follow-only TRUNK"
    6.21 -
    6.22 -SSH="ssh -f"
    6.23 -
    6.24 -## diagnostics
    6.25 -
    6.26 -PRG="$(basename "$0")"
    6.27 -
    6.28 -function usage()
    6.29 -{
    6.30 -  echo
    6.31 -  echo "Usage: $PRG"
    6.32 -  echo
    6.33 -  echo "   Build distribution and run isatest-make for lots of platforms."
    6.34 -  echo
    6.35 -  exit 1
    6.36 -}
    6.37 -
    6.38 -function fail()
    6.39 -{
    6.40 -  echo "$1" >&2
    6.41 -  exit 2
    6.42 -}
    6.43 -
    6.44 -## main
    6.45 -
    6.46 -# cleanup old error log and test-still-running files
    6.47 -rm -f $ERRORLOG
    6.48 -rm -f $ERRORDIR/isatest-*.log
    6.49 -rm -f $RUNNING/*.runnning
    6.50 -
    6.51 -export DISTPREFIX
    6.52 -export CVS2CL
    6.53 -
    6.54 -DATE=$(date "+%Y-%m-%d")
    6.55 -DISTLOG=$LOGPREFIX/isatest-makedist-$DATE.log
    6.56 -
    6.57 -echo ------------------- preparing test release --- `date` --- $HOSTNAME > $DISTLOG 2>&1
    6.58 -
    6.59 -echo "### cleaning up old dist directory"  >> $DISTLOG 2>&1
    6.60 -rm -rf $DISTPREFIX >> $DISTLOG 2>&1
    6.61 -
    6.62 -echo "### cleaning up old isabelle-* directories" >> $DISTLOG 2>&1
    6.63 -rm -rf $HOME/isabelle-*
    6.64 -
    6.65 -echo "### building distribution"  >> $DISTLOG 2>&1
    6.66 -mkdir -p $DISTPREFIX
    6.67 -$MAKEDIST - >> $DISTLOG 2>&1
    6.68 -
    6.69 -if [ $? -ne 0 ]
    6.70 -then
    6.71 -    echo ------------------- DIST BUILD FAILED --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
    6.72 -    ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
    6.73 -    echo "$(date) $HOSTNAME $PRG: dist build FAILED, elapsed time $ELAPSED." >> $MASTERLOG
    6.74 -
    6.75 -    echo "Could not build isabelle distribution. Log file available at" > $TMP
    6.76 -    echo "$HOSTNAME:$DISTLOG" >> $TMP
    6.77 -
    6.78 -    for R in $MAILTO; do
    6.79 -        $MAIL "isabelle dist build failed" $R $TMP
    6.80 -    done
    6.81 -
    6.82 -    rm $TMP
    6.83 -
    6.84 -    exit 1
    6.85 -fi
    6.86 -
    6.87 -cd $DISTPREFIX >> $DISTLOG 2>&1
    6.88 -$TAR xvzf `cat $DISTPREFIX/ISABELLE_DIST` >> $DISTLOG 2>&1
    6.89 -
    6.90 -echo ------------------- prepared test successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
    6.91 -
    6.92 -ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
    6.93 -echo "$(date) $HOSTNAME $PRG: dist build successful, elapsed time $ELAPSED." >> $MASTERLOG
    6.94 -
    6.95 -
    6.96 -## spawn test runs
    6.97 -
    6.98 -$SSH sunbroy2 "$MAKEALL $HOME/settings/sun-poly"
    6.99 -# give test some time to copy settings and start
   6.100 -sleep 5
   6.101 -$SSH atbroy51 "$MAKEALL $HOME/settings/at-poly $HOME/settings/at-poly-e"
   6.102 -sleep 5
   6.103 -$SSH atbroy10 "$MAKEALL $HOME/settings/at-sml-dev"
   6.104 -sleep 5
   6.105 -$SSH atbroy101 "$MAKEALL $HOME/settings/at64-poly-e"
   6.106 -sleep 5
   6.107 -$SSH macbroy5 "$MAKEALL $HOME/settings/mac-poly $HOME/settings/mac-sml-dev"
   6.108 -sleep 5
   6.109 -$SSH macbroy6 "/usr/stud/isatest/bin/isatest-makeall $HOME/settings/at-mac-poly-e"
   6.110 -
   6.111 -echo ------------------- spawned tests successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
   6.112 -
   6.113 -gzip -f $DISTLOG
   6.114 -
   6.115 -## end
     7.1 --- a/Admin/isatest-settings	Mon Mar 05 10:14:32 2007 +0100
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,24 +0,0 @@
     7.4 -# -*- shell-script -*-
     7.5 -# $Id$
     7.6 -# Author: Gerwin Klein, NICTA
     7.7 -#
     7.8 -# DESCRIPTION: common settings for the isatest-* scripts
     7.9 -
    7.10 -# source bashrc, we're called by cron
    7.11 -. ~/.bashrc
    7.12 -
    7.13 -# canoncical home for all platforms
    7.14 -HOME=/home/isatest
    7.15 -
    7.16 -## send email on failure to
    7.17 -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"
    7.18 -
    7.19 -LOGPREFIX=$HOME/log
    7.20 -MASTERLOG=$LOGPREFIX/isatest.log
    7.21 -
    7.22 -ERRORDIR=$HOME/var
    7.23 -ERRORLOG=$ERRORDIR/error.log
    7.24 -
    7.25 -RUNNING=$HOME/var/running
    7.26 -
    7.27 -DISTPREFIX=$HOME/tmp/isadist
     8.1 --- a/Admin/isatest-statistics	Mon Mar 05 10:14:32 2007 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,91 +0,0 @@
     8.4 -#!/usr/bin/env bash
     8.5 -#
     8.6 -# $Id$
     8.7 -# Author: Makarius
     8.8 -#
     8.9 -# DESCRIPTION: Produce statistics from isatest session logs.
    8.10 -
    8.11 -ISATEST_LOG=~isatest/log
    8.12 -
    8.13 -## platform settings
    8.14 -
    8.15 -case $(uname) in
    8.16 -	SunOS)	
    8.17 -		ZGREP=xgrep 
    8.18 -		TE="png color"
    8.19 -	;;
    8.20 -	*)	
    8.21 -		ZGREP=zgrep
    8.22 -		TE="png"
    8.23 -	;;
    8.24 -esac
    8.25 -
    8.26 -## diagnostics
    8.27 -
    8.28 -PRG="$(basename "$0")"
    8.29 -
    8.30 -function usage()
    8.31 -{
    8.32 -  echo
    8.33 -  echo "Usage: $PRG DIR PLATFORM TIMESPAN SESSIONS..."
    8.34 -  echo
    8.35 -  echo "  Produce statistics from isatest session logs, looking TIMESPAN"
    8.36 -  echo "  days into the past.  Outputs .png files into DIR."
    8.37 -  echo
    8.38 -  exit 1
    8.39 -}
    8.40 -
    8.41 -function fail()
    8.42 -{
    8.43 -  echo "$1" >&2
    8.44 -  exit 2
    8.45 -}
    8.46 -
    8.47 -
    8.48 -## arguments
    8.49 -
    8.50 -[ "$1" = "-?" ] && usage
    8.51 -[ "$#" -lt "4" ] && usage
    8.52 -
    8.53 -DIR="$1"; shift
    8.54 -PLATFORM="$1"; shift
    8.55 -TIMESPAN="$1"; shift
    8.56 -SESSIONS="$@"
    8.57 -
    8.58 -
    8.59 -## main
    8.60 -
    8.61 -ALL_DATA="/tmp/isatest-all$$.dat"
    8.62 -SESSION_DATA="/tmp/isatest$$.dat"
    8.63 -mkdir -p "$DIR" || fail "Bad directory: $DIR"
    8.64 -
    8.65 -$ZGREP "^Finished .*elapsed" \
    8.66 -  $(find "$ISATEST_LOG" -name "isatest-makeall-${PLATFORM}*" -ctime "-${TIMESPAN}") | \
    8.67 -perl -e '
    8.68 -  while (<>) {
    8.69 -    if (m/isatest-makeall-.*-(\d+)-(\d+)-(\d+)-.*:Finished (\S+) \(.*, (\d+):(\d+):(\d+) cpu time\)/) {
    8.70 -        my $year = $1;
    8.71 -        my $month = $2;
    8.72 -        my $day = $3;
    8.73 -        my $name = $4;
    8.74 -        my $time = ($5 * 3600 + $6 * 60 + $7) / 60;
    8.75 -
    8.76 -        printf "$name $year-$month-$day %.2f\n", $time;
    8.77 -    }
    8.78 -  }' > "$ALL_DATA"
    8.79 -
    8.80 -for SESSION in $SESSIONS
    8.81 -do
    8.82 -  fgrep "$SESSION " "$ALL_DATA" > "$SESSION_DATA"
    8.83 -  gnuplot <<EOF
    8.84 -set terminal $TE
    8.85 -set output "$DIR/${SESSION}.png"
    8.86 -set xdata time
    8.87 -set timefmt "%Y-%m-%d"
    8.88 -set format x "%d-%b"
    8.89 -set xlabel "$SESSION"
    8.90 -plot [] [0:] "$SESSION_DATA" using 2:3 smooth sbezier notitle, "$SESSION_DATA" using 2:3 smooth csplines notitle
    8.91 -EOF
    8.92 -done
    8.93 -
    8.94 -rm -f "$ALL_DATA" "$SESSION_DATA"
     9.1 --- a/Admin/isatest-stats	Mon Mar 05 10:14:32 2007 +0100
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,51 +0,0 @@
     9.4 -#!/usr/bin/env bash
     9.5 -#
     9.6 -# $Id$
     9.7 -# Author: Makarius
     9.8 -#
     9.9 -# DESCRIPTION: Standard statistics.
    9.10 -
    9.11 -THIS=$(cd "$(dirname "$0")"; pwd -P)
    9.12 -
    9.13 -PLATFORMS="at-poly at-sml-dev at-mac-poly-e at64-poly-e"
    9.14 -SESSIONS="\
    9.15 -  HOL \
    9.16 -  HOL-Algebra \
    9.17 -  HOL-Auth \
    9.18 -  HOL-Bali \
    9.19 -  HOL-Complex \
    9.20 -  HOL-Complex-ex \
    9.21 -  HOL-Extraction \
    9.22 -  HOL-Hoare \
    9.23 -  HOL-HoareParallel \
    9.24 -  HOL-Lambda \
    9.25 -  HOL-MicroJava \
    9.26 -  HOL-NumberTheory \
    9.27 -  HOL-SET-Protocol \
    9.28 -  HOL-UNITY \
    9.29 -  HOL-ex \
    9.30 -  ZF \
    9.31 -  ZF-Constructible\
    9.32 -  ZF-UNITY"
    9.33 -
    9.34 -for PLATFORM in $PLATFORMS
    9.35 -do
    9.36 -  "$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" ${1:-100} $SESSIONS
    9.37 -  cat > "stats/$PLATFORM.html" <<EOF
    9.38 -<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
    9.39 -<html>
    9.40 -<head><title>Development Snapshot -- Performance Statistics</title></head>
    9.41 -
    9.42 -<body>
    9.43 -<h1>$PLATFORM</h1>
    9.44 -EOF
    9.45 -
    9.46 -for SESSION in $SESSIONS
    9.47 -do
    9.48 -  echo "<br><img src="$PLATFORM/$SESSION.png"><br>" >> "stats/$PLATFORM.html"
    9.49 -done
    9.50 -
    9.51 -echo "</body>" >> "stats/$PLATFORM.html"
    9.52 -echo "</html>" >> "stats/$PLATFORM.html"
    9.53 -
    9.54 -done
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/Admin/isatest/annomaly	Mon Mar 05 22:12:20 2007 +0100
    10.3 @@ -0,0 +1,70 @@
    10.4 +#!/bin/sh
    10.5 +
    10.6 +# Create AnnoMaLy documentation for Isabelle
    10.7 +# See http://martin.von-gagern.net/projects/annomaly/
    10.8 +#   2007  Martin von Gagern (martin@von-gagern.net)
    10.9 +
   10.10 +# Abort on any error
   10.11 +set -e -o pipefail
   10.12 +
   10.13 +ISABELLE_CVS="$(cd "$HOME/isabelle.cvs"; pwd -P)"
   10.14 +ISABELLE_HOME="$ISABELLE_CVS/Distribution"
   10.15 +HTML_DIR="$HOME/html-data/isabelle-doc"
   10.16 +export CVS_RSH=ssh
   10.17 +export SMLNJ_HOME="$HOME/annomaly"
   10.18 +export PATH="$SMLNJ_HOME/bin:$PATH"
   10.19 +export SML_DOC_DIR="$HTML_DIR.tmp"
   10.20 +export SML_DOC_REWRITE="isabelle=$ISABELLE_CVS"
   10.21 +# export SML_DOC_DEBUG="all"
   10.22 +TARGET=HOL
   10.23 +CVSUP=true
   10.24 +
   10.25 +# Parse command line
   10.26 +for ARG in "$@"; do case "$ARG" in
   10.27 +	-p) TARGET=Pure ;;
   10.28 +	-n) CVSUP=false ;;
   10.29 +	-l) export SML_LOG_DIR="$HOME/logs" ;;
   10.30 +esac; done
   10.31 +
   10.32 +# Create clean output directory
   10.33 +rm -rf "$SML_DOC_DIR"
   10.34 +mkdir "$SML_DOC_DIR"
   10.35 +cp "$SMLNJ_HOME/annomaly/resources/"* "$SML_DOC_DIR"
   10.36 +cat > "$SML_DOC_DIR/.htaccess" <<EOF
   10.37 +DirectoryIndex index.html source.html
   10.38 +<IfModule mod_deflate>
   10.39 +SetOutputFilter DEFLATE 
   10.40 +</IfModule>
   10.41 +AddType text/plain .dot
   10.42 +EOF
   10.43 +
   10.44 +# Update CVS
   10.45 +cd "$ISABELLE_CVS"
   10.46 +if $CVSUP; then
   10.47 +  echo "Updating CVS"
   10.48 +  cvs -q up -d
   10.49 +fi
   10.50 +
   10.51 +# Build isabelle
   10.52 +cd "$ISABELLE_HOME"
   10.53 +rm -rf heaps/*
   10.54 +./build -b $TARGET
   10.55 +
   10.56 +# Postprocess created files
   10.57 +cd $SML_DOC_DIR
   10.58 +dot -Tsvg depGraph.dot \
   10.59 +  | perl -pe 's/(width|height)="(\d+)/sprintf("%s=\"%.2f",$1,$2*0.6)/ge' \
   10.60 +  > depGraph.svg
   10.61 +dot -Tps2 depGraph.dot > depGraph.ps
   10.62 +ps2pdf depGraph.ps depGraph.pdf
   10.63 +grep -rl "$ISABELLE_HOME" . | xargs sed -i "s@$ISABELLE_HOME@\$ISABELLE_HOME@g"
   10.64 +
   10.65 +# Install result by renaming to be almost atomic
   10.66 +rm -rf "$HTML_DIR.bac"
   10.67 +if [[ -d $HTML_DIR ]]; then mv "$HTML_DIR" "$HTML_DIR.bac"; fi
   10.68 +mv "$SML_DOC_DIR" "$HTML_DIR"
   10.69 +rm -rf "$HTML_DIR.bac"
   10.70 +
   10.71 +# Done
   10.72 +echo "Completed successfully"
   10.73 +exit 0
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/Admin/isatest/isatest-check	Mon Mar 05 22:12:20 2007 +0100
    11.3 @@ -0,0 +1,105 @@
    11.4 +#!/usr/bin/env bash
    11.5 +#
    11.6 +# $Id$
    11.7 +# Author: Gerwin Klein, TU Muenchen
    11.8 +#
    11.9 +# DESCRIPTION: sends email for failed tests, checks for error.log,
   11.10 +#              generates development snapshot if test ok
   11.11 +
   11.12 +## global settings
   11.13 +. ~/admin/isatest-settings
   11.14 +
   11.15 +# produce empty list for patterns like isatest-*.log if no 
   11.16 +# such file exists 
   11.17 +shopt -s nullglob
   11.18 +
   11.19 +# mail program
   11.20 +MAIL=$HOME/bin/pmail
   11.21 +
   11.22 +# tmp file for sending mail
   11.23 +TMP=/tmp/isatest-makedist.$$
   11.24 +
   11.25 +export DISTPREFIX
   11.26 +
   11.27 +
   11.28 +## diagnostics
   11.29 +
   11.30 +PRG="$(basename "$0")"
   11.31 +
   11.32 +function usage()
   11.33 +{
   11.34 +  echo
   11.35 +  echo "Usage: $PRG"
   11.36 +  echo
   11.37 +  echo "   sends email for failed tests, checks for error.log,"
   11.38 +  echo "   generates development snapshot if test ok."
   11.39 +  echo "   To be called by cron."
   11.40 +  echo
   11.41 +  exit 1
   11.42 +}
   11.43 +
   11.44 +function fail()
   11.45 +{
   11.46 +  echo "$1" >&2
   11.47 +  exit 2
   11.48 +}
   11.49 +
   11.50 +## main
   11.51 +
   11.52 +# check if tests are still running, wait for them a couple of hours
   11.53 +i=0
   11.54 +while [ -n "$(ls $RUNNING)" -a $i -lt 8 ]; do 
   11.55 +    sleep 3600
   11.56 +    let "i = i+1"
   11.57 +done
   11.58 +
   11.59 +FAIL=0
   11.60 +
   11.61 +# still running -> give up
   11.62 +if [ -n "$(ls $RUNNING)" ]; then
   11.63 +    echo "Giving up waiting for test to finish at $(date)." > $TMP
   11.64 +    echo >> $TMP
   11.65 +    echo "Sessions still running:" >> $TMP
   11.66 +    echo "$(ls $RUNNING)" >> $TMP
   11.67 +    echo >> $TMP
   11.68 +    echo "Attaching all error logs collected so far." >> $TMP
   11.69 +    echo >> $TMP
   11.70 +
   11.71 +    if [ -e $ERRORLOG ]; then
   11.72 +        cat $ERRORLOG >> $TMP
   11.73 +    fi
   11.74 +
   11.75 +    echo "Have a nice day," >> $TMP
   11.76 +    echo "  isatest" >> $TMP
   11.77 +
   11.78 +    for R in $MAILTO; do
   11.79 +        LOGS=$ERRORDIR/isatest*.log
   11.80 +        $MAIL "isabelle test taking too long" $R $TMP $LOGS
   11.81 +    done
   11.82 +
   11.83 +    rm $TMP
   11.84 +    
   11.85 +    FAIL=1
   11.86 +elif [ -e $ERRORLOG ]; then
   11.87 +  # no tests running, check if there were errors
   11.88 +    cat $ERRORLOG > $TMP
   11.89 +    echo "Have a nice day," >> $TMP
   11.90 +    echo "  isatest" >> $TMP
   11.91 +
   11.92 +    for R in $MAILTO; do
   11.93 +        LOGS=$ERRORDIR/isatest*.log
   11.94 +        $MAIL "isabelle test failed" $R $TMP $LOGS
   11.95 +    done
   11.96 +    
   11.97 +    rm $TMP
   11.98 +fi
   11.99 +
  11.100 +# generate development snapshot page only for successful tests
  11.101 +# (failures in experimental sessions ok)
  11.102 +if [ "$FAIL"=="0" -a "$(echo $ERRORDIR/isatest*[^e].log)" == "$(echo)" ]; then
  11.103 +  (cd $HOME/devel-page; env DISTNAME=`$DISTPREFIX/Isabelle/bin/isatool version` make)
  11.104 +  echo "$(date) $HOSTNAME $PRG: generated development snapshot web page." >> $MASTERLOG
  11.105 +fi
  11.106 +
  11.107 +exit 0
  11.108 +## end
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/Admin/isatest/isatest-doc	Mon Mar 05 22:12:20 2007 +0100
    12.3 @@ -0,0 +1,127 @@
    12.4 +#!/usr/bin/env bash
    12.5 +#
    12.6 +# $Id$
    12.7 +# Author: Gerwin Klein, NICTA
    12.8 +#
    12.9 +# Run IsaMakefile for every Doc/ subdirectory.
   12.10 +#
   12.11 +# Relies on being run in the isatest environment on sunbroy2.
   12.12 +# 
   12.13 +
   12.14 +. ~/.bashrc
   12.15 +
   12.16 +## global settings
   12.17 +. ~/admin/isatest-settings
   12.18 +
   12.19 +DOCDIR=$HOME/Doc
   12.20 +
   12.21 +MAXTIME=1800
   12.22 +
   12.23 +ISABELLE_DEVEL=$DISTPREFIX/Isabelle
   12.24 +DATE=$(date "+%Y-%m-%d")
   12.25 +
   12.26 +LOG=$LOGPREFIX/isatest-doc-$DATE.log
   12.27 +
   12.28 +SHORT=sun-poly
   12.29 +SETTINGS=~/settings/$SHORT
   12.30 +
   12.31 +ISATOOL=$ISABELLE_DEVEL/bin/isatool
   12.32 +    
   12.33 +
   12.34 +MAIL=~/afp/release/admin/mail-attach
   12.35 +
   12.36 +TMP=/tmp/isatest-doc.mail.tmp
   12.37 +while [ -e $TMP ]; do TMP=$TMP.x; done
   12.38 +
   12.39 +#
   12.40 +PRG="$(basename "$0")"
   12.41 +
   12.42 +## functions
   12.43 +
   12.44 +function usage()
   12.45 +{
   12.46 +  echo
   12.47 +  echo "Usage: $PRG"
   12.48 +  echo
   12.49 +  echo "  Run IsaMakefile for every Doc/ subdirectory"
   12.50 +  echo 
   12.51 +  exit 1
   12.52 +}
   12.53 +
   12.54 +function fail()
   12.55 +{
   12.56 +  echo "$1" >&2
   12.57 +  exit 2
   12.58 +}
   12.59 +
   12.60 +## 
   12.61 +
   12.62 +[ "$#" != "0" ] && usage
   12.63 +
   12.64 +if [ -f "$RUNNING/$SHORT.running" -o -e $ERRORLOG ]; then
   12.65 +  echo "$(date) $HOSTNAME $PRG: Skipped test. Isabelle devel version broken." >> $MASTERLOG
   12.66 +  exit 1
   12.67 +fi
   12.68 +cat $SETTINGS >> $ISABELLE_DEVEL/etc/settings
   12.69 +
   12.70 +
   12.71 +echo "Start test at `date`" > $LOG
   12.72 +echo >> $LOG
   12.73 +echo "begin cvs update" >> $LOG
   12.74 +
   12.75 +# cvs update to newest version 
   12.76 +cd $DOCDIR || fail "could not cd to $DOCDIR"
   12.77 +cvs -q up -A -P -d >> $LOG 2>&1 || fail "could not CVS update."
   12.78 +
   12.79 +echo "end cvs update" >> $LOG
   12.80 +echo >> $LOG
   12.81 +
   12.82 +# run test
   12.83 +FAIL="";
   12.84 +
   12.85 +cd $DOCDIR
   12.86 +for DIR in */; do
   12.87 +  if [ -f "$DIR/IsaMakefile" ]; then
   12.88 +    echo "Testing [$DIR]" >> $LOG
   12.89 +    (
   12.90 +      cd $DIR
   12.91 +      ulimit -t $MAXTIME 
   12.92 +      nice $ISATOOL make >> $LOG 2>&1
   12.93 +    ) || FAIL="${FAIL}${DIR} "    
   12.94 +    echo "Finished [$DIR]" >> $LOG
   12.95 +    echo >> $LOG
   12.96 +  fi
   12.97 +done
   12.98 +
   12.99 +ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
  12.100 +
  12.101 +echo >> $LOG
  12.102 +echo "End test on `date`, elapsed time: $ELAPSED" >> $LOG
  12.103 +
  12.104 +# send email if there was a problem
  12.105 +if [ "$FAIL" != "" ]; then
  12.106 +  echo >> $LOG
  12.107 +  echo "Failed sessions: ${FAIL}" >> $LOG
  12.108 +
  12.109 +  echo "$(date) $HOSTNAME $PRG: doc test FAILED for ${FAIL}, elapsed time $ELAPSED." >> $MASTERLOG
  12.110 +
  12.111 +  cat > $TMP <<EOF
  12.112 +Session(s) ${FAIL} in the documentation test failed (log attached).
  12.113 +Test ended on: $HOSTNAME, `date`.
  12.114 +
  12.115 +Have a nice day,
  12.116 +  isatest
  12.117 +
  12.118 +EOF
  12.119 +
  12.120 +  for R in $MAILTO; do
  12.121 +    $MAIL 'doc test failed' "$R" $TMP $LOG
  12.122 +  done
  12.123 +
  12.124 +  rm -f $TMP
  12.125 +
  12.126 +  exit 1
  12.127 +else
  12.128 +  echo "$(date) $HOSTNAME $PRG: doc test successful, elapsed time $ELAPSED." >> $MASTERLOG
  12.129 +fi
  12.130 +
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/Admin/isatest/isatest-lint	Mon Mar 05 22:12:20 2007 +0100
    13.3 @@ -0,0 +1,41 @@
    13.4 +#!/usr/bin/env perl
    13.5 +#
    13.6 +# $Id$
    13.7 +# Author: Florian Haftmann, TUM
    13.8 +#
    13.9 +# Do consistency and quality checks on the isabelle sources
   13.10 +#
   13.11 +
   13.12 +use strict;
   13.13 +use File::Find;
   13.14 +use File::Basename;
   13.15 +
   13.16 +# configuration
   13.17 +my $isabelleRoot = $ENV{'HOME'} . "/isabelle";
   13.18 +my @suffices = ('\.thy', '\.ml', '\.ML');
   13.19 +
   13.20 +# lint main procedure
   13.21 +sub lint() {
   13.22 +    my ($basename, $dirname, $ext) = fileparse($File::Find::name, @suffices);
   13.23 +    if ($ext) {
   13.24 +        open ISTREAM, $File::Find::name or die("error opening $File::Find::name");
   13.25 +        my $found = 0;
   13.26 +        while (<ISTREAM>) {
   13.27 +            $found ||= m/\$Id[^\$]*\$/;
   13.28 +            last if $found;
   13.29 +        }
   13.30 +        close ISTREAM;
   13.31 +        my $relname = substr($File::Find::name, (length $isabelleRoot) + 1);
   13.32 +        if (! $found) {
   13.33 +            print "Found no CVS id in $relname\n";
   13.34 +        }
   13.35 +    }
   13.36 +}
   13.37 +
   13.38 +# first argument =^= isabelle repository root
   13.39 +if (@ARGV) {
   13.40 +    $isabelleRoot = $ARGV[0];
   13.41 +}
   13.42 +
   13.43 +find(\&lint, $isabelleRoot);
   13.44 +
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/Admin/isatest/isatest-makeall	Mon Mar 05 22:12:20 2007 +0100
    14.3 @@ -0,0 +1,134 @@
    14.4 +#!/usr/bin/env bash
    14.5 +#
    14.6 +# $Id$
    14.7 +# Author: Gerwin Klein, TU Muenchen
    14.8 +#
    14.9 +# DESCRIPTION: Run isatool makeall from specified distribution and settings.
   14.10 +
   14.11 +## global settings
   14.12 +. ~/admin/isatest-settings
   14.13 +
   14.14 +# max time until test is aborted (in sec)
   14.15 +MAXTIME=28800
   14.16 +
   14.17 +## diagnostics
   14.18 +
   14.19 +PRG="$(basename "$0")"
   14.20 +
   14.21 +function usage()
   14.22 +{
   14.23 +  echo
   14.24 +  echo "Usage: $PRG settings1 [settings2 ...]"
   14.25 +  echo
   14.26 +  echo "  Runs isatool makeall for specified settings."
   14.27 +  echo "  Leaves messages in ${ERRORLOG} and ${LOGPREFIX} if it fails."
   14.28 +  echo
   14.29 +  exit 1
   14.30 +}
   14.31 +
   14.32 +function fail()
   14.33 +{
   14.34 +  echo "$1" >&2
   14.35 +  echo "$(date) $HOSTNAME $PRG: FAILED, $1" >> $MASTERLOG
   14.36 +  exit 2
   14.37 +}
   14.38 +
   14.39 +## main
   14.40 +
   14.41 +# argument checking
   14.42 +
   14.43 +[ "$1" = "-?" ] && usage
   14.44 +[ "$#" -lt "1" ] && usage
   14.45 +
   14.46 +[ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
   14.47 +
   14.48 +# make file flags and nice setup for different target platforms
   14.49 +case $HOSTNAME in
   14.50 +    atbroy51)
   14.51 +        # 2 processors
   14.52 +        MFLAGS="-j 2"
   14.53 +        # MFLAGS=""
   14.54 +        NICE=""
   14.55 +        ;;
   14.56 +
   14.57 +    atbroy31)
   14.58 +        # cluster
   14.59 +        MFLAGS="-j 5"
   14.60 +        ;;
   14.61 +  
   14.62 +    sunbroy2)
   14.63 +        MFLAGS="-j 6"
   14.64 +        NICE="nice"
   14.65 +        ;;
   14.66 +
   14.67 +    sunbroy1)
   14.68 +        MFLAGS="-j 2"
   14.69 +        NICE="nice"
   14.70 +        ;;
   14.71 +
   14.72 +    macbroy5)
   14.73 +        MFLAGS="" # -j 2 does not work on poly/macos 10.4.1
   14.74 +        NICE=""
   14.75 +        ;;
   14.76 +
   14.77 +    *)
   14.78 +        MFLAGS=""
   14.79 +        # be nice by default
   14.80 +        NICE=nice
   14.81 +        ;;
   14.82 +esac
   14.83 +
   14.84 +# main test loop
   14.85 +
   14.86 +for SETTINGS in $@; do
   14.87 +
   14.88 +    [ -r $SETTINGS ] || fail "Cannot read $SETTINGS."
   14.89 +
   14.90 +    # logfile setup
   14.91 +
   14.92 +    DATE=$(date "+%Y-%m-%d")
   14.93 +    SHORT=${SETTINGS##*/}
   14.94 +    TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log
   14.95 +
   14.96 +    # the test
   14.97 +
   14.98 +    touch $RUNNING/$SHORT.running
   14.99 +
  14.100 +    echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
  14.101 +
  14.102 +    cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
  14.103 +    (ulimit -t $MAXTIME; $NICE $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1)
  14.104 +
  14.105 +    if [ $? -eq 0 ]
  14.106 +    then
  14.107 +        # test log and cleanup
  14.108 +        echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
  14.109 +        gzip -f $TESTLOG
  14.110 +    else
  14.111 +        # test log
  14.112 +        echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
  14.113 +
  14.114 +        # error log
  14.115 +        echo "Test for platform ${SHORT} failed. Log file attached." >> $ERRORLOG
  14.116 +        echo "[...]" >> $ERRORLOG
  14.117 +        tail -3 $TESTLOG >> $ERRORLOG
  14.118 +        echo >> $ERRORLOG
  14.119 +
  14.120 +        FAIL="$FAIL$SHORT "
  14.121 +        (cd $ERRORDIR; ln -s $TESTLOG)
  14.122 +    fi
  14.123 +
  14.124 +    rm -f $RUNNING/$SHORT.running
  14.125 +done
  14.126 +
  14.127 +# time and success/failure to master log
  14.128 +ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
  14.129 +
  14.130 +if [ -z "$FAIL" ]; then
  14.131 +    echo "$(date) $HOSTNAME $PRG: all tests successful, elapsed time $ELAPSED." >> $MASTERLOG
  14.132 +else
  14.133 +    echo "$(date) $HOSTNAME $PRG: targets ${FAIL}FAILED, elapsed time $ELAPSED." >> $MASTERLOG
  14.134 +    exit 1
  14.135 +fi
  14.136 +
  14.137 +# end
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/Admin/isatest/isatest-makedist	Mon Mar 05 22:12:20 2007 +0100
    15.3 @@ -0,0 +1,112 @@
    15.4 +#!/usr/bin/env bash
    15.5 +#
    15.6 +# $Id$
    15.7 +# Author: Gerwin Klein, TU Muenchen
    15.8 +#
    15.9 +# DESCRIPTION: Build distribution and run isatest-make for lots of platforms.
   15.10 +
   15.11 +## global settings
   15.12 +. ~/admin/isatest-settings
   15.13 +
   15.14 +TMP=/tmp/isatest-makedist.$$
   15.15 +MAIL=$HOME/bin/pmail
   15.16 +
   15.17 +MAKEDIST=$HOME/bin/makedist
   15.18 +MAKEALL=$HOME/bin/isatest-makeall
   15.19 +TAR=gtar
   15.20 +CVS2CL="$HOME/bin/cvs2cl --follow-only TRUNK"
   15.21 +
   15.22 +SSH="ssh -f"
   15.23 +
   15.24 +## diagnostics
   15.25 +
   15.26 +PRG="$(basename "$0")"
   15.27 +
   15.28 +function usage()
   15.29 +{
   15.30 +  echo
   15.31 +  echo "Usage: $PRG"
   15.32 +  echo
   15.33 +  echo "   Build distribution and run isatest-make for lots of platforms."
   15.34 +  echo
   15.35 +  exit 1
   15.36 +}
   15.37 +
   15.38 +function fail()
   15.39 +{
   15.40 +  echo "$1" >&2
   15.41 +  exit 2
   15.42 +}
   15.43 +
   15.44 +## main
   15.45 +
   15.46 +# cleanup old error log and test-still-running files
   15.47 +rm -f $ERRORLOG
   15.48 +rm -f $ERRORDIR/isatest-*.log
   15.49 +rm -f $RUNNING/*.runnning
   15.50 +
   15.51 +export DISTPREFIX
   15.52 +export CVS2CL
   15.53 +
   15.54 +DATE=$(date "+%Y-%m-%d")
   15.55 +DISTLOG=$LOGPREFIX/isatest-makedist-$DATE.log
   15.56 +
   15.57 +echo ------------------- preparing test release --- `date` --- $HOSTNAME > $DISTLOG 2>&1
   15.58 +
   15.59 +echo "### cleaning up old dist directory"  >> $DISTLOG 2>&1
   15.60 +rm -rf $DISTPREFIX >> $DISTLOG 2>&1
   15.61 +
   15.62 +echo "### cleaning up old isabelle-* directories" >> $DISTLOG 2>&1
   15.63 +rm -rf $HOME/isabelle-*
   15.64 +
   15.65 +echo "### building distribution"  >> $DISTLOG 2>&1
   15.66 +mkdir -p $DISTPREFIX
   15.67 +$MAKEDIST - >> $DISTLOG 2>&1
   15.68 +
   15.69 +if [ $? -ne 0 ]
   15.70 +then
   15.71 +    echo ------------------- DIST BUILD FAILED --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
   15.72 +    ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
   15.73 +    echo "$(date) $HOSTNAME $PRG: dist build FAILED, elapsed time $ELAPSED." >> $MASTERLOG
   15.74 +
   15.75 +    echo "Could not build isabelle distribution. Log file available at" > $TMP
   15.76 +    echo "$HOSTNAME:$DISTLOG" >> $TMP
   15.77 +
   15.78 +    for R in $MAILTO; do
   15.79 +        $MAIL "isabelle dist build failed" $R $TMP
   15.80 +    done
   15.81 +
   15.82 +    rm $TMP
   15.83 +
   15.84 +    exit 1
   15.85 +fi
   15.86 +
   15.87 +cd $DISTPREFIX >> $DISTLOG 2>&1
   15.88 +$TAR xvzf `cat $DISTPREFIX/ISABELLE_DIST` >> $DISTLOG 2>&1
   15.89 +
   15.90 +echo ------------------- prepared test successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
   15.91 +
   15.92 +ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
   15.93 +echo "$(date) $HOSTNAME $PRG: dist build successful, elapsed time $ELAPSED." >> $MASTERLOG
   15.94 +
   15.95 +
   15.96 +## spawn test runs
   15.97 +
   15.98 +$SSH sunbroy2 "$MAKEALL $HOME/settings/sun-poly"
   15.99 +# give test some time to copy settings and start
  15.100 +sleep 5
  15.101 +$SSH atbroy51 "$MAKEALL $HOME/settings/at-poly $HOME/settings/at-poly-e"
  15.102 +sleep 5
  15.103 +$SSH atbroy10 "$MAKEALL $HOME/settings/at-sml-dev"
  15.104 +sleep 5
  15.105 +$SSH atbroy101 "$MAKEALL $HOME/settings/at64-poly-e"
  15.106 +sleep 5
  15.107 +$SSH macbroy5 "$MAKEALL $HOME/settings/mac-poly $HOME/settings/mac-sml-dev"
  15.108 +sleep 5
  15.109 +$SSH macbroy6 "/usr/stud/isatest/bin/isatest-makeall $HOME/settings/at-mac-poly-e"
  15.110 +
  15.111 +echo ------------------- spawned tests successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
  15.112 +
  15.113 +gzip -f $DISTLOG
  15.114 +
  15.115 +## end
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/Admin/isatest/isatest-settings	Mon Mar 05 22:12:20 2007 +0100
    16.3 @@ -0,0 +1,24 @@
    16.4 +# -*- shell-script -*-
    16.5 +# $Id$
    16.6 +# Author: Gerwin Klein, NICTA
    16.7 +#
    16.8 +# DESCRIPTION: common settings for the isatest-* scripts
    16.9 +
   16.10 +# source bashrc, we're called by cron
   16.11 +. ~/.bashrc
   16.12 +
   16.13 +# canoncical home for all platforms
   16.14 +HOME=/home/isatest
   16.15 +
   16.16 +## send email on failure to
   16.17 +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"
   16.18 +
   16.19 +LOGPREFIX=$HOME/log
   16.20 +MASTERLOG=$LOGPREFIX/isatest.log
   16.21 +
   16.22 +ERRORDIR=$HOME/var
   16.23 +ERRORLOG=$ERRORDIR/error.log
   16.24 +
   16.25 +RUNNING=$HOME/var/running
   16.26 +
   16.27 +DISTPREFIX=$HOME/tmp/isadist
    17.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.2 +++ b/Admin/isatest/isatest-statistics	Mon Mar 05 22:12:20 2007 +0100
    17.3 @@ -0,0 +1,91 @@
    17.4 +#!/usr/bin/env bash
    17.5 +#
    17.6 +# $Id$
    17.7 +# Author: Makarius
    17.8 +#
    17.9 +# DESCRIPTION: Produce statistics from isatest session logs.
   17.10 +
   17.11 +ISATEST_LOG=~isatest/log
   17.12 +
   17.13 +## platform settings
   17.14 +
   17.15 +case $(uname) in
   17.16 +	SunOS)	
   17.17 +		ZGREP=xgrep 
   17.18 +		TE="png color"
   17.19 +	;;
   17.20 +	*)	
   17.21 +		ZGREP=zgrep
   17.22 +		TE="png"
   17.23 +	;;
   17.24 +esac
   17.25 +
   17.26 +## diagnostics
   17.27 +
   17.28 +PRG="$(basename "$0")"
   17.29 +
   17.30 +function usage()
   17.31 +{
   17.32 +  echo
   17.33 +  echo "Usage: $PRG DIR PLATFORM TIMESPAN SESSIONS..."
   17.34 +  echo
   17.35 +  echo "  Produce statistics from isatest session logs, looking TIMESPAN"
   17.36 +  echo "  days into the past.  Outputs .png files into DIR."
   17.37 +  echo
   17.38 +  exit 1
   17.39 +}
   17.40 +
   17.41 +function fail()
   17.42 +{
   17.43 +  echo "$1" >&2
   17.44 +  exit 2
   17.45 +}
   17.46 +
   17.47 +
   17.48 +## arguments
   17.49 +
   17.50 +[ "$1" = "-?" ] && usage
   17.51 +[ "$#" -lt "4" ] && usage
   17.52 +
   17.53 +DIR="$1"; shift
   17.54 +PLATFORM="$1"; shift
   17.55 +TIMESPAN="$1"; shift
   17.56 +SESSIONS="$@"
   17.57 +
   17.58 +
   17.59 +## main
   17.60 +
   17.61 +ALL_DATA="/tmp/isatest-all$$.dat"
   17.62 +SESSION_DATA="/tmp/isatest$$.dat"
   17.63 +mkdir -p "$DIR" || fail "Bad directory: $DIR"
   17.64 +
   17.65 +$ZGREP "^Finished .*elapsed" \
   17.66 +  $(find "$ISATEST_LOG" -name "isatest-makeall-${PLATFORM}*" -ctime "-${TIMESPAN}") | \
   17.67 +perl -e '
   17.68 +  while (<>) {
   17.69 +    if (m/isatest-makeall-.*-(\d+)-(\d+)-(\d+)-.*:Finished (\S+) \(.*, (\d+):(\d+):(\d+) cpu time\)/) {
   17.70 +        my $year = $1;
   17.71 +        my $month = $2;
   17.72 +        my $day = $3;
   17.73 +        my $name = $4;
   17.74 +        my $time = ($5 * 3600 + $6 * 60 + $7) / 60;
   17.75 +
   17.76 +        printf "$name $year-$month-$day %.2f\n", $time;
   17.77 +    }
   17.78 +  }' > "$ALL_DATA"
   17.79 +
   17.80 +for SESSION in $SESSIONS
   17.81 +do
   17.82 +  fgrep "$SESSION " "$ALL_DATA" > "$SESSION_DATA"
   17.83 +  gnuplot <<EOF
   17.84 +set terminal $TE
   17.85 +set output "$DIR/${SESSION}.png"
   17.86 +set xdata time
   17.87 +set timefmt "%Y-%m-%d"
   17.88 +set format x "%d-%b"
   17.89 +set xlabel "$SESSION"
   17.90 +plot [] [0:] "$SESSION_DATA" using 2:3 smooth sbezier notitle, "$SESSION_DATA" using 2:3 smooth csplines notitle
   17.91 +EOF
   17.92 +done
   17.93 +
   17.94 +rm -f "$ALL_DATA" "$SESSION_DATA"
    18.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.2 +++ b/Admin/isatest/isatest-stats	Mon Mar 05 22:12:20 2007 +0100
    18.3 @@ -0,0 +1,51 @@
    18.4 +#!/usr/bin/env bash
    18.5 +#
    18.6 +# $Id$
    18.7 +# Author: Makarius
    18.8 +#
    18.9 +# DESCRIPTION: Standard statistics.
   18.10 +
   18.11 +THIS=$(cd "$(dirname "$0")"; pwd -P)
   18.12 +
   18.13 +PLATFORMS="at-poly at-sml-dev at-mac-poly-e at64-poly-e"
   18.14 +SESSIONS="\
   18.15 +  HOL \
   18.16 +  HOL-Algebra \
   18.17 +  HOL-Auth \
   18.18 +  HOL-Bali \
   18.19 +  HOL-Complex \
   18.20 +  HOL-Complex-ex \
   18.21 +  HOL-Extraction \
   18.22 +  HOL-Hoare \
   18.23 +  HOL-HoareParallel \
   18.24 +  HOL-Lambda \
   18.25 +  HOL-MicroJava \
   18.26 +  HOL-NumberTheory \
   18.27 +  HOL-SET-Protocol \
   18.28 +  HOL-UNITY \
   18.29 +  HOL-ex \
   18.30 +  ZF \
   18.31 +  ZF-Constructible\
   18.32 +  ZF-UNITY"
   18.33 +
   18.34 +for PLATFORM in $PLATFORMS
   18.35 +do
   18.36 +  "$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" ${1:-100} $SESSIONS
   18.37 +  cat > "stats/$PLATFORM.html" <<EOF
   18.38 +<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
   18.39 +<html>
   18.40 +<head><title>Development Snapshot -- Performance Statistics</title></head>
   18.41 +
   18.42 +<body>
   18.43 +<h1>$PLATFORM</h1>
   18.44 +EOF
   18.45 +
   18.46 +for SESSION in $SESSIONS
   18.47 +do
   18.48 +  echo "<br><img src="$PLATFORM/$SESSION.png"><br>" >> "stats/$PLATFORM.html"
   18.49 +done
   18.50 +
   18.51 +echo "</body>" >> "stats/$PLATFORM.html"
   18.52 +echo "</html>" >> "stats/$PLATFORM.html"
   18.53 +
   18.54 +done
    19.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.2 +++ b/Admin/isatest/pmail	Mon Mar 05 22:12:20 2007 +0100
    19.3 @@ -0,0 +1,97 @@
    19.4 +#!/usr/bin/env bash
    19.5 +#
    19.6 +# $Id$
    19.7 +# Author: Gerwin Klein, TU Muenchen
    19.8 +#
    19.9 +# DESCRIPTION: send email with text attachments.
   19.10 +# (works for "mail" command of SunOS 5.8)
   19.11 +#
   19.12 +
   19.13 +PRG="$(basename "$0")"
   19.14 +
   19.15 +MIME_BOUNDARY="==PM_=_37427935"
   19.16 +
   19.17 +function usage()
   19.18 +{
   19.19 +  echo
   19.20 +  echo "Usage: $PRG subject recipient <body> [<attachments>]"
   19.21 +  echo
   19.22 +  echo "  Send email with text attachments. <body> is a file."
   19.23 +  echo
   19.24 +  exit 1
   19.25 +}
   19.26 +
   19.27 +function fail()
   19.28 +{
   19.29 +  echo "$1" >&2
   19.30 +  exit 2
   19.31 +}
   19.32 +
   19.33 +#
   19.34 +# print_attachment <file>
   19.35 +#
   19.36 +# print mime "encoded" <file> to stdout (text/plain, 8bit)
   19.37 +#
   19.38 +function print_attachment()
   19.39 +{
   19.40 +    local FILE=$1
   19.41 +    local NAME=${FILE##*/}
   19.42 +
   19.43 +    cat <<EOF
   19.44 +--$MIME_BOUNDARY
   19.45 +Content-Type: text/plain
   19.46 +Content-Transfer-Encoding: 8bit
   19.47 +Content-Disposition: attachment; filename="$NAME"
   19.48 +
   19.49 +EOF
   19.50 +    cat $FILE
   19.51 +    echo
   19.52 +}
   19.53 +
   19.54 +
   19.55 +#
   19.56 +# print_body subject <message-file> [<attachments>]
   19.57 +#
   19.58 +# prints mime "encoded" message with text attachments to stdout
   19.59 +#
   19.60 +function print_body()
   19.61 +{
   19.62 +    local SUBJECT=$1
   19.63 +    local BODY=$2
   19.64 +    shift 2
   19.65 +
   19.66 +    cat <<EOF
   19.67 +Subject: $SUBJECT
   19.68 +Mime-Version: 1.0
   19.69 +Content-Type: multipart/mixed; boundary="$MIME_BOUNDARY"
   19.70 +
   19.71 +--$MIME_BOUNDARY
   19.72 +Content-Type: text/plain
   19.73 +Content-Transfer-Encoding: 8bit
   19.74 +
   19.75 +EOF
   19.76 +    cat $BODY
   19.77 +    echo
   19.78 +
   19.79 +    for a in $@; do print_attachment $a; done
   19.80 +
   19.81 +    echo "--$MIME_BOUNDARY--"
   19.82 +    echo 
   19.83 +}
   19.84 +
   19.85 +## main
   19.86 +
   19.87 +# argument checking
   19.88 +
   19.89 +[ "$1" = "-?" ] && usage
   19.90 +[ "$#" -lt "3" ] && usage
   19.91 +
   19.92 +SUBJECT="$1"
   19.93 +TO="$2"
   19.94 +BODY="$3"
   19.95 +
   19.96 +shift 3
   19.97 +
   19.98 +[ -r "$BODY" ] || fail "could not read $BODY"
   19.99 +
  19.100 +print_body "$SUBJECT" "$BODY" $@ | mail -t "$TO"
    20.1 --- a/Admin/pmail	Mon Mar 05 10:14:32 2007 +0100
    20.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.3 @@ -1,97 +0,0 @@
    20.4 -#!/usr/bin/env bash
    20.5 -#
    20.6 -# $Id$
    20.7 -# Author: Gerwin Klein, TU Muenchen
    20.8 -#
    20.9 -# DESCRIPTION: send email with text attachments.
   20.10 -# (works for "mail" command of SunOS 5.8)
   20.11 -#
   20.12 -
   20.13 -PRG="$(basename "$0")"
   20.14 -
   20.15 -MIME_BOUNDARY="==PM_=_37427935"
   20.16 -
   20.17 -function usage()
   20.18 -{
   20.19 -  echo
   20.20 -  echo "Usage: $PRG subject recipient <body> [<attachments>]"
   20.21 -  echo
   20.22 -  echo "  Send email with text attachments. <body> is a file."
   20.23 -  echo
   20.24 -  exit 1
   20.25 -}
   20.26 -
   20.27 -function fail()
   20.28 -{
   20.29 -  echo "$1" >&2
   20.30 -  exit 2
   20.31 -}
   20.32 -
   20.33 -#
   20.34 -# print_attachment <file>
   20.35 -#
   20.36 -# print mime "encoded" <file> to stdout (text/plain, 8bit)
   20.37 -#
   20.38 -function print_attachment()
   20.39 -{
   20.40 -    local FILE=$1
   20.41 -    local NAME=${FILE##*/}
   20.42 -
   20.43 -    cat <<EOF
   20.44 ---$MIME_BOUNDARY
   20.45 -Content-Type: text/plain
   20.46 -Content-Transfer-Encoding: 8bit
   20.47 -Content-Disposition: attachment; filename="$NAME"
   20.48 -
   20.49 -EOF
   20.50 -    cat $FILE
   20.51 -    echo
   20.52 -}
   20.53 -
   20.54 -
   20.55 -#
   20.56 -# print_body subject <message-file> [<attachments>]
   20.57 -#
   20.58 -# prints mime "encoded" message with text attachments to stdout
   20.59 -#
   20.60 -function print_body()
   20.61 -{
   20.62 -    local SUBJECT=$1
   20.63 -    local BODY=$2
   20.64 -    shift 2
   20.65 -
   20.66 -    cat <<EOF
   20.67 -Subject: $SUBJECT
   20.68 -Mime-Version: 1.0
   20.69 -Content-Type: multipart/mixed; boundary="$MIME_BOUNDARY"
   20.70 -
   20.71 ---$MIME_BOUNDARY
   20.72 -Content-Type: text/plain
   20.73 -Content-Transfer-Encoding: 8bit
   20.74 -
   20.75 -EOF
   20.76 -    cat $BODY
   20.77 -    echo
   20.78 -
   20.79 -    for a in $@; do print_attachment $a; done
   20.80 -
   20.81 -    echo "--$MIME_BOUNDARY--"
   20.82 -    echo 
   20.83 -}
   20.84 -
   20.85 -## main
   20.86 -
   20.87 -# argument checking
   20.88 -
   20.89 -[ "$1" = "-?" ] && usage
   20.90 -[ "$#" -lt "3" ] && usage
   20.91 -
   20.92 -SUBJECT="$1"
   20.93 -TO="$2"
   20.94 -BODY="$3"
   20.95 -
   20.96 -shift 3
   20.97 -
   20.98 -[ -r "$BODY" ] || fail "could not read $BODY"
   20.99 -
  20.100 -print_body "$SUBJECT" "$BODY" $@ | mail -t "$TO"