src/Pure/mk
author wenzelm
Fri Sep 01 17:54:58 2000 +0200 (2000-09-01)
changeset 9789 7e5e6c47c0b5
parent 8361 ac19e5abbfb1
child 10102 3c21a2e616e7
permissions -rwxr-xr-x
GPLed;
more robust handling of spaces in args / file names;
wenzelm@3056
     1
#!/bin/bash
wenzelm@2339
     2
#
wenzelm@2339
     3
# $Id$
wenzelm@9789
     4
# Author: Markus Wenzel, TU Muenchen
wenzelm@9789
     5
# License: GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@2339
     6
#
wenzelm@2339
     7
# mk - build Pure Isabelle.
wenzelm@2339
     8
#
wenzelm@2432
     9
# Assumes to be called via Isabelle make utility (cf. IsaMakefile).
wenzelm@2339
    10
wenzelm@2339
    11
wenzelm@2339
    12
## diagnostics
wenzelm@2339
    13
wenzelm@3774
    14
function usage()
wenzelm@3774
    15
{
wenzelm@3774
    16
  echo
wenzelm@3774
    17
  echo "Usage: $PRG [OPTIONS]"
wenzelm@3774
    18
  echo
wenzelm@3774
    19
  echo "  Make Pure Isabelle."
wenzelm@3774
    20
  echo
wenzelm@3774
    21
  echo "    -r           just prepare RAW image"
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@3774
    37
RAW=""
wenzelm@3774
    38
wenzelm@3774
    39
while getopts "r" OPT
wenzelm@3774
    40
do
wenzelm@3774
    41
  case "$OPT" in
wenzelm@3774
    42
    r)
wenzelm@3774
    43
      RAW=true
wenzelm@3774
    44
      ;;
wenzelm@3774
    45
    \?)
wenzelm@3774
    46
      usage
wenzelm@3774
    47
      ;;
wenzelm@3774
    48
  esac
wenzelm@3774
    49
done
wenzelm@3774
    50
wenzelm@3774
    51
shift $(($OPTIND - 1))
wenzelm@3774
    52
wenzelm@3774
    53
wenzelm@3774
    54
# args
wenzelm@3774
    55
wenzelm@9789
    56
[ "$#" -ne 0 ] && usage
wenzelm@3774
    57
wenzelm@3774
    58
wenzelm@2339
    59
## main
wenzelm@2339
    60
wenzelm@4442
    61
# get compatibility file
wenzelm@4442
    62
wenzelm@9789
    63
ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
wenzelm@3056
    64
[ -z "$ML_SYSTEM" ] && \
wenzelm@6186
    65
  fail "Missing ML system settings! Probably not run via 'isatool make'."
wenzelm@2339
    66
wenzelm@2339
    67
COMPAT=""
wenzelm@2339
    68
[ -f "ML-Systems/$ML_SYSTEM_BASE.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM_BASE.ML"
wenzelm@2339
    69
[ -f "ML-Systems/$ML_SYSTEM.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM.ML"
wenzelm@2339
    70
[ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
wenzelm@2339
    71
wenzelm@4442
    72
wenzelm@4442
    73
# prepare log dir
wenzelm@4442
    74
wenzelm@4442
    75
LOGDIR="$ISABELLE_OUTPUT/log"
wenzelm@4442
    76
mkdir -p "$LOGDIR"
wenzelm@4442
    77
wenzelm@4442
    78
wenzelm@4442
    79
# run isabelle
wenzelm@4442
    80
wenzelm@4442
    81
SECONDS=0
wenzelm@4442
    82
wenzelm@3774
    83
if [ -z "$RAW" ]; then
wenzelm@4442
    84
  ITEM="Pure"
wenzelm@7277
    85
  echo "Building $ITEM ..."
wenzelm@4442
    86
  LOG="$LOGDIR/$ITEM"
wenzelm@4442
    87
wenzelm@9789
    88
  "$ISABELLE" \
wenzelm@3774
    89
    -e "val ml_system = \"$ML_SYSTEM\";" \
wenzelm@4495
    90
    -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
wenzelm@9789
    91
    -c -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1
wenzelm@9789
    92
  RC="$?"
wenzelm@3774
    93
else
wenzelm@4442
    94
  ITEM="RAW"
wenzelm@7277
    95
  echo "Building $ITEM ..."
wenzelm@4442
    96
  LOG="$LOGDIR/$ITEM"
wenzelm@4442
    97
wenzelm@9789
    98
  "$ISABELLE" \
wenzelm@3774
    99
    -e "val ml_system = \"$ML_SYSTEM\";" \
wenzelm@4495
   100
    -e "use\"$COMPAT\" handle _ => exit 1;;" \
wenzelm@9789
   101
    -q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1
wenzelm@9789
   102
  RC="$?"
wenzelm@3774
   103
fi
wenzelm@4442
   104
wenzelm@9789
   105
ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS")
wenzelm@4442
   106
wenzelm@4442
   107
wenzelm@4442
   108
# exit status
wenzelm@4442
   109
wenzelm@9789
   110
if [ "$RC" -eq 0 ]; then
wenzelm@7277
   111
  echo "Finished $ITEM ($ELAPSED elapsed time)"
wenzelm@4442
   112
  gzip --force "$LOG"
wenzelm@4442
   113
else
wenzelm@7263
   114
  echo "$ITEM FAILED"
wenzelm@4442
   115
  echo "(see also $LOG)"
wenzelm@9789
   116
  echo; tail "$LOG"; echo
wenzelm@4442
   117
fi
wenzelm@4442
   118
wenzelm@9789
   119
exit "$RC"