--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/isatest/minimal-test Sat Nov 21 14:03:36 2009 +0100
@@ -0,0 +1,59 @@
+#!/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@${HOST}"
+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
+