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