do logging to MASTERLOG centrally (avoid multiple writers over NFS as
this tends to corrupt the log file if not mounted with -sync option
which apparently is not the default any more).
--- a/Admin/isatest/isatest-annomaly Thu Oct 09 08:47:28 2008 +0200
+++ b/Admin/isatest/isatest-annomaly Thu Oct 09 09:18:32 2008 +0200
@@ -34,7 +34,7 @@
function fail()
{
echo "$1" >&2
- echo "$(date) $HOSTNAME $PRG: FAILED, $1" >> $MASTERLOG
+ log "FAILED, $1"
exit 2
}
@@ -89,4 +89,4 @@
# grep -rl "$ISABELLE_HOME" . | xargs sed -i "s@$ISABELLE_HOME@\$ISABELLE_HOME@g"
-echo "$(date) $HOSTNAME $PRG: annomaly docs generated successfully." >> $MASTERLOG
+log "annomaly docs generated successfully."
--- a/Admin/isatest/isatest-check Thu Oct 09 08:47:28 2008 +0200
+++ b/Admin/isatest/isatest-check Thu Oct 09 09:18:32 2008 +0200
@@ -98,9 +98,9 @@
# (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)
- echo "$(date) $HOSTNAME $PRG: generated development snapshot web page." >> $MASTERLOG
+ log "generated development snapshot web page."
else
- echo "$(date) $HOSTNAME $PRG: test failures, no web snapshot generated." >> $MASTERLOG
+ log "test failures, no web snapshot generated."
fi
exit 0
--- a/Admin/isatest/isatest-doc Thu Oct 09 08:47:28 2008 +0200
+++ b/Admin/isatest/isatest-doc Thu Oct 09 09:18:32 2008 +0200
@@ -59,7 +59,7 @@
[ "$#" != "0" ] && usage
if [ -f "$RUNNING/$SHORT.running" -o -e $ERRORLOG ]; then
- echo "$(date) $HOSTNAME $PRG: Skipped test. Isabelle devel version broken." >> $MASTERLOG
+ log "Skipped test. Isabelle devel version broken."
exit 1
fi
cat $SETTINGS >> $ISABELLE_DEVEL/etc/settings
@@ -97,7 +97,7 @@
echo >> $LOG
echo "Failed sessions: ${FAIL}" >> $LOG
- echo "$(date) $HOSTNAME $PRG: doc test FAILED for ${FAIL}, elapsed time $ELAPSED." >> $MASTERLOG
+ log "doc test FAILED for ${FAIL}, elapsed time $ELAPSED."
cat > $TMP <<EOF
Session(s) ${FAIL} in the documentation test failed (log attached).
@@ -116,6 +116,6 @@
exit 1
else
- echo "$(date) $HOSTNAME $PRG: doc test successful, elapsed time $ELAPSED." >> $MASTERLOG
+ log "doc test successful, elapsed time $ELAPSED."
fi
--- a/Admin/isatest/isatest-makeall Thu Oct 09 08:47:28 2008 +0200
+++ b/Admin/isatest/isatest-makeall Thu Oct 09 09:18:32 2008 +0200
@@ -32,7 +32,7 @@
function fail()
{
echo "$1" >&2
- echo "$(date) $HOSTNAME $PRG: FAILED, $1" >> $MASTERLOG
+ log "FAILED, $1"
exit 2
}
@@ -160,9 +160,9 @@
ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
if [ -z "$FAIL" ]; then
- echo "$(date) $HOSTNAME $PRG: all tests successful, elapsed time $ELAPSED." >> $MASTERLOG
+ log "all tests successful, elapsed time $ELAPSED."
else
- echo "$(date) $HOSTNAME $PRG: targets ${FAIL}FAILED, elapsed time $ELAPSED." >> $MASTERLOG
+ log "targets ${FAIL}FAILED, elapsed time $ELAPSED."
exit 1
fi
--- a/Admin/isatest/isatest-makedist Thu Oct 09 08:47:28 2008 +0200
+++ b/Admin/isatest/isatest-makedist Thu Oct 09 09:18:32 2008 +0200
@@ -67,7 +67,7 @@
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
+ log "dist build FAILED, elapsed time $ELAPSED."
echo "Could not build isabelle distribution. Log file available at" > $TMP
echo "$HOSTNAME:$DISTLOG" >> $TMP
@@ -87,7 +87,7 @@
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
+log "dist build successful, elapsed time $ELAPSED."
## clean up var/running
rm -f $RUNNING/*
--- a/Admin/isatest/isatest-settings Thu Oct 09 08:47:28 2008 +0200
+++ b/Admin/isatest/isatest-settings Thu Oct 09 09:18:32 2008 +0200
@@ -15,6 +15,7 @@
LOGPREFIX=$HOME/log
MASTERLOG=$LOGPREFIX/isatest.log
+LOGSERVER=macbroy23.informatik.tu-muenchen.de
ERRORDIR=$HOME/var
ERRORLOG=$ERRORDIR/error.log
@@ -22,3 +23,14 @@
RUNNING=$HOME/var/running
DISTPREFIX=$HOME/tmp/isadist
+
+# this function avoids NFS inconsistencies with multiple writers by
+# sshing to one central machine and writing locally. There is stil a
+# race condition, but at least it should not corrupt a whole set of entries
+# any more.
+function log()
+{
+ MSG="$1"
+ TIMESTAMP="$(date)"
+ echo "[$TIMESTAMP $HOSTNAME $PRG]: $MSG" | ssh $LOGSERVER "cat >> $MASTERLOG"
+}
\ No newline at end of file