Admin/isatest/minimal-test

adding termination proofs to series functions in LSC; commenting out momentarily unused term refinement functions in LSC

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