src/Pure/mk
author wenzelm
Mon Oct 06 18:20:15 1997 +0200 (1997-10-06)
changeset 3774 b1bfd394b60a
parent 3505 1cb4ea47d967
child 4442 8ed9e689a15e
permissions -rwxr-xr-x
RAW target;
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@2339
    59
ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
wenzelm@3056
    60
[ -z "$ML_SYSTEM" ] && \
wenzelm@3056
    61
  fail "Missing ML system settings! Probably not run via 'isatool make'?."
wenzelm@2339
    62
wenzelm@2339
    63
COMPAT=""
wenzelm@2339
    64
[ -f "ML-Systems/$ML_SYSTEM_BASE.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM_BASE.ML"
wenzelm@2339
    65
[ -f "ML-Systems/$ML_SYSTEM.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM.ML"
wenzelm@2339
    66
[ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
wenzelm@2339
    67
wenzelm@3774
    68
if [ -z "$RAW" ]; then
wenzelm@3774
    69
  $ISABELLE \
wenzelm@3774
    70
    -e "val ml_system = \"$ML_SYSTEM\";" \
wenzelm@3774
    71
    -e "use\"$COMPAT\"; use\"ROOT.ML\" handle _ => exit 1;" \
wenzelm@3774
    72
    -q -w RAW_ML_SYSTEM Pure
wenzelm@3774
    73
else
wenzelm@3774
    74
  $ISABELLE \
wenzelm@3774
    75
    -e "val ml_system = \"$ML_SYSTEM\";" \
wenzelm@3774
    76
    -e "use\"$COMPAT\";" \
wenzelm@3774
    77
    -q -w RAW_ML_SYSTEM RAW
wenzelm@3774
    78
fi