build

Optimized proofs.

#!/bin/bash -norc
#
# $Id$
#
# build - compile parts of the Isabelle system

## args

LOGICS="$*"


## settings

PRG=$(basename $0)

ISABELLE_HOME=$(dirname $0)
. $ISABELLE_HOME/lib/scripts/getsettings || \
  { echo "$PRG probably not called from its original place!"; exit 2 }


## tell the user about current values

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 are appropriate."
echo "Your current values are:"
echo

echo "ML_SYSTEM=$ML_SYSTEM"
echo "ML_HOME=$ML_HOME"
echo "ML_OPTIONS=$ML_OPTIONS"


## build it

LOGICS="Pure $DEFAULT_LOGIC $LOGICS"

echo
echo
echo "Press RETURN to start compilation of: $LOGICS"
read


export THIS_IS_ISABELLE_BUILD=true

for DIR in $LOGICS
do
  ( cd $ISABELLE_HOME/src/$DIR; $ISATOOL make)
done