#!/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"
PUBLISH_TEST="/home/isabelle-repository/repos/testtool/publish_test.py"
## 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
[ -x "$PUBLISH_TEST" ] && \
"$PUBLISH_TEST" -r "$IDENT" -s SUCCESS -a log "$LOG" -n "$TEST_NAME"
gzip -f "$LOG"
else
[ -x "$PUBLISH_TEST" ] && \
"$PUBLISH_TEST" -r "$IDENT" -s FAIL -a log "$LOG" -n "$TEST_NAME"
fail "Minimal test failed, see $LOG"
fi