# HG changeset patch
# User kleing
# Date 1223536712 -7200
# Node ID bdb308737bfdefe3951021390d5ffeba4c923c7d
# Parent  3147236326ea7defe961903a03db44c5657d8947
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).

diff -r 3147236326ea -r bdb308737bfd Admin/isatest/isatest-annomaly
--- 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."
diff -r 3147236326ea -r bdb308737bfd Admin/isatest/isatest-check
--- 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
diff -r 3147236326ea -r bdb308737bfd Admin/isatest/isatest-doc
--- 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
 
diff -r 3147236326ea -r bdb308737bfd Admin/isatest/isatest-makeall
--- 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
 
diff -r 3147236326ea -r bdb308737bfd Admin/isatest/isatest-makedist
--- 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/*
diff -r 3147236326ea -r bdb308737bfd Admin/isatest/isatest-settings
--- 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