src/Pure/mk
author wenzelm
Mon, 09 Nov 1998 15:42:08 +0100
changeset 5840 e2d2b896c717
parent 4495 8648ba842d14
child 6186 72abe86d9418
permissions -rwxr-xr-x
Object logic specific operations.
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
4442
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    59
# get compatibility file
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    60
2339
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    61
ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
3056
200565f7592a removed -c option;
wenzelm
parents: 2768
diff changeset
    62
[ -z "$ML_SYSTEM" ] && \
200565f7592a removed -c option;
wenzelm
parents: 2768
diff changeset
    63
  fail "Missing ML system settings! Probably not run via 'isatool make'?."
2339
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    64
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    65
COMPAT=""
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    66
[ -f "ML-Systems/$ML_SYSTEM_BASE.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM_BASE.ML"
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    67
[ -f "ML-Systems/$ML_SYSTEM.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM.ML"
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    68
[ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    69
4442
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    70
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    71
# prepare log dir
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    72
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    73
LOGDIR="$ISABELLE_OUTPUT/log"
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    74
mkdir -p "$LOGDIR"
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    75
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    76
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    77
# run isabelle
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    78
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    79
SECONDS=0
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    80
3774
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    81
if [ -z "$RAW" ]; then
4442
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    82
  ITEM="Pure"
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    83
  echo -n "Building $ITEM ... "
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    84
  LOG="$LOGDIR/$ITEM"
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    85
3774
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    86
  $ISABELLE \
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    87
    -e "val ml_system = \"$ML_SYSTEM\";" \
4495
8648ba842d14 improved error handling;
wenzelm
parents: 4492
diff changeset
    88
    -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
4492
ab441d89a2cb stderr to $LOG;
wenzelm
parents: 4442
diff changeset
    89
    -q -w RAW_ML_SYSTEM Pure > $LOG 2>&1
3774
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    90
else
4442
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    91
  ITEM="RAW"
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    92
  echo -n "Building $ITEM ... "
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    93
  LOG="$LOGDIR/$ITEM"
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    94
3774
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    95
  $ISABELLE \
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    96
    -e "val ml_system = \"$ML_SYSTEM\";" \
4495
8648ba842d14 improved error handling;
wenzelm
parents: 4492
diff changeset
    97
    -e "use\"$COMPAT\" handle _ => exit 1;;" \
4492
ab441d89a2cb stderr to $LOG;
wenzelm
parents: 4442
diff changeset
    98
    -q -w RAW_ML_SYSTEM RAW > $LOG 2>&1
3774
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    99
fi
4442
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   100
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   101
RC=$?
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   102
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   103
ELAPSED=$($ISABELLE_HOME/lib/scripts/showtime $SECONDS)
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   104
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   105
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   106
# exit status
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   107
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   108
if [ $RC -eq 0 ]; then
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   109
  echo "OK  ($ELAPSED elapsed time)"
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   110
  gzip --force "$LOG"
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   111
else
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   112
  echo "FAILED"
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   113
  echo "(see also $LOG)"
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   114
  echo; tail $LOG; echo
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   115
fi
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   116
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   117
exit $RC