build
author wenzelm
Wed Apr 02 19:12:26 1997 +0200 (1997-04-02)
changeset 2879 477bfcb022d8
parent 2789 69cf3aea45ee
child 2902 bacef535265c
permissions -rwxr-xr-x
misc improvements;
wenzelm@2755
     1
#!/bin/bash -norc
wenzelm@2755
     2
#
wenzelm@2755
     3
# $Id$
wenzelm@2755
     4
#
wenzelm@2755
     5
# build - compile parts of the Isabelle system
wenzelm@2755
     6
wenzelm@2755
     7
wenzelm@2789
     8
## settings
wenzelm@2789
     9
wenzelm@2789
    10
PRG=$(basename $0)
wenzelm@2755
    11
wenzelm@2789
    12
ISABELLE_HOME=$(dirname $0)
wenzelm@2789
    13
. $ISABELLE_HOME/lib/scripts/getsettings || \
wenzelm@2789
    14
  { echo "$PRG probably not called from its original place!"; exit 2 }
wenzelm@2755
    15
wenzelm@2789
    16
wenzelm@2879
    17
## diagnostics
wenzelm@2879
    18
wenzelm@2879
    19
function usage()
wenzelm@2879
    20
{
wenzelm@2879
    21
  echo
wenzelm@2879
    22
  echo "Usage: $PRG [OPTIONS] [LOGICS ...]"
wenzelm@2879
    23
  echo
wenzelm@2879
    24
  echo "  Options are:"
wenzelm@2879
    25
  echo "    -a           all logics"
wenzelm@2879
    26
  echo
wenzelm@2879
    27
  echo "  Compile the named LOGICS (default $DEFAULT_LOGIC), or all object logics"
wenzelm@2879
    28
  echo "  in the distribution."
wenzelm@2879
    29
  echo
wenzelm@2879
    30
  exit 1
wenzelm@2879
    31
}
wenzelm@2879
    32
wenzelm@2879
    33
function fail()
wenzelm@2879
    34
{
wenzelm@2879
    35
  echo "$1" >&2
wenzelm@2879
    36
  exit 2
wenzelm@2879
    37
}
wenzelm@2879
    38
wenzelm@2879
    39
wenzelm@2879
    40
## process command line
wenzelm@2879
    41
wenzelm@2879
    42
# options
wenzelm@2879
    43
wenzelm@2879
    44
ALL=""
wenzelm@2755
    45
wenzelm@2879
    46
while getopts "a" OPT
wenzelm@2879
    47
do
wenzelm@2879
    48
  case "$OPT" in
wenzelm@2879
    49
    a)
wenzelm@2879
    50
      ALL=true
wenzelm@2879
    51
      ;;
wenzelm@2879
    52
    \?)
wenzelm@2879
    53
      usage
wenzelm@2879
    54
      ;;
wenzelm@2879
    55
  esac
wenzelm@2879
    56
done
wenzelm@2879
    57
wenzelm@2879
    58
shift $(($OPTIND - 1))
wenzelm@2879
    59
wenzelm@2879
    60
wenzelm@2879
    61
# args
wenzelm@2879
    62
wenzelm@2879
    63
LOGICS="$@"
wenzelm@2879
    64
wenzelm@2879
    65
wenzelm@2879
    66
## main
wenzelm@2879
    67
wenzelm@2879
    68
# tell the user about current values
wenzelm@2879
    69
wenzelm@2879
    70
echo
wenzelm@2879
    71
echo "                *****************************"
wenzelm@2879
    72
echo "                * Welcome to Isabelle build *"
wenzelm@2879
    73
echo "                *****************************"
wenzelm@2755
    74
echo
wenzelm@2789
    75
echo "Please check $ISABELLE_HOME/etc/settings"
wenzelm@2789
    76
[ -f $ISABELLE_HOME_USER/etc/settings ] && echo "AND $ISABELLE_HOME_USER/etc/settings"
wenzelm@2755
    77
echo "to make sure that Isabelle's ML system settings are appropriate."
wenzelm@2879
    78
echo
wenzelm@2755
    79
echo "Your current values are:"
wenzelm@2755
    80
echo
wenzelm@2755
    81
wenzelm@2879
    82
echo "  ML_SYSTEM=$ML_SYSTEM"
wenzelm@2879
    83
echo "  ML_HOME=$ML_HOME"
wenzelm@2879
    84
echo "  ML_OPTIONS=$ML_OPTIONS"
wenzelm@2789
    85
wenzelm@2789
    86
wenzelm@2879
    87
# check logics
wenzelm@2755
    88
wenzelm@2755
    89
echo
wenzelm@2761
    90
echo
wenzelm@2879
    91
echo "Press RETURN to start compilation (including parents) of:"
wenzelm@2879
    92
echo
wenzelm@2879
    93
wenzelm@2879
    94
[ -z "$LOGICS" ] && LOGICS=$DEFAULT_LOGIC
wenzelm@2879
    95
wenzelm@2879
    96
if [ -n "$ALL" ]; then
wenzelm@2879
    97
  LOGICS=""
wenzelm@2879
    98
  for DIR in $ISABELLE_HOME/src/*
wenzelm@2879
    99
  do
wenzelm@2879
   100
    if [ -f $DIR/IsaMakefile ]; then
wenzelm@2879
   101
      L=$(basename $DIR)
wenzelm@2879
   102
      LOGICS="$LOGICS $L"
wenzelm@2879
   103
    fi
wenzelm@2879
   104
  done
wenzelm@2879
   105
else
wenzelm@2879
   106
  for L in $LOGICS
wenzelm@2879
   107
  do
wenzelm@2879
   108
    DIR=$ISABELLE_HOME/src/$L
wenzelm@2879
   109
    [ ! -f $DIR/IsaMakefile ] && fail "No such logic: $L"
wenzelm@2879
   110
  done
wenzelm@2879
   111
fi
wenzelm@2879
   112
wenzelm@2879
   113
echo " " $LOGICS
wenzelm@2879
   114
echo
wenzelm@2755
   115
read
wenzelm@2755
   116
wenzelm@2755
   117
wenzelm@2879
   118
# build it
wenzelm@2879
   119
wenzelm@2781
   120
export THIS_IS_ISABELLE_BUILD=true
wenzelm@2755
   121
wenzelm@2879
   122
for L in $LOGICS
wenzelm@2755
   123
do
wenzelm@2879
   124
  ( cd $ISABELLE_HOME/src/$L; $ISATOOL make )
wenzelm@2755
   125
done