Admin/isatest/isatest-check

generalize lemma of_nat_number_of_eq to class number_semiring

#!/usr/bin/env bash
#
# 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/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 40 ]; do 
    sleep 900
    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/isabelle getenv -b ISABELLE_IDENTIFIER` make)
  log "generated development snapshot web page."
else
  log "test failures, no web snapshot generated."
fi

exit 0
## end