build

lucas - fixed bug with name capture variables bound outside redex could (previously)conflict with scheme variables that occur in the conditions of an equation, and which were renamed to avoid conflict with another instantiation. This has now been fixed.

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


## global settings

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


## settings

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

export THIS_IS_ISABELLE_BUILD=true
ISABELLE_HOME="$(dirname "$0")"
. "$ISABELLE_HOME/lib/scripts/getsettings" || \
  { echo "$PRG probably not called from its original place!"; 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:p: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"
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
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"