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