build
author wenzelm
Wed Jul 09 16:52:51 1997 +0200 (1997-07-09)
changeset 3508 089806e6133b
parent 3255 7678f3d93053
child 4457 6e6d99e06d0c
permissions -rwxr-xr-x
removed init_database;
wenzelm@3255
     1
#!/bin/bash
wenzelm@2755
     2
#
wenzelm@2755
     3
# $Id$
wenzelm@2755
     4
#
wenzelm@2902
     5
# build - compile the Isabelle system and object-logics
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@2936
    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@2902
    26
  echo "    -b           batch mode"
wenzelm@2918
    27
  echo "    -t           run tests"
wenzelm@2879
    28
  echo
wenzelm@3184
    29
  echo "  Compile the named LOGICS (default $ISABELLE_LOGIC), or all object logics"
wenzelm@2879
    30
  echo "  in the distribution."
wenzelm@2879
    31
  echo
wenzelm@2879
    32
  exit 1
wenzelm@2879
    33
}
wenzelm@2879
    34
wenzelm@2879
    35
function fail()
wenzelm@2879
    36
{
wenzelm@2879
    37
  echo "$1" >&2
wenzelm@2879
    38
  exit 2
wenzelm@2879
    39
}
wenzelm@2879
    40
wenzelm@2879
    41
wenzelm@2879
    42
## process command line
wenzelm@2879
    43
wenzelm@2879
    44
# options
wenzelm@2879
    45
wenzelm@2879
    46
ALL=""
wenzelm@2902
    47
BATCH=""
wenzelm@2918
    48
TEST=""
wenzelm@2755
    49
wenzelm@2918
    50
while getopts "abt" OPT
wenzelm@2879
    51
do
wenzelm@2879
    52
  case "$OPT" in
wenzelm@2879
    53
    a)
wenzelm@2879
    54
      ALL=true
wenzelm@2879
    55
      ;;
wenzelm@2902
    56
    b)
wenzelm@2902
    57
      BATCH=true
wenzelm@2902
    58
      ;;
wenzelm@2918
    59
    t)
wenzelm@2918
    60
      TEST=test
wenzelm@2918
    61
      ;;
wenzelm@2879
    62
    \?)
wenzelm@2879
    63
      usage
wenzelm@2879
    64
      ;;
wenzelm@2879
    65
  esac
wenzelm@2879
    66
done
wenzelm@2879
    67
wenzelm@2879
    68
shift $(($OPTIND - 1))
wenzelm@2879
    69
wenzelm@2879
    70
wenzelm@2879
    71
# args
wenzelm@2879
    72
wenzelm@2879
    73
LOGICS="$@"
wenzelm@2879
    74
wenzelm@2879
    75
wenzelm@2879
    76
## main
wenzelm@2879
    77
wenzelm@2879
    78
# tell the user about current values
wenzelm@2879
    79
wenzelm@2902
    80
if [ -z "$BATCH" ]; then
wenzelm@2902
    81
  echo
wenzelm@2902
    82
  echo "                *****************************"
wenzelm@2902
    83
  echo "                * Welcome to Isabelle build *"
wenzelm@2902
    84
  echo "                *****************************"
wenzelm@2902
    85
  echo
wenzelm@2902
    86
  echo "Please check $ISABELLE_HOME/etc/settings"
wenzelm@2902
    87
  [ -f $ISABELLE_HOME_USER/etc/settings ] && echo "AND $ISABELLE_HOME_USER/etc/settings"
wenzelm@2902
    88
  echo "to make sure that Isabelle's ML system settings are appropriate."
wenzelm@2902
    89
  echo
wenzelm@2902
    90
  echo "Your current values are:"
wenzelm@2902
    91
  echo
wenzelm@2902
    92
  echo "  ML_SYSTEM=$ML_SYSTEM"
wenzelm@2902
    93
  echo "  ML_HOME=$ML_HOME"
wenzelm@2902
    94
  echo "  ML_OPTIONS=$ML_OPTIONS"
wenzelm@2902
    95
fi
wenzelm@2789
    96
wenzelm@2789
    97
wenzelm@2879
    98
# check logics
wenzelm@2755
    99
wenzelm@2902
   100
if [ -z "$BATCH" ]; then
wenzelm@2902
   101
  echo
wenzelm@2902
   102
  echo
wenzelm@2902
   103
  echo "Press RETURN to start compilation (including parents) of:"
wenzelm@2902
   104
  echo
wenzelm@2902
   105
fi
wenzelm@2879
   106
wenzelm@3184
   107
[ -z "$LOGICS" ] && LOGICS=$ISABELLE_LOGIC
wenzelm@2879
   108
wenzelm@2879
   109
if [ -n "$ALL" ]; then
wenzelm@2879
   110
  LOGICS=""
wenzelm@2879
   111
  for DIR in $ISABELLE_HOME/src/*
wenzelm@2879
   112
  do
wenzelm@2879
   113
    if [ -f $DIR/IsaMakefile ]; then
wenzelm@2879
   114
      L=$(basename $DIR)
wenzelm@2879
   115
      LOGICS="$LOGICS $L"
wenzelm@2879
   116
    fi
wenzelm@2879
   117
  done
wenzelm@2879
   118
else
wenzelm@2879
   119
  for L in $LOGICS
wenzelm@2879
   120
  do
wenzelm@2879
   121
    DIR=$ISABELLE_HOME/src/$L
wenzelm@2879
   122
    [ ! -f $DIR/IsaMakefile ] && fail "No such logic: $L"
wenzelm@2879
   123
  done
wenzelm@2879
   124
fi
wenzelm@2879
   125
wenzelm@2902
   126
if [ -z "$BATCH" ]; then
wenzelm@2902
   127
  echo " " $LOGICS
wenzelm@2902
   128
  echo
wenzelm@2902
   129
  read
wenzelm@2902
   130
else
wenzelm@2902
   131
  echo
wenzelm@2914
   132
  echo "Isabelle build:" $LOGICS
wenzelm@2914
   133
  echo
wenzelm@2902
   134
  echo "ML_SYSTEM=$ML_SYSTEM"
wenzelm@2902
   135
  echo "ML_HOME=$ML_HOME"
wenzelm@2902
   136
  echo "ML_OPTIONS=$ML_OPTIONS"
wenzelm@2902
   137
  echo
wenzelm@2902
   138
fi
wenzelm@2755
   139
wenzelm@2755
   140
wenzelm@2879
   141
# build it
wenzelm@2879
   142
wenzelm@2914
   143
echo
wenzelm@2914
   144
echo -n "Started at "; date
wenzelm@2914
   145
echo
wenzelm@2914
   146
wenzelm@2781
   147
export THIS_IS_ISABELLE_BUILD=true
wenzelm@2755
   148
wenzelm@2879
   149
for L in $LOGICS
wenzelm@2755
   150
do
wenzelm@2918
   151
  ( cd $ISABELLE_HOME/src/$L; $ISATOOL make $TEST )
wenzelm@2755
   152
done
wenzelm@2902
   153
wenzelm@2914
   154
echo
wenzelm@2914
   155
echo -n "Finished at "; date
wenzelm@2914
   156
echo