src/Pure/mk
author haftmann
Fri Nov 10 07:44:47 2006 +0100 (2006-11-10)
changeset 21286 b5e7b80caa6a
parent 20814 bc3a2b9b9960
child 21996 18937ee21db7
permissions -rwxr-xr-x
introduces canonical AList functions for loop_tacs
wenzelm@11391
     1
#!/usr/bin/env bash
wenzelm@2339
     2
#
wenzelm@2339
     3
# $Id$
wenzelm@9789
     4
# Author: Markus Wenzel, TU Muenchen
wenzelm@2339
     5
#
wenzelm@2339
     6
# mk - build Pure Isabelle.
wenzelm@2339
     7
#
wenzelm@10102
     8
# Requires proper Isabelle settings environment (cf. IsaMakefile).
wenzelm@2339
     9
wenzelm@2339
    10
wenzelm@2339
    11
## diagnostics
wenzelm@2339
    12
wenzelm@3774
    13
function usage()
wenzelm@3774
    14
{
wenzelm@3774
    15
  echo
wenzelm@3774
    16
  echo "Usage: $PRG [OPTIONS]"
wenzelm@3774
    17
  echo
wenzelm@3774
    18
  echo "  Make Pure Isabelle."
wenzelm@3774
    19
  echo
wenzelm@10102
    20
  echo "    -C           tell ML system to copy output image"
wenzelm@10102
    21
  echo "    -r           prepare RAW image only"
wenzelm@3774
    22
  echo
wenzelm@3774
    23
  exit 1
wenzelm@3774
    24
}
wenzelm@3774
    25
wenzelm@2339
    26
function fail()
wenzelm@2339
    27
{
wenzelm@2339
    28
  echo "$1" >&2
wenzelm@2339
    29
  exit 2
wenzelm@2339
    30
}
wenzelm@2339
    31
wenzelm@2339
    32
wenzelm@3774
    33
## process command line
wenzelm@3774
    34
wenzelm@3774
    35
# options
wenzelm@3774
    36
wenzelm@10102
    37
COPY=""
wenzelm@3774
    38
RAW=""
wenzelm@3774
    39
wenzelm@10102
    40
while getopts "Cr" OPT
wenzelm@3774
    41
do
wenzelm@3774
    42
  case "$OPT" in
wenzelm@10102
    43
    C)
wenzelm@10102
    44
      COPY="-C"
wenzelm@10102
    45
      ;;
wenzelm@3774
    46
    r)
wenzelm@3774
    47
      RAW=true
wenzelm@3774
    48
      ;;
wenzelm@3774
    49
    \?)
wenzelm@3774
    50
      usage
wenzelm@3774
    51
      ;;
wenzelm@3774
    52
  esac
wenzelm@3774
    53
done
wenzelm@3774
    54
wenzelm@3774
    55
shift $(($OPTIND - 1))
wenzelm@3774
    56
wenzelm@3774
    57
wenzelm@3774
    58
# args
wenzelm@3774
    59
wenzelm@9789
    60
[ "$#" -ne 0 ] && usage
wenzelm@3774
    61
wenzelm@3774
    62
wenzelm@2339
    63
## main
wenzelm@2339
    64
wenzelm@4442
    65
# get compatibility file
wenzelm@4442
    66
wenzelm@9789
    67
ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
wenzelm@16131
    68
[ -z "$ML_SYSTEM" ] && fail "Missing ML_SYSTEM settings!"
wenzelm@2339
    69
wenzelm@2339
    70
COMPAT=""
wenzelm@2339
    71
[ -f "ML-Systems/$ML_SYSTEM_BASE.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM_BASE.ML"
wenzelm@2339
    72
[ -f "ML-Systems/$ML_SYSTEM.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM.ML"
wenzelm@2339
    73
[ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
wenzelm@2339
    74
wenzelm@4442
    75
wenzelm@4442
    76
# prepare log dir
wenzelm@4442
    77
wenzelm@4442
    78
LOGDIR="$ISABELLE_OUTPUT/log"
wenzelm@4442
    79
mkdir -p "$LOGDIR"
wenzelm@4442
    80
wenzelm@4442
    81
wenzelm@4442
    82
# run isabelle
wenzelm@4442
    83
wenzelm@18321
    84
. "$ISABELLE_HOME/lib/scripts/timestart.bash"
wenzelm@4442
    85
wenzelm@3774
    86
if [ -z "$RAW" ]; then
wenzelm@4442
    87
  ITEM="Pure"
wenzelm@7277
    88
  echo "Building $ITEM ..."
wenzelm@4442
    89
  LOG="$LOGDIR/$ITEM"
wenzelm@4442
    90
wenzelm@10102
    91
  "$ISABELLE" $COPY \
wenzelm@3774
    92
    -e "val ml_system = \"$ML_SYSTEM\";" \
wenzelm@16376
    93
    -e "val ml_platform = \"$ML_PLATFORM\";" \
wenzelm@4495
    94
    -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
wenzelm@10900
    95
    -f -c -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1
wenzelm@9789
    96
  RC="$?"
wenzelm@3774
    97
else
wenzelm@4442
    98
  ITEM="RAW"
wenzelm@7277
    99
  echo "Building $ITEM ..."
wenzelm@4442
   100
  LOG="$LOGDIR/$ITEM"
wenzelm@4442
   101
wenzelm@10102
   102
  "$ISABELLE" $COPY \
wenzelm@3774
   103
    -e "val ml_system = \"$ML_SYSTEM\";" \
wenzelm@16376
   104
    -e "val ml_platform = \"$ML_PLATFORM\";" \
wenzelm@10900
   105
    -e "use\"$COMPAT\" handle _ => exit 1;" \
wenzelm@9789
   106
    -q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1
wenzelm@9789
   107
  RC="$?"
wenzelm@3774
   108
fi
wenzelm@4442
   109
wenzelm@18321
   110
. "$ISABELLE_HOME/lib/scripts/timestop.bash"
wenzelm@4442
   111
wenzelm@4442
   112
wenzelm@4442
   113
# exit status
wenzelm@4442
   114
wenzelm@9789
   115
if [ "$RC" -eq 0 ]; then
wenzelm@18321
   116
  echo "Finished $ITEM ($TIMES_REPORT)"
wenzelm@4442
   117
  gzip --force "$LOG"
wenzelm@4442
   118
else
wenzelm@7263
   119
  echo "$ITEM FAILED"
wenzelm@4442
   120
  echo "(see also $LOG)"
wenzelm@9789
   121
  echo; tail "$LOG"; echo
wenzelm@4442
   122
fi
wenzelm@4442
   123
wenzelm@9789
   124
exit "$RC"