Admin/isatest/minimal-test
author blanchet
Wed, 08 Dec 2010 22:18:37 +0100
changeset 41093 dfbc8759415f
parent 33859 033ce4cafba6
child 48212 cccc92c0addc
permissions -rwxr-xr-x
lower fudge factor
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33831
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
     2
#
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
     3
# Author: Makarius
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
     4
#
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
     5
# DESCRIPTION: minimal test of current repository version
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
     6
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
     7
## global settings
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
     8
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
     9
MAXTIME=14400
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    10
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    11
DATE=$(date "+%Y-%m-%d_%H:%M")
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    12
HOST=$(hostname -s)
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    13
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    14
LOGDIR="$HOME/log"
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    15
LOG="$LOGDIR/test-${DATE}-${HOST}.log"
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    16
33859
033ce4cafba6 do not add host suffix -- it is appended by test framework
krauss
parents: 33831
diff changeset
    17
TEST_NAME="minimal-test"
33831
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    18
PUBLISH_TEST="/home/isabelle-repository/repos/testtool/publish_test.py"
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    19
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    20
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    21
## diagnostics
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    22
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    23
function fail()
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    24
{
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    25
  echo "$1" >&2
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    26
  exit 2
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    27
}
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    28
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    29
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    30
## main
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    31
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    32
mkdir -p "$LOGDIR" || fail "Bad log directory: $LOGDIR"
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    33
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    34
[ -z "$ISABELLE_HOME" -o -z "$ISABELLE_TOOL" ] && fail "Bad Isabelle environment"
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    35
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    36
cd "$ISABELLE_HOME"
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    37
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    38
hg pull -u || fail "Bad repository: $PWD"
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    39
IDENT="$(hg parent --template "{node|short}")"
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    40
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    41
(
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    42
  ulimit -t "$MAXTIME"
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    43
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    44
  echo -n "hg id: "; hg id
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    45
  "$ISABELLE_TOOL" makeall clean
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    46
  "$ISABELLE_TOOL" makeall all -k
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    47
  exit "$?"
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    48
) > "$LOG" 2>&1
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    49
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    50
if [ "$?" -eq 0 ]; then
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    51
  [ -x "$PUBLISH_TEST" ] && \
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    52
    "$PUBLISH_TEST" -r "$IDENT" -s SUCCESS -a log "$LOG" -n "$TEST_NAME"
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    53
  gzip -f "$LOG"
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    54
else
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    55
  [ -x "$PUBLISH_TEST" ] && \
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    56
    "$PUBLISH_TEST" -r "$IDENT" -s FAIL -a log "$LOG" -n "$TEST_NAME"
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    57
  fail "Minimal test failed, see $LOG"
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    58
fi
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    59