src/Pure/mk
author wenzelm
Sat, 21 Jan 2006 23:02:14 +0100
changeset 18728 6790126ab5f6
parent 18321 3414557c2dda
child 20776 cc436bcdd5fc
permissions -rwxr-xr-x
simplified type attribute;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11391
e8638d07fdee #!/usr/bin/env bash;
wenzelm
parents: 10900
diff changeset
     1
#!/usr/bin/env bash
2339
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
     2
#
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
     3
# $Id$
9789
wenzelm
parents: 8361
diff changeset
     4
# Author: Markus Wenzel, TU Muenchen
2339
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
     5
#
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
     6
# mk - build Pure Isabelle.
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
     7
#
10102
3c21a2e616e7 support copy option;
wenzelm
parents: 9789
diff changeset
     8
# Requires proper Isabelle settings environment (cf. IsaMakefile).
2339
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
     9
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    10
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    11
## diagnostics
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    12
3774
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    13
function usage()
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    14
{
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    15
  echo
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    16
  echo "Usage: $PRG [OPTIONS]"
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    17
  echo
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    18
  echo "  Make Pure Isabelle."
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    19
  echo
10102
3c21a2e616e7 support copy option;
wenzelm
parents: 9789
diff changeset
    20
  echo "    -C           tell ML system to copy output image"
3c21a2e616e7 support copy option;
wenzelm
parents: 9789
diff changeset
    21
  echo "    -r           prepare RAW image only"
3774
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    22
  echo
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    23
  exit 1
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    24
}
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    25
2339
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    26
function fail()
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    27
{
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    28
  echo "$1" >&2
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    29
  exit 2
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    30
}
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    31
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    32
3774
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    33
## process command line
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    34
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    35
# options
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    36
10102
3c21a2e616e7 support copy option;
wenzelm
parents: 9789
diff changeset
    37
COPY=""
3774
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    38
RAW=""
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    39
10102
3c21a2e616e7 support copy option;
wenzelm
parents: 9789
diff changeset
    40
while getopts "Cr" OPT
3774
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    41
do
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    42
  case "$OPT" in
10102
3c21a2e616e7 support copy option;
wenzelm
parents: 9789
diff changeset
    43
    C)
3c21a2e616e7 support copy option;
wenzelm
parents: 9789
diff changeset
    44
      COPY="-C"
3c21a2e616e7 support copy option;
wenzelm
parents: 9789
diff changeset
    45
      ;;
3774
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    46
    r)
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    47
      RAW=true
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    48
      ;;
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    49
    \?)
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    50
      usage
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    51
      ;;
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    52
  esac
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    53
done
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    54
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    55
shift $(($OPTIND - 1))
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    56
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    57
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    58
# args
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    59
9789
wenzelm
parents: 8361
diff changeset
    60
[ "$#" -ne 0 ] && usage
3774
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    61
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    62
2339
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    63
## main
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    64
4442
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    65
# get compatibility file
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    66
9789
wenzelm
parents: 8361
diff changeset
    67
ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
16131
e1b85512d87d tuned msg;
wenzelm
parents: 15790
diff changeset
    68
[ -z "$ML_SYSTEM" ] && fail "Missing ML_SYSTEM settings!"
2339
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    69
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    70
COMPAT=""
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    71
[ -f "ML-Systems/$ML_SYSTEM_BASE.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM_BASE.ML"
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    72
[ -f "ML-Systems/$ML_SYSTEM.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM.ML"
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    73
[ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    74
4442
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    75
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    76
# prepare log dir
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    77
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    78
LOGDIR="$ISABELLE_OUTPUT/log"
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    79
mkdir -p "$LOGDIR"
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    80
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    81
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    82
# run isabelle
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    83
18321
3414557c2dda replaced lib/scripts/showtime by more advanced lib/scripts/timestart|stop.bash;
wenzelm
parents: 16376
diff changeset
    84
. "$ISABELLE_HOME/lib/scripts/timestart.bash"
4442
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    85
3774
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    86
if [ -z "$RAW" ]; then
4442
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    87
  ITEM="Pure"
7277
bb9502f9154a improved messages;
wenzelm
parents: 7263
diff changeset
    88
  echo "Building $ITEM ..."
4442
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    89
  LOG="$LOGDIR/$ITEM"
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    90
10102
3c21a2e616e7 support copy option;
wenzelm
parents: 9789
diff changeset
    91
  "$ISABELLE" $COPY \
3774
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    92
    -e "val ml_system = \"$ML_SYSTEM\";" \
16376
65e2df6d8e10 pass ml_platform;
wenzelm
parents: 16131
diff changeset
    93
    -e "val ml_platform = \"$ML_PLATFORM\";" \
4495
8648ba842d14 improved error handling;
wenzelm
parents: 4492
diff changeset
    94
    -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
10900
7268a5f425f8 isabelle -f;
wenzelm
parents: 10102
diff changeset
    95
    -f -c -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1
9789
wenzelm
parents: 8361
diff changeset
    96
  RC="$?"
3774
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
    97
else
4442
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
    98
  ITEM="RAW"
7277
bb9502f9154a improved messages;
wenzelm
parents: 7263
diff changeset
    99
  echo "Building $ITEM ..."
4442
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   100
  LOG="$LOGDIR/$ITEM"
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   101
10102
3c21a2e616e7 support copy option;
wenzelm
parents: 9789
diff changeset
   102
  "$ISABELLE" $COPY \
3774
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
   103
    -e "val ml_system = \"$ML_SYSTEM\";" \
16376
65e2df6d8e10 pass ml_platform;
wenzelm
parents: 16131
diff changeset
   104
    -e "val ml_platform = \"$ML_PLATFORM\";" \
10900
7268a5f425f8 isabelle -f;
wenzelm
parents: 10102
diff changeset
   105
    -e "use\"$COMPAT\" handle _ => exit 1;" \
9789
wenzelm
parents: 8361
diff changeset
   106
    -q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1
wenzelm
parents: 8361
diff changeset
   107
  RC="$?"
3774
b1bfd394b60a RAW target;
wenzelm
parents: 3505
diff changeset
   108
fi
4442
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   109
18321
3414557c2dda replaced lib/scripts/showtime by more advanced lib/scripts/timestart|stop.bash;
wenzelm
parents: 16376
diff changeset
   110
. "$ISABELLE_HOME/lib/scripts/timestop.bash"
4442
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   111
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   112
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   113
# exit status
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   114
9789
wenzelm
parents: 8361
diff changeset
   115
if [ "$RC" -eq 0 ]; then
18321
3414557c2dda replaced lib/scripts/showtime by more advanced lib/scripts/timestart|stop.bash;
wenzelm
parents: 16376
diff changeset
   116
  echo "Finished $ITEM ($TIMES_REPORT)"
4442
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   117
  gzip --force "$LOG"
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   118
else
7263
2d09363ada6c tuned messages;
wenzelm
parents: 6239
diff changeset
   119
  echo "$ITEM FAILED"
4442
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   120
  echo "(see also $LOG)"
9789
wenzelm
parents: 8361
diff changeset
   121
  echo; tail "$LOG"; echo
4442
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   122
fi
8ed9e689a15e log file;
wenzelm
parents: 3774
diff changeset
   123
9789
wenzelm
parents: 8361
diff changeset
   124
exit "$RC"