--- a/Admin/isatest/isatest-makeall Sat Jul 14 21:05:29 2012 +0200
+++ b/Admin/isatest/isatest-makeall Sat Jul 14 21:15:41 2012 +0200
@@ -10,6 +10,7 @@
# max time until test is aborted (in sec)
MAXTIME=28800
+
## diagnostics
PRG="$(basename "$0")"
@@ -35,6 +36,7 @@
exit 2
}
+
## main
# argument checking
@@ -47,61 +49,17 @@
TARGETS=all
# make file flags and nice setup for different target platforms
+MFLAGS="-k"
+NICE="nice"
case $HOSTNAME in
- atbroy51)
- MFLAGS="-k -j 2"
- NICE=""
- ;;
-
- atbroy98)
- MFLAGS="-k"
- NICE=""
- ;;
-
- atbroy31)
- MFLAGS="-k -j 2"
- ;;
-
- macbroy2)
- MFLAGS="-k"
+ macbroy2 | macbroy6 | macbroy30)
NICE=""
;;
-
- macbroy6)
- MFLAGS="-k"
- NICE=""
- ;;
-
- macbroy22)
- MFLAGS="-k"
- NICE=""
- ;;
-
- macbroy27 | macbroy28)
- MFLAGS="-k -j 2"
- NICE="nice"
- ;;
-
- macbroy2[0-9])
- MFLAGS="-k -j 2"
- NICE=""
- ;;
-
- macbroy30)
- MFLAGS="-k"
- NICE=""
- ;;
-
lxbroy[234])
MFLAGS="-k -j 2"
NICE=""
;;
- *)
- MFLAGS="-k"
- # be nice by default
- NICE=nice
- ;;
esac
ISABELLE_TOOL="$DISTPREFIX/Isabelle/bin/isabelle"
@@ -129,6 +87,7 @@
IDENT=$(cat "$DISTPREFIX/ISABELLE_IDENT")
+
# main test loop
log "starting [$@]"
@@ -142,13 +101,13 @@
DATE=$(date "+%Y-%m-%d")
SHORT=${SETTINGS##*/}
- if [ "${SHORT%-e}" == "$SHORT" ]; then
- # normal test
- TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log
- else
- # experimental test
- TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME-e.log
- fi
+ if [ "${SHORT%-e}" == "$SHORT" ]; then
+ # normal test
+ TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log
+ else
+ # experimental test
+ TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME-e.log
+ fi
# the test
@@ -199,4 +158,3 @@
exit 1
fi
-# end
--- a/Admin/isatest/isatest-makedist Sat Jul 14 21:05:29 2012 +0200
+++ b/Admin/isatest/isatest-makedist Sat Jul 14 21:15:41 2012 +0200
@@ -16,6 +16,7 @@
SSH="ssh -f"
+
## diagnostics
PRG="$(basename "$0")"
@@ -36,6 +37,7 @@
exit 2
}
+
## main
# cleanup old error log and test-still-running files
@@ -89,16 +91,21 @@
ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
log "dist build successful, elapsed time $ELAPSED."
+
## clean up var/running
rm -f $RUNNING/*
mkdir -p $RUNNING
+
## spawn test runs
-$SSH lxbroy2 "$MAKEALL $HOME/settings/at-poly; $MAKEALL $HOME/settings/at-poly-test"
-# give test some time to copy settings and start
+$SSH lxbroy2 "
+ $MAKEALL $HOME/settings/at-poly;
+ $MAKEALL $HOME/settings/at-poly-test"
sleep 15
-$SSH lxbroy3 "$MAKEALL $HOME/settings/at64-poly; $MAKEALL -l HOL HOL-Library $HOME/settings/at-sml-dev-e"
+$SSH lxbroy3 "
+ $MAKEALL $HOME/settings/at64-poly;
+ $MAKEALL -l HOL HOL-Library $HOME/settings/at-sml-dev-e"
sleep 15
$SSH macbroy23 "$MAKEALL $HOME/settings/at-poly-e"
sleep 15
@@ -112,11 +119,7 @@
sleep 15
$SSH macbroy30 "sleep 10800; $MAKEALL $HOME/settings/mac-poly-M2"
-#sleep 15
-#$SSH atbroy51 "$HOME/admin/isatest/isatest-annomaly"
-
echo ------------------- spawned tests successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
gzip -f $DISTLOG
-## end