do logging to MASTERLOG centrally (avoid multiple writers over NFS as
authorkleing
Thu Oct 09 09:18:32 2008 +0200 (2008-10-09)
changeset 28539bdb308737bfd
parent 28538 3147236326ea
child 28540 541366e3c1b3
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).
Admin/isatest/isatest-annomaly
Admin/isatest/isatest-check
Admin/isatest/isatest-doc
Admin/isatest/isatest-makeall
Admin/isatest/isatest-makedist
Admin/isatest/isatest-settings
     1.1 --- a/Admin/isatest/isatest-annomaly	Thu Oct 09 08:47:28 2008 +0200
     1.2 +++ b/Admin/isatest/isatest-annomaly	Thu Oct 09 09:18:32 2008 +0200
     1.3 @@ -34,7 +34,7 @@
     1.4  function fail()
     1.5  {
     1.6    echo "$1" >&2
     1.7 -  echo "$(date) $HOSTNAME $PRG: FAILED, $1" >> $MASTERLOG
     1.8 +  log "FAILED, $1"
     1.9    exit 2
    1.10  }
    1.11  
    1.12 @@ -89,4 +89,4 @@
    1.13  # grep -rl "$ISABELLE_HOME" . | xargs sed -i "s@$ISABELLE_HOME@\$ISABELLE_HOME@g"
    1.14  
    1.15  
    1.16 -echo "$(date) $HOSTNAME $PRG: annomaly docs generated successfully." >> $MASTERLOG
    1.17 +log "annomaly docs generated successfully."
     2.1 --- a/Admin/isatest/isatest-check	Thu Oct 09 08:47:28 2008 +0200
     2.2 +++ b/Admin/isatest/isatest-check	Thu Oct 09 09:18:32 2008 +0200
     2.3 @@ -98,9 +98,9 @@
     2.4  # (failures in experimental sessions ok)
     2.5  if [ "$FAIL"=="0" -a "$(echo $ERRORDIR/isatest*[^e].log)" == "$(echo)" ]; then
     2.6    (cd $HOME/devel-page; env DISTNAME=`$DISTPREFIX/Isabelle/bin/isabelle getenv -b ISABELLE_IDENTIFIER` make)
     2.7 -  echo "$(date) $HOSTNAME $PRG: generated development snapshot web page." >> $MASTERLOG
     2.8 +  log "generated development snapshot web page."
     2.9  else
    2.10 -  echo "$(date) $HOSTNAME $PRG: test failures, no web snapshot generated." >> $MASTERLOG
    2.11 +  log "test failures, no web snapshot generated."
    2.12  fi
    2.13  
    2.14  exit 0
     3.1 --- a/Admin/isatest/isatest-doc	Thu Oct 09 08:47:28 2008 +0200
     3.2 +++ b/Admin/isatest/isatest-doc	Thu Oct 09 09:18:32 2008 +0200
     3.3 @@ -59,7 +59,7 @@
     3.4  [ "$#" != "0" ] && usage
     3.5  
     3.6  if [ -f "$RUNNING/$SHORT.running" -o -e $ERRORLOG ]; then
     3.7 -  echo "$(date) $HOSTNAME $PRG: Skipped test. Isabelle devel version broken." >> $MASTERLOG
     3.8 +  log "Skipped test. Isabelle devel version broken."
     3.9    exit 1
    3.10  fi
    3.11  cat $SETTINGS >> $ISABELLE_DEVEL/etc/settings
    3.12 @@ -97,7 +97,7 @@
    3.13    echo >> $LOG
    3.14    echo "Failed sessions: ${FAIL}" >> $LOG
    3.15  
    3.16 -  echo "$(date) $HOSTNAME $PRG: doc test FAILED for ${FAIL}, elapsed time $ELAPSED." >> $MASTERLOG
    3.17 +  log "doc test FAILED for ${FAIL}, elapsed time $ELAPSED."
    3.18  
    3.19    cat > $TMP <<EOF
    3.20  Session(s) ${FAIL} in the documentation test failed (log attached).
    3.21 @@ -116,6 +116,6 @@
    3.22  
    3.23    exit 1
    3.24  else
    3.25 -  echo "$(date) $HOSTNAME $PRG: doc test successful, elapsed time $ELAPSED." >> $MASTERLOG
    3.26 +  log "doc test successful, elapsed time $ELAPSED."
    3.27  fi
    3.28  
     4.1 --- a/Admin/isatest/isatest-makeall	Thu Oct 09 08:47:28 2008 +0200
     4.2 +++ b/Admin/isatest/isatest-makeall	Thu Oct 09 09:18:32 2008 +0200
     4.3 @@ -32,7 +32,7 @@
     4.4  function fail()
     4.5  {
     4.6    echo "$1" >&2
     4.7 -  echo "$(date) $HOSTNAME $PRG: FAILED, $1" >> $MASTERLOG
     4.8 +  log "FAILED, $1"
     4.9    exit 2
    4.10  }
    4.11  
    4.12 @@ -160,9 +160,9 @@
    4.13  ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
    4.14  
    4.15  if [ -z "$FAIL" ]; then
    4.16 -    echo "$(date) $HOSTNAME $PRG: all tests successful, elapsed time $ELAPSED." >> $MASTERLOG
    4.17 +    log "all tests successful, elapsed time $ELAPSED."
    4.18  else
    4.19 -    echo "$(date) $HOSTNAME $PRG: targets ${FAIL}FAILED, elapsed time $ELAPSED." >> $MASTERLOG
    4.20 +    log "targets ${FAIL}FAILED, elapsed time $ELAPSED."
    4.21      exit 1
    4.22  fi
    4.23  
     5.1 --- a/Admin/isatest/isatest-makedist	Thu Oct 09 08:47:28 2008 +0200
     5.2 +++ b/Admin/isatest/isatest-makedist	Thu Oct 09 09:18:32 2008 +0200
     5.3 @@ -67,7 +67,7 @@
     5.4  then
     5.5      echo ------------------- DIST BUILD FAILED --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
     5.6      ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
     5.7 -    echo "$(date) $HOSTNAME $PRG: dist build FAILED, elapsed time $ELAPSED." >> $MASTERLOG
     5.8 +    log "dist build FAILED, elapsed time $ELAPSED."
     5.9  
    5.10      echo "Could not build isabelle distribution. Log file available at" > $TMP
    5.11      echo "$HOSTNAME:$DISTLOG" >> $TMP
    5.12 @@ -87,7 +87,7 @@
    5.13  echo ------------------- prepared test successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
    5.14  
    5.15  ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
    5.16 -echo "$(date) $HOSTNAME $PRG: dist build successful, elapsed time $ELAPSED." >> $MASTERLOG
    5.17 +log "dist build successful, elapsed time $ELAPSED."
    5.18  
    5.19  ## clean up var/running
    5.20  rm -f $RUNNING/*
     6.1 --- a/Admin/isatest/isatest-settings	Thu Oct 09 08:47:28 2008 +0200
     6.2 +++ b/Admin/isatest/isatest-settings	Thu Oct 09 09:18:32 2008 +0200
     6.3 @@ -15,6 +15,7 @@
     6.4  
     6.5  LOGPREFIX=$HOME/log
     6.6  MASTERLOG=$LOGPREFIX/isatest.log
     6.7 +LOGSERVER=macbroy23.informatik.tu-muenchen.de
     6.8  
     6.9  ERRORDIR=$HOME/var
    6.10  ERRORLOG=$ERRORDIR/error.log
    6.11 @@ -22,3 +23,14 @@
    6.12  RUNNING=$HOME/var/running
    6.13  
    6.14  DISTPREFIX=$HOME/tmp/isadist
    6.15 +
    6.16 +# this function avoids NFS inconsistencies with multiple writers by
    6.17 +# sshing to one central machine and writing locally. There is stil a
    6.18 +# race condition, but at least it should not corrupt a whole set of entries
    6.19 +# any more.
    6.20 +function log()
    6.21 +{
    6.22 +  MSG="$1"
    6.23 +  TIMESTAMP="$(date)"
    6.24 +  echo "[$TIMESTAMP $HOSTNAME $PRG]: $MSG" | ssh $LOGSERVER "cat >> $MASTERLOG"
    6.25 +}
    6.26 \ No newline at end of file