src/Pure/mk
author wenzelm
Wed Feb 03 16:41:00 1999 +0100 (1999-02-03)
changeset 6186 72abe86d9418
parent 4495 8648ba842d14
child 6239 6b9194aff620
permissions -rwxr-xr-x
tuned msg;
wenzelm@3056
     1
#!/bin/bash
wenzelm@2339
     2
#
wenzelm@2339
     3
# $Id$
wenzelm@2339
     4
#
wenzelm@2339
     5
# mk - build Pure Isabelle.
wenzelm@2339
     6
#
wenzelm@2432
     7
# Assumes to be called via Isabelle make utility (cf. IsaMakefile).
wenzelm@2339
     8
wenzelm@2339
     9
wenzelm@2339
    10
## diagnostics
wenzelm@2339
    11
wenzelm@3774
    12
function usage()
wenzelm@3774
    13
{
wenzelm@3774
    14
  echo
wenzelm@3774
    15
  echo "Usage: $PRG [OPTIONS]"
wenzelm@3774
    16
  echo
wenzelm@3774
    17
  echo "  Make Pure Isabelle."
wenzelm@3774
    18
  echo
wenzelm@3774
    19
  echo "    -r           just prepare RAW image"
wenzelm@3774
    20
  echo
wenzelm@3774
    21
  exit 1
wenzelm@3774
    22
}
wenzelm@3774
    23
wenzelm@2339
    24
function fail()
wenzelm@2339
    25
{
wenzelm@2339
    26
  echo "$1" >&2
wenzelm@2339
    27
  exit 2
wenzelm@2339
    28
}
wenzelm@2339
    29
wenzelm@2339
    30
wenzelm@3774
    31
## process command line
wenzelm@3774
    32
wenzelm@3774
    33
# options
wenzelm@3774
    34
wenzelm@3774
    35
RAW=""
wenzelm@3774
    36
wenzelm@3774
    37
while getopts "r" OPT
wenzelm@3774
    38
do
wenzelm@3774
    39
  case "$OPT" in
wenzelm@3774
    40
    r)
wenzelm@3774
    41
      RAW=true
wenzelm@3774
    42
      ;;
wenzelm@3774
    43
    \?)
wenzelm@3774
    44
      usage
wenzelm@3774
    45
      ;;
wenzelm@3774
    46
  esac
wenzelm@3774
    47
done
wenzelm@3774
    48
wenzelm@3774
    49
shift $(($OPTIND - 1))
wenzelm@3774
    50
wenzelm@3774
    51
wenzelm@3774
    52
# args
wenzelm@3774
    53
wenzelm@3774
    54
[ $# -ne 0 ] && usage
wenzelm@3774
    55
wenzelm@3774
    56
wenzelm@2339
    57
## main
wenzelm@2339
    58
wenzelm@4442
    59
# get compatibility file
wenzelm@4442
    60
wenzelm@2339
    61
ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
wenzelm@3056
    62
[ -z "$ML_SYSTEM" ] && \
wenzelm@6186
    63
  fail "Missing ML system settings! Probably not run via 'isatool make'."
wenzelm@2339
    64
wenzelm@2339
    65
COMPAT=""
wenzelm@2339
    66
[ -f "ML-Systems/$ML_SYSTEM_BASE.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM_BASE.ML"
wenzelm@2339
    67
[ -f "ML-Systems/$ML_SYSTEM.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM.ML"
wenzelm@2339
    68
[ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
wenzelm@2339
    69
wenzelm@4442
    70
wenzelm@4442
    71
# prepare log dir
wenzelm@4442
    72
wenzelm@4442
    73
LOGDIR="$ISABELLE_OUTPUT/log"
wenzelm@4442
    74
mkdir -p "$LOGDIR"
wenzelm@4442
    75
wenzelm@4442
    76
wenzelm@4442
    77
# run isabelle
wenzelm@4442
    78
wenzelm@4442
    79
SECONDS=0
wenzelm@4442
    80
wenzelm@3774
    81
if [ -z "$RAW" ]; then
wenzelm@4442
    82
  ITEM="Pure"
wenzelm@4442
    83
  echo -n "Building $ITEM ... "
wenzelm@4442
    84
  LOG="$LOGDIR/$ITEM"
wenzelm@4442
    85
wenzelm@3774
    86
  $ISABELLE \
wenzelm@3774
    87
    -e "val ml_system = \"$ML_SYSTEM\";" \
wenzelm@4495
    88
    -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
wenzelm@4492
    89
    -q -w RAW_ML_SYSTEM Pure > $LOG 2>&1
wenzelm@3774
    90
else
wenzelm@4442
    91
  ITEM="RAW"
wenzelm@4442
    92
  echo -n "Building $ITEM ... "
wenzelm@4442
    93
  LOG="$LOGDIR/$ITEM"
wenzelm@4442
    94
wenzelm@3774
    95
  $ISABELLE \
wenzelm@3774
    96
    -e "val ml_system = \"$ML_SYSTEM\";" \
wenzelm@4495
    97
    -e "use\"$COMPAT\" handle _ => exit 1;;" \
wenzelm@4492
    98
    -q -w RAW_ML_SYSTEM RAW > $LOG 2>&1
wenzelm@3774
    99
fi
wenzelm@4442
   100
wenzelm@4442
   101
RC=$?
wenzelm@4442
   102
wenzelm@4442
   103
ELAPSED=$($ISABELLE_HOME/lib/scripts/showtime $SECONDS)
wenzelm@4442
   104
wenzelm@4442
   105
wenzelm@4442
   106
# exit status
wenzelm@4442
   107
wenzelm@4442
   108
if [ $RC -eq 0 ]; then
wenzelm@4442
   109
  echo "OK  ($ELAPSED elapsed time)"
wenzelm@4442
   110
  gzip --force "$LOG"
wenzelm@4442
   111
else
wenzelm@4442
   112
  echo "FAILED"
wenzelm@4442
   113
  echo "(see also $LOG)"
wenzelm@4442
   114
  echo; tail $LOG; echo
wenzelm@4442
   115
fi
wenzelm@4442
   116
wenzelm@4442
   117
exit $RC