#!/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