# HG changeset patch
# User wenzelm
# Date 1258808616 -3600
# Node ID 38507aef93cd1f2e93938647738eb120eb73c27c
# Parent  1b634d37aa64a76393b1f350895b442de2aadaac
minimal test of current repository version;

diff -r 1b634d37aa64 -r 38507aef93cd Admin/isatest/minimal-test
--- /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
+