build
author wenzelm
Thu Aug 27 13:52:46 1998 +0200 (1998-08-27)
changeset 5386 4325d853494a
parent 4581 52edf5ac3afa
child 5393 7299e531d481
permissions -rwxr-xr-x
tuned;
added ISABELLE_USEDIR_OPTIONS;
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@4457
     8
## global settings
wenzelm@4457
     9
wenzelm@4457
    10
ALL_LOGICS="CCL CTT Cube FOL FOLP HOL HOLCF LCF Pure Sequents ZF"
wenzelm@4457
    11
wenzelm@4457
    12
wenzelm@2789
    13
## settings
wenzelm@2789
    14
wenzelm@2789
    15
PRG=$(basename $0)
wenzelm@2755
    16
wenzelm@2789
    17
ISABELLE_HOME=$(dirname $0)
wenzelm@2789
    18
. $ISABELLE_HOME/lib/scripts/getsettings || \
wenzelm@2936
    19
  { echo "$PRG probably not called from its original place!"; exit 2; }
wenzelm@2755
    20
wenzelm@2789
    21
wenzelm@2879
    22
## diagnostics
wenzelm@2879
    23
wenzelm@2879
    24
function usage()
wenzelm@2879
    25
{
wenzelm@2879
    26
  echo
wenzelm@2879
    27
  echo "Usage: $PRG [OPTIONS] [LOGICS ...]"
wenzelm@2879
    28
  echo
wenzelm@2879
    29
  echo "  Options are:"
wenzelm@2879
    30
  echo "    -a           all logics"
wenzelm@2902
    31
  echo "    -b           batch mode"
wenzelm@2918
    32
  echo "    -t           run tests"
wenzelm@2879
    33
  echo
wenzelm@3184
    34
  echo "  Compile the named LOGICS (default $ISABELLE_LOGIC), or all object logics"
wenzelm@2879
    35
  echo "  in the distribution."
wenzelm@2879
    36
  echo
wenzelm@2879
    37
  exit 1
wenzelm@2879
    38
}
wenzelm@2879
    39
wenzelm@2879
    40
function fail()
wenzelm@2879
    41
{
wenzelm@2879
    42
  echo "$1" >&2
wenzelm@2879
    43
  exit 2
wenzelm@2879
    44
}
wenzelm@2879
    45
wenzelm@2879
    46
wenzelm@2879
    47
## process command line
wenzelm@2879
    48
wenzelm@2879
    49
# options
wenzelm@2879
    50
wenzelm@2879
    51
ALL=""
wenzelm@2902
    52
BATCH=""
wenzelm@2918
    53
TEST=""
wenzelm@2755
    54
wenzelm@2918
    55
while getopts "abt" OPT
wenzelm@2879
    56
do
wenzelm@2879
    57
  case "$OPT" in
wenzelm@2879
    58
    a)
wenzelm@2879
    59
      ALL=true
wenzelm@2879
    60
      ;;
wenzelm@2902
    61
    b)
wenzelm@2902
    62
      BATCH=true
wenzelm@2902
    63
      ;;
wenzelm@2918
    64
    t)
wenzelm@2918
    65
      TEST=test
wenzelm@2918
    66
      ;;
wenzelm@2879
    67
    \?)
wenzelm@2879
    68
      usage
wenzelm@2879
    69
      ;;
wenzelm@2879
    70
  esac
wenzelm@2879
    71
done
wenzelm@2879
    72
wenzelm@2879
    73
shift $(($OPTIND - 1))
wenzelm@2879
    74
wenzelm@2879
    75
wenzelm@2879
    76
# args
wenzelm@2879
    77
wenzelm@2879
    78
LOGICS="$@"
wenzelm@2879
    79
wenzelm@4457
    80
[ -n "$ALL" ] && LOGICS="$LOGICS $ALL_LOGICS"
wenzelm@4457
    81
[ -z "$LOGICS" ] && LOGICS="$ISABELLE_LOGIC"
wenzelm@4457
    82
wenzelm@2879
    83
wenzelm@2879
    84
## main
wenzelm@2879
    85
wenzelm@2879
    86
# tell the user about current values
wenzelm@2879
    87
wenzelm@2902
    88
if [ -z "$BATCH" ]; then
wenzelm@2902
    89
  echo
wenzelm@2902
    90
  echo "                *****************************"
wenzelm@2902
    91
  echo "                * Welcome to Isabelle build *"
wenzelm@2902
    92
  echo "                *****************************"
wenzelm@2902
    93
  echo
wenzelm@2902
    94
  echo "Please check $ISABELLE_HOME/etc/settings"
wenzelm@2902
    95
  [ -f $ISABELLE_HOME_USER/etc/settings ] && echo "AND $ISABELLE_HOME_USER/etc/settings"
wenzelm@5386
    96
  echo "to make sure that Isabelle's ML system settings and compilation options"
wenzelm@5386
    97
  echo "are appropriate."
wenzelm@2902
    98
  echo
wenzelm@5386
    99
  echo "The current values are:"
wenzelm@2902
   100
  echo
wenzelm@2902
   101
  echo "  ML_SYSTEM=$ML_SYSTEM"
wenzelm@2902
   102
  echo "  ML_HOME=$ML_HOME"
wenzelm@2902
   103
  echo "  ML_OPTIONS=$ML_OPTIONS"
wenzelm@5386
   104
  echo
wenzelm@5386
   105
  echo "  ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
wenzelm@2902
   106
fi
wenzelm@2789
   107
wenzelm@2789
   108
wenzelm@2879
   109
# check logics
wenzelm@2755
   110
wenzelm@2902
   111
if [ -z "$BATCH" ]; then
wenzelm@2902
   112
  echo
wenzelm@2902
   113
  echo
wenzelm@2902
   114
  echo "Press RETURN to start compilation (including parents) of:"
wenzelm@2902
   115
  echo
wenzelm@2902
   116
fi
wenzelm@2879
   117
wenzelm@4457
   118
wenzelm@4457
   119
MAKE_LOGICS=""
wenzelm@2879
   120
wenzelm@4457
   121
for L in $LOGICS
wenzelm@4457
   122
do
wenzelm@4457
   123
  DIR=$ISABELLE_HOME/src/$L
wenzelm@4457
   124
  if [ -f $DIR/IsaMakefile ]; then
wenzelm@4457
   125
    MAKE_LOGICS="$MAKE_LOGICS $L"
wenzelm@4457
   126
  else
wenzelm@4457
   127
    echo "No such logic: $L"
wenzelm@4457
   128
  fi
wenzelm@4457
   129
done
wenzelm@4457
   130
wenzelm@2879
   131
wenzelm@2902
   132
if [ -z "$BATCH" ]; then
wenzelm@4457
   133
  echo " " $MAKE_LOGICS
wenzelm@2902
   134
  echo
wenzelm@2902
   135
  read
wenzelm@2902
   136
else
wenzelm@2902
   137
  echo
wenzelm@4457
   138
  echo "Isabelle build:" $MAKE_LOGICS
wenzelm@2914
   139
  echo
wenzelm@2902
   140
  echo "ML_SYSTEM=$ML_SYSTEM"
wenzelm@2902
   141
  echo "ML_HOME=$ML_HOME"
wenzelm@2902
   142
  echo "ML_OPTIONS=$ML_OPTIONS"
wenzelm@2902
   143
  echo
wenzelm@2902
   144
fi
wenzelm@2755
   145
wenzelm@2755
   146
wenzelm@2879
   147
# build it
wenzelm@2879
   148
wenzelm@4457
   149
SECONDS=0
wenzelm@2914
   150
echo -n "Started at "; date
wenzelm@2914
   151
wenzelm@2781
   152
export THIS_IS_ISABELLE_BUILD=true
wenzelm@2755
   153
wenzelm@4457
   154
for L in $MAKE_LOGICS
wenzelm@2755
   155
do
wenzelm@4581
   156
  ( cd $ISABELLE_HOME/src/$L; $ISATOOL make images $TEST )
wenzelm@2755
   157
done
wenzelm@2902
   158
wenzelm@2914
   159
echo -n "Finished at "; date
wenzelm@4457
   160
wenzelm@4457
   161
ELAPSED=$($ISABELLE_HOME/lib/scripts/showtime $SECONDS)
wenzelm@4457
   162
echo "$ELAPSED total elapsed time"