minimal test of current repository version;
authorwenzelm
Sat Nov 21 14:03:36 2009 +0100 (2009-11-21)
changeset 3383138507aef93cd
parent 33830 1b634d37aa64
child 33832 cff42395c246
minimal test of current repository version;
Admin/isatest/minimal-test
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/Admin/isatest/minimal-test	Sat Nov 21 14:03:36 2009 +0100
     1.3 @@ -0,0 +1,59 @@
     1.4 +#!/usr/bin/env bash
     1.5 +#
     1.6 +# Author: Makarius
     1.7 +#
     1.8 +# DESCRIPTION: minimal test of current repository version
     1.9 +
    1.10 +## global settings
    1.11 +
    1.12 +MAXTIME=14400
    1.13 +
    1.14 +DATE=$(date "+%Y-%m-%d_%H:%M")
    1.15 +HOST=$(hostname -s)
    1.16 +
    1.17 +LOGDIR="$HOME/log"
    1.18 +LOG="$LOGDIR/test-${DATE}-${HOST}.log"
    1.19 +
    1.20 +TEST_NAME="minimal-test@${HOST}"
    1.21 +PUBLISH_TEST="/home/isabelle-repository/repos/testtool/publish_test.py"
    1.22 +
    1.23 +
    1.24 +## diagnostics
    1.25 +
    1.26 +function fail()
    1.27 +{
    1.28 +  echo "$1" >&2
    1.29 +  exit 2
    1.30 +}
    1.31 +
    1.32 +
    1.33 +## main
    1.34 +
    1.35 +mkdir -p "$LOGDIR" || fail "Bad log directory: $LOGDIR"
    1.36 +
    1.37 +[ -z "$ISABELLE_HOME" -o -z "$ISABELLE_TOOL" ] && fail "Bad Isabelle environment"
    1.38 +
    1.39 +cd "$ISABELLE_HOME"
    1.40 +
    1.41 +hg pull -u || fail "Bad repository: $PWD"
    1.42 +IDENT="$(hg parent --template "{node|short}")"
    1.43 +
    1.44 +(
    1.45 +  ulimit -t "$MAXTIME"
    1.46 +
    1.47 +  echo -n "hg id: "; hg id
    1.48 +  "$ISABELLE_TOOL" makeall clean
    1.49 +  "$ISABELLE_TOOL" makeall all -k
    1.50 +  exit "$?"
    1.51 +) > "$LOG" 2>&1
    1.52 +
    1.53 +if [ "$?" -eq 0 ]; then
    1.54 +  [ -x "$PUBLISH_TEST" ] && \
    1.55 +    "$PUBLISH_TEST" -r "$IDENT" -s SUCCESS -a log "$LOG" -n "$TEST_NAME"
    1.56 +  gzip -f "$LOG"
    1.57 +else
    1.58 +  [ -x "$PUBLISH_TEST" ] && \
    1.59 +    "$PUBLISH_TEST" -r "$IDENT" -s FAIL -a log "$LOG" -n "$TEST_NAME"
    1.60 +  fail "Minimal test failed, see $LOG"
    1.61 +fi
    1.62 +