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"