src/Pure/mk
author wenzelm
Fri May 28 20:41:23 2010 +0200 (2010-05-28)
changeset 37174 6feaab4fc27d
parent 34282 549969a7f582
child 43948 8f5add916a99
permissions -rwxr-xr-x
assume given SCALA_HOME, e.g. from component settings or external setup;
wenzelm@11391
     1
#!/usr/bin/env bash
wenzelm@2339
     2
#
wenzelm@9789
     3
# Author: Markus Wenzel, TU Muenchen
wenzelm@2339
     4
#
wenzelm@34282
     5
# mk - build Isabelle/Pure.
wenzelm@2339
     6
#
wenzelm@34282
     7
# Requires proper Isabelle settings environment.
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@21996
    19
  echo "    -R DIR/FILE  run RAW session"
wenzelm@21996
    20
  echo "    -r           build RAW image"
wenzelm@3774
    21
  echo
wenzelm@3774
    22
  exit 1
wenzelm@3774
    23
}
wenzelm@3774
    24
wenzelm@2339
    25
function fail()
wenzelm@2339
    26
{
wenzelm@2339
    27
  echo "$1" >&2
wenzelm@2339
    28
  exit 2
wenzelm@2339
    29
}
wenzelm@2339
    30
wenzelm@2339
    31
wenzelm@3774
    32
## process command line
wenzelm@3774
    33
wenzelm@3774
    34
# options
wenzelm@3774
    35
wenzelm@21996
    36
RAW_SESSION=""
wenzelm@3774
    37
RAW=""
wenzelm@3774
    38
wenzelm@21996
    39
while getopts "R:r" OPT
wenzelm@3774
    40
do
wenzelm@3774
    41
  case "$OPT" in
wenzelm@21996
    42
    R)
wenzelm@21996
    43
      RAW_SESSION="$OPTARG"
wenzelm@10102
    44
      ;;
wenzelm@3774
    45
    r)
wenzelm@3774
    46
      RAW=true
wenzelm@3774
    47
      ;;
wenzelm@3774
    48
    \?)
wenzelm@3774
    49
      usage
wenzelm@3774
    50
      ;;
wenzelm@3774
    51
  esac
wenzelm@3774
    52
done
wenzelm@3774
    53
wenzelm@3774
    54
shift $(($OPTIND - 1))
wenzelm@3774
    55
wenzelm@3774
    56
wenzelm@3774
    57
# args
wenzelm@3774
    58
wenzelm@9789
    59
[ "$#" -ne 0 ] && usage
wenzelm@3774
    60
wenzelm@3774
    61
wenzelm@2339
    62
## main
wenzelm@2339
    63
wenzelm@4442
    64
# get compatibility file
wenzelm@4442
    65
wenzelm@9789
    66
ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
wenzelm@16131
    67
[ -z "$ML_SYSTEM" ] && fail "Missing ML_SYSTEM settings!"
wenzelm@2339
    68
wenzelm@2339
    69
COMPAT=""
wenzelm@2339
    70
[ -f "ML-Systems/$ML_SYSTEM_BASE.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM_BASE.ML"
wenzelm@2339
    71
[ -f "ML-Systems/$ML_SYSTEM.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM.ML"
wenzelm@2339
    72
[ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
wenzelm@2339
    73
wenzelm@4442
    74
wenzelm@4442
    75
# prepare log dir
wenzelm@4442
    76
wenzelm@4442
    77
LOGDIR="$ISABELLE_OUTPUT/log"
wenzelm@4442
    78
mkdir -p "$LOGDIR"
wenzelm@4442
    79
wenzelm@4442
    80
wenzelm@4442
    81
# run isabelle
wenzelm@4442
    82
wenzelm@18321
    83
. "$ISABELLE_HOME/lib/scripts/timestart.bash"
wenzelm@4442
    84
wenzelm@21996
    85
if [ -n "$RAW" ]; then
wenzelm@21996
    86
  ITEM="RAW"
wenzelm@21996
    87
  echo "Building $ITEM ..."
wenzelm@21996
    88
  LOG="$LOGDIR/$ITEM"
wenzelm@21996
    89
wenzelm@28502
    90
  "$ISABELLE_PROCESS" \
wenzelm@21996
    91
    -e "val ml_system = \"$ML_SYSTEM\";" \
wenzelm@21996
    92
    -e "val ml_platform = \"$ML_PLATFORM\";" \
wenzelm@21996
    93
    -e "use\"$COMPAT\" handle _ => exit 1;" \
wenzelm@30592
    94
    -e "structure Isar = struct fun main () = () end;" \
wenzelm@30611
    95
    -e "ml_prompts \"ML> \" \"ML# \";" \
wenzelm@21996
    96
    -q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1
wenzelm@21996
    97
  RC="$?"
wenzelm@21996
    98
elif [ -n "$RAW_SESSION" ]; then
wenzelm@21996
    99
  ITEM="RAW-$(basename $(dirname "$RAW_SESSION"))"
wenzelm@22011
   100
  echo "Running $ITEM ..."
wenzelm@21996
   101
  LOG="$LOGDIR/$ITEM"
wenzelm@21996
   102
wenzelm@28502
   103
  "$ISABELLE_PROCESS" \
wenzelm@21996
   104
    -e "use\"$RAW_SESSION\" handle _ => exit 1;" \
wenzelm@21996
   105
    -q RAW > "$LOG" 2>&1
wenzelm@21996
   106
  RC="$?"
wenzelm@21996
   107
else
wenzelm@4442
   108
  ITEM="Pure"
wenzelm@7277
   109
  echo "Building $ITEM ..."
wenzelm@4442
   110
  LOG="$LOGDIR/$ITEM"
wenzelm@4442
   111
wenzelm@28502
   112
  "$ISABELLE_PROCESS" \
wenzelm@3774
   113
    -e "val ml_system = \"$ML_SYSTEM\";" \
wenzelm@16376
   114
    -e "val ml_platform = \"$ML_PLATFORM\";" \
wenzelm@4495
   115
    -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
wenzelm@30611
   116
    -e "ml_prompts \"ML> \" \"ML# \";" \
wenzelm@31317
   117
    -f -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1
wenzelm@9789
   118
  RC="$?"
wenzelm@3774
   119
fi
wenzelm@4442
   120
wenzelm@18321
   121
. "$ISABELLE_HOME/lib/scripts/timestop.bash"
wenzelm@4442
   122
wenzelm@4442
   123
wenzelm@4442
   124
# exit status
wenzelm@4442
   125
wenzelm@9789
   126
if [ "$RC" -eq 0 ]; then
wenzelm@18321
   127
  echo "Finished $ITEM ($TIMES_REPORT)"
wenzelm@4442
   128
  gzip --force "$LOG"
wenzelm@4442
   129
else
wenzelm@7263
   130
  echo "$ITEM FAILED"
wenzelm@4442
   131
  echo "(see also $LOG)"
wenzelm@9789
   132
  echo; tail "$LOG"; echo
wenzelm@4442
   133
fi
wenzelm@4442
   134
wenzelm@9789
   135
exit "$RC"