src/Pure/mk
author wenzelm
Mon, 01 Dec 1997 18:22:38 +0100
changeset 4334 e567f3425267
parent 3774 b1bfd394b60a
child 4442 8ed9e689a15e
permissions -rwxr-xr-x
ISABELLE_TMP_PREFIX;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3056
200565f7592a removed -c option;
wenzelm
parents: 2768
diff changeset
     1
#!/bin/bash
2339
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
     2
#
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
     3
# $Id$
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
     4
#
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
     5
# mk - build Pure Isabelle.
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
     6
#
2432
527b5f1b7520 minor modifications to accomodate IsaMakefile;
wenzelm
parents: 2401
diff changeset
     7
# Assumes to be called via Isabelle make utility (cf. IsaMakefile).
2339
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
     8
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
     9
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    10
## diagnostics
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    11
3774
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    12
function usage()
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    13
{
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    14
  echo
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    15
  echo "Usage: $PRG [OPTIONS]"
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    16
  echo
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    17
  echo "  Make Pure Isabelle."
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    18
  echo
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    19
  echo "    -r           just prepare RAW image"
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    20
  echo
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    21
  exit 1
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    22
}
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    23
2339
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    24
function fail()
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    25
{
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    26
  echo "$1" >&2
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    27
  exit 2
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    28
}
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    29
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    30
3774
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    31
## process command line
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    32
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    33
# options
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    34
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    35
RAW=""
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    36
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    37
while getopts "r" OPT
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    38
do
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    39
  case "$OPT" in
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    40
    r)
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    41
      RAW=true
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    42
      ;;
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    43
    \?)
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    44
      usage
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    45
      ;;
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    46
  esac
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    47
done
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    48
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    49
shift $(($OPTIND - 1))
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    50
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    51
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    52
# args
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    53
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    54
[ $# -ne 0 ] && usage
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    55
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    56
2339
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    57
## main
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    58
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    59
ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
3056
200565f7592a removed -c option;
wenzelm
parents: 2768
diff changeset
    60
[ -z "$ML_SYSTEM" ] && \
200565f7592a removed -c option;
wenzelm
parents: 2768
diff changeset
    61
  fail "Missing ML system settings! Probably not run via 'isatool make'?."
2339
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    62
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    63
COMPAT=""
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    64
[ -f "ML-Systems/$ML_SYSTEM_BASE.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM_BASE.ML"
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    65
[ -f "ML-Systems/$ML_SYSTEM.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM.ML"
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    66
[ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    67
3774
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    68
if [ -z "$RAW" ]; then
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    69
  $ISABELLE \
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    70
    -e "val ml_system = \"$ML_SYSTEM\";" \
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    71
    -e "use\"$COMPAT\"; use\"ROOT.ML\" handle _ => exit 1;" \
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    72
    -q -w RAW_ML_SYSTEM Pure
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    73
else
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    74
  $ISABELLE \
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    75
    -e "val ml_system = \"$ML_SYSTEM\";" \
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    76
    -e "use\"$COMPAT\";" \
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    77
    -q -w RAW_ML_SYSTEM RAW
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    78
fi