Admin/isatest/minimal-test
author berghofe
Mon, 23 Jul 2012 18:52:10 +0200
changeset 48453 2421ff8c57a5
parent 48212 cccc92c0addc
permissions -rwxr-xr-x
set_vcs now derives prefix from fully qualified procedure / function name

#!/usr/bin/env bash
#
# Author: Makarius
#
# DESCRIPTION: minimal test of current repository version

## global settings

MAXTIME=14400

DATE=$(date "+%Y-%m-%d_%H:%M")
HOST=$(hostname -s)

LOGDIR="$HOME/log"
LOG="$LOGDIR/test-${DATE}-${HOST}.log"

TEST_NAME="minimal-test"


## diagnostics

function fail()
{
  echo "$1" >&2
  exit 2
}


## main

mkdir -p "$LOGDIR" || fail "Bad log directory: $LOGDIR"

[ -z "$ISABELLE_HOME" -o -z "$ISABELLE_TOOL" ] && fail "Bad Isabelle environment"

cd "$ISABELLE_HOME"

hg pull -u || fail "Bad repository: $PWD"
IDENT="$(hg parent --template "{node|short}")"

(
  ulimit -t "$MAXTIME"

  echo -n "hg id: "; hg id
  "$ISABELLE_TOOL" makeall clean
  "$ISABELLE_TOOL" makeall all -k
  exit "$?"
) > "$LOG" 2>&1

if [ "$?" -eq 0 ]; then
  gzip -f "$LOG"
else
  fail "Minimal test failed, see $LOG"
fi