Admin/isatest/minimal-test

abandoned import of isatest reports into (old version of) mira -- unstable, and not worth the maintenance effort

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