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