build

Added several new functions that are used to prove HOL goals. Added new methods "vampireH" and "eproverH" that can prove both FOL and HOL goals. The old "vampire" and "eprover" methods are renamed to "vampireF" and "eproverF"; they can only prove FOL goals.

#!/usr/bin/env bash
#
# $Id$
# Author: Markus Wenzel, TU Muenchen
#
# build - compile the Isabelle system and object-logics

if [ -L "$0" ]; then
  TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
  exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
fi


## global settings

ALL_LOGICS="Pure FOL HOL ZF CCL CTT Cube FOLP HOLCF LCF Sequents"


## settings

export THIS_IS_ISABELLE_BUILD=true

PRG="$(basename "$0")"

ISABELLE_HOME="$(cd "$(dirname "$0")"; pwd -P)"
source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2


## diagnostics

function usage()
{
  echo
  echo "Usage: $PRG [OPTIONS] [LOGICS ...]"
  echo
  echo "  Options are:"
  echo "    -a           all logics"
  echo "    -b           batch mode"
  echo "    -i           make images"
  echo "    -m TARGET    make this target"
  echo "    -t           make test"
  echo
  echo "  Compile the named LOGICS (default $ISABELLE_LOGIC), or all object logics"
  echo "  in the distribution."
  echo
  exit 1
}

function fail()
{
  echo "$1" >&2
  exit 2
}


## process command line

# options

ALL=""
BATCH=""
TARGETS=""

while getopts "abim:t" OPT
do
  case "$OPT" in
    a)
      ALL=true
      ;;
    b)
      BATCH=true
      ;;
    i)
      TARGETS="$TARGETS images"
      ;;
    m)
      TARGETS="$TARGETS $OPTARG"
      ;;
    t)
      TARGETS="$TARGETS test"
      ;;
    \?)
      usage
      ;;
  esac
done

shift $(($OPTIND - 1))


# args

LOGICS="$@"

[ -n "$ALL" ] && LOGICS="$LOGICS $ALL_LOGICS"
[ -z "$LOGICS" ] && LOGICS="$ISABELLE_LOGIC"


## main

# tell the user about current values

if [ -z "$BATCH" ]; then
  echo
  echo "                *****************************"
  echo "                * Welcome to Isabelle build *"
  echo "                *****************************"
  echo
  echo "Please check $ISABELLE_HOME/etc/settings"
  [ -f "$ISABELLE_HOME_USER/etc/settings" ] && echo "AND $ISABELLE_HOME_USER/etc/settings"
  echo "to make sure that Isabelle's ML system settings and compilation options"
  echo "are appropriate."
  echo
  echo "The current values are:"
  echo
  echo "  ML_SYSTEM=$ML_SYSTEM"
  echo "  ML_HOME=$ML_HOME"
  echo "  ML_OPTIONS=$ML_OPTIONS"
  echo "  ML_PLATFORM=$ML_PLATFORM"
  echo
  echo "  ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
  echo "  HOL_USEDIR_OPTIONS=$HOL_USEDIR_OPTIONS"
fi


# check logics

if [ -z "$BATCH" ]; then
  echo
  echo
  echo "Press RETURN to compilation of"
  echo
fi


MAKE_LOGICS=""

for L in $LOGICS
do
  DIR="$ISABELLE_HOME/src/$L"
  if [ -f "$DIR/IsaMakefile" ]; then
    MAKE_LOGICS="$MAKE_LOGICS $L"
  else
    echo "No such logic: $L"
  fi
done


if [ -z "$BATCH" ]; then
  echo " $MAKE_LOGICS"
  [ -n "$TARGETS" ] && echo "  (targets:$TARGETS)"
  echo
  read
else
  echo
  echo "Isabelle build: $MAKE_LOGICS"
  [ -n "$TARGETS" ] && echo "(targets:$TARGETS)"
  echo
  echo "ML_SYSTEM=$ML_SYSTEM"
  echo "ML_HOME=$ML_HOME"
  echo "ML_OPTIONS=$ML_OPTIONS"
  echo "ML_PLATFORM=$ML_PLATFORM"
  echo
  echo "ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
  echo "HOL_USEDIR_OPTIONS=$HOL_USEDIR_OPTIONS"
  echo
fi


# build it

SECONDS=0
echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"

for L in $MAKE_LOGICS
do
  ( cd "$ISABELLE_HOME/src/$L"; "$ISATOOL" make $TARGETS )
done

echo -n "Finished at "; date

ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS")
echo "$ELAPSED total elapsed time"