author | wenzelm |
Sat, 04 Oct 2008 17:40:56 +0200 | |
changeset 28504 | 7ad7d7d6df47 |
parent 28500 | 4b79e5d3d0aa |
child 28527 | 82b36daff4c1 |
permissions | -rwxr-xr-x |
kleing@22410 | 1 |
#!/usr/bin/env bash |
kleing@22410 | 2 |
# |
kleing@22410 | 3 |
# $Id$ |
kleing@22410 | 4 |
# Author: Gerwin Klein, TU Muenchen |
kleing@22410 | 5 |
# |
wenzelm@28504 | 6 |
# DESCRIPTION: Run isabelle makeall from specified distribution and settings. |
kleing@22410 | 7 |
|
kleing@22410 | 8 |
## global settings |
kleing@22411 | 9 |
. ~/admin/isatest/isatest-settings |
kleing@22410 | 10 |
|
kleing@22410 | 11 |
# max time until test is aborted (in sec) |
kleing@22410 | 12 |
MAXTIME=28800 |
kleing@22410 | 13 |
|
kleing@22410 | 14 |
## diagnostics |
kleing@22410 | 15 |
|
kleing@22410 | 16 |
PRG="$(basename "$0")" |
kleing@22410 | 17 |
|
kleing@22410 | 18 |
function usage() |
kleing@22410 | 19 |
{ |
kleing@22410 | 20 |
echo |
kleing@24753 | 21 |
echo "Usage: $PRG [-l logic targets] settings1 [settings2 ...]" |
kleing@22410 | 22 |
echo |
wenzelm@28504 | 23 |
echo " Runs isabelle makeall for specified settings." |
kleing@22410 | 24 |
echo " Leaves messages in ${ERRORLOG} and ${LOGPREFIX} if it fails." |
kleing@22410 | 25 |
echo |
kleing@24753 | 26 |
echo "Examples:" |
kleing@24753 | 27 |
echo " $PRG ~/settings/at-poly ~/settings/at-sml" |
kleing@24753 | 28 |
echo " $PRG -l HOL \"HOL-Library HOL-Bali\" ~/settings/at-poly" |
kleing@22410 | 29 |
exit 1 |
kleing@22410 | 30 |
} |
kleing@22410 | 31 |
|
kleing@22410 | 32 |
function fail() |
kleing@22410 | 33 |
{ |
kleing@22410 | 34 |
echo "$1" >&2 |
kleing@22410 | 35 |
echo "$(date) $HOSTNAME $PRG: FAILED, $1" >> $MASTERLOG |
kleing@22410 | 36 |
exit 2 |
kleing@22410 | 37 |
} |
kleing@22410 | 38 |
|
kleing@22410 | 39 |
## main |
kleing@22410 | 40 |
|
kleing@22410 | 41 |
# argument checking |
kleing@22410 | 42 |
|
kleing@22410 | 43 |
[ "$1" = "-?" ] && usage |
kleing@22410 | 44 |
[ "$#" -lt "1" ] && usage |
kleing@22410 | 45 |
|
kleing@22410 | 46 |
[ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory." |
kleing@22410 | 47 |
|
kleing@22410 | 48 |
# make file flags and nice setup for different target platforms |
kleing@22410 | 49 |
case $HOSTNAME in |
kleing@22410 | 50 |
atbroy51) |
kleing@22410 | 51 |
MFLAGS="-j 2" |
kleing@22410 | 52 |
NICE="" |
kleing@22410 | 53 |
;; |
kleing@22410 | 54 |
|
isatest@24758 | 55 |
atbroy98) |
wenzelm@26369 | 56 |
MFLAGS="" |
wenzelm@26369 | 57 |
NICE="" |
wenzelm@26369 | 58 |
;; |
isatest@24647 | 59 |
|
kleing@22410 | 60 |
atbroy31) |
wenzelm@26369 | 61 |
MFLAGS="-j 2" |
kleing@22410 | 62 |
;; |
kleing@22410 | 63 |
|
kleing@22410 | 64 |
sunbroy2) |
kleing@22410 | 65 |
MFLAGS="-j 6" |
kleing@22410 | 66 |
NICE="nice" |
kleing@22410 | 67 |
;; |
kleing@22410 | 68 |
|
kleing@22410 | 69 |
sunbroy1) |
kleing@22410 | 70 |
MFLAGS="-j 2" |
kleing@22410 | 71 |
NICE="nice" |
kleing@22410 | 72 |
;; |
kleing@22410 | 73 |
|
kleing@22410 | 74 |
macbroy5) |
wenzelm@23415 | 75 |
MFLAGS="-j 2" |
kleing@22410 | 76 |
NICE="" |
kleing@22410 | 77 |
;; |
kleing@22410 | 78 |
|
wenzelm@26369 | 79 |
macbroy2[0-9]) |
wenzelm@26369 | 80 |
MFLAGS="-j 2" |
wenzelm@26369 | 81 |
NICE="" |
wenzelm@26369 | 82 |
;; |
wenzelm@26369 | 83 |
|
kleing@22410 | 84 |
*) |
kleing@22410 | 85 |
MFLAGS="" |
kleing@22410 | 86 |
# be nice by default |
kleing@22410 | 87 |
NICE=nice |
kleing@22410 | 88 |
;; |
kleing@22410 | 89 |
esac |
kleing@22410 | 90 |
|
wenzelm@28504 | 91 |
ISABELLE_TOOL="$DISTPREFIX/Isabelle/bin/isabelle" |
kleing@24753 | 92 |
|
wenzelm@28500 | 93 |
[ -x $ISABELLE_TOOL ] || fail "Cannot run $ISABELLE_TOOL" |
kleing@24753 | 94 |
|
kleing@24753 | 95 |
if [ "$1" = "-l" ]; then |
kleing@24753 | 96 |
shift |
kleing@24753 | 97 |
[ "$#" -lt "3" ] && usage |
kleing@24753 | 98 |
LOGIC="$1" |
kleing@24753 | 99 |
TARGETS="$2" |
kleing@24753 | 100 |
shift 2 |
wenzelm@28500 | 101 |
ISABELLE_HOME="$($ISABELLE_TOOL getenv -b ISABELLE_HOME)" |
isatest@24786 | 102 |
DIR="$ISABELLE_HOME/src/$LOGIC" |
wenzelm@28500 | 103 |
TOOL="$ISABELLE_TOOL make $MFLAGS $TARGETS" |
kleing@24753 | 104 |
else |
isatest@24781 | 105 |
DIR="." |
wenzelm@28500 | 106 |
TOOL="$ISABELLE_TOOL makeall $MFLAGS all" |
kleing@24753 | 107 |
fi |
kleing@24753 | 108 |
|
kleing@22410 | 109 |
# main test loop |
kleing@22410 | 110 |
|
kleing@22410 | 111 |
for SETTINGS in $@; do |
kleing@22410 | 112 |
|
kleing@22410 | 113 |
[ -r $SETTINGS ] || fail "Cannot read $SETTINGS." |
kleing@22410 | 114 |
|
kleing@22410 | 115 |
# logfile setup |
kleing@22410 | 116 |
|
kleing@22410 | 117 |
DATE=$(date "+%Y-%m-%d") |
kleing@22410 | 118 |
SHORT=${SETTINGS##*/} |
kleing@22410 | 119 |
TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log |
kleing@22410 | 120 |
|
kleing@22410 | 121 |
# the test |
kleing@22410 | 122 |
|
kleing@22410 | 123 |
touch $RUNNING/$SHORT.running |
kleing@22410 | 124 |
|
kleing@22410 | 125 |
echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1 |
kleing@22410 | 126 |
|
kleing@22410 | 127 |
cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings |
isatest@24781 | 128 |
(ulimit -t $MAXTIME; cd $DIR; $NICE $TOOL >> $TESTLOG 2>&1) |
kleing@22410 | 129 |
|
kleing@22410 | 130 |
if [ $? -eq 0 ] |
kleing@22410 | 131 |
then |
kleing@22410 | 132 |
# test log and cleanup |
kleing@22410 | 133 |
echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1 |
kleing@22410 | 134 |
gzip -f $TESTLOG |
kleing@22410 | 135 |
else |
kleing@22410 | 136 |
# test log |
kleing@22410 | 137 |
echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1 |
kleing@22410 | 138 |
|
kleing@22410 | 139 |
# error log |
kleing@22410 | 140 |
echo "Test for platform ${SHORT} failed. Log file attached." >> $ERRORLOG |
kleing@22410 | 141 |
echo "[...]" >> $ERRORLOG |
kleing@22410 | 142 |
tail -3 $TESTLOG >> $ERRORLOG |
kleing@22410 | 143 |
echo >> $ERRORLOG |
kleing@22410 | 144 |
|
kleing@22410 | 145 |
FAIL="$FAIL$SHORT " |
kleing@22410 | 146 |
(cd $ERRORDIR; ln -s $TESTLOG) |
kleing@22410 | 147 |
fi |
kleing@22410 | 148 |
|
kleing@22410 | 149 |
rm -f $RUNNING/$SHORT.running |
kleing@22410 | 150 |
done |
kleing@22410 | 151 |
|
kleing@22410 | 152 |
# time and success/failure to master log |
kleing@22410 | 153 |
ELAPSED=$("$HOME/bin/showtime" "$SECONDS") |
kleing@22410 | 154 |
|
kleing@22410 | 155 |
if [ -z "$FAIL" ]; then |
kleing@22410 | 156 |
echo "$(date) $HOSTNAME $PRG: all tests successful, elapsed time $ELAPSED." >> $MASTERLOG |
kleing@22410 | 157 |
else |
kleing@22410 | 158 |
echo "$(date) $HOSTNAME $PRG: targets ${FAIL}FAILED, elapsed time $ELAPSED." >> $MASTERLOG |
kleing@22410 | 159 |
exit 1 |
kleing@22410 | 160 |
fi |
kleing@22410 | 161 |
|
kleing@22410 | 162 |
# end |