| author | wenzelm |
| Thu Sep 02 00:48:07 2010 +0200 (2010-09-02) | |
| changeset 38980 | af73cf0dc31f |
| parent 34282 | 549969a7f582 |
| child 43948 | 8f5add916a99 |
| permissions | -rwxr-xr-x |
| 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" |