Admin/isatest/minimal-test
author wenzelm
Thu, 26 Jul 2012 17:17:53 +0200
changeset 48520 6d4ea2efa64b
parent 48212 cccc92c0addc
permissions -rwxr-xr-x
more build options;
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
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    19
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    20
## diagnostics
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    21
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    22
function fail()
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    23
{
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    24
  echo "$1" >&2
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    25
  exit 2
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    26
}
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
## main
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    30
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    31
mkdir -p "$LOGDIR" || fail "Bad log directory: $LOGDIR"
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    32
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    33
[ -z "$ISABELLE_HOME" -o -z "$ISABELLE_TOOL" ] && fail "Bad Isabelle environment"
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    34
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    35
cd "$ISABELLE_HOME"
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    36
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    37
hg pull -u || fail "Bad repository: $PWD"
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    38
IDENT="$(hg parent --template "{node|short}")"
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    39
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    40
(
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    41
  ulimit -t "$MAXTIME"
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    42
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    43
  echo -n "hg id: "; hg id
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    44
  "$ISABELLE_TOOL" makeall clean
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    45
  "$ISABELLE_TOOL" makeall all -k
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    46
  exit "$?"
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    47
) > "$LOG" 2>&1
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    48
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    49
if [ "$?" -eq 0 ]; then
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    50
  gzip -f "$LOG"
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    51
else
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    52
  fail "Minimal test failed, see $LOG"
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    53
fi
38507aef93cd minimal test of current repository version;
wenzelm
parents:
diff changeset
    54