author | wenzelm |
Thu, 26 Jul 2012 12:59:09 +0200 | |
changeset 49526 | 37999ee01156 |
parent 49462 | ef600ce4559c |
child 49677 | b171bcd5dd86 |
permissions | -rwxr-xr-x |
wenzelm@49375 | 1 |
#!/usr/bin/env bash |
wenzelm@49375 | 2 |
# |
wenzelm@49375 | 3 |
# Author: Makarius |
wenzelm@49375 | 4 |
# |
wenzelm@49375 | 5 |
# build - build Isabelle/ML |
wenzelm@49375 | 6 |
# |
wenzelm@49375 | 7 |
# Requires proper Isabelle settings environment. |
wenzelm@49375 | 8 |
|
wenzelm@49375 | 9 |
|
wenzelm@49375 | 10 |
## diagnostics |
wenzelm@49375 | 11 |
|
wenzelm@49375 | 12 |
function usage() |
wenzelm@49375 | 13 |
{ |
wenzelm@49375 | 14 |
echo |
wenzelm@49526 | 15 |
echo "Usage: $PRG TARGET [OUTPUT]" |
wenzelm@49375 | 16 |
echo |
wenzelm@49375 | 17 |
exit 1 |
wenzelm@49375 | 18 |
} |
wenzelm@49375 | 19 |
|
wenzelm@49375 | 20 |
function fail() |
wenzelm@49375 | 21 |
{ |
wenzelm@49375 | 22 |
echo "$1" >&2 |
wenzelm@49375 | 23 |
exit 2 |
wenzelm@49375 | 24 |
} |
wenzelm@49375 | 25 |
|
wenzelm@49375 | 26 |
[ -z "$ISABELLE_HOME" ] && fail "Missing Isabelle settings environment" |
wenzelm@49375 | 27 |
|
wenzelm@49375 | 28 |
|
wenzelm@49375 | 29 |
## process command line |
wenzelm@49375 | 30 |
|
wenzelm@49388 | 31 |
# args |
wenzelm@49388 | 32 |
|
wenzelm@49526 | 33 |
if [ "$#" -eq 1 ]; then |
wenzelm@49526 | 34 |
TARGET="$1"; shift |
wenzelm@49526 | 35 |
OUTPUT=""; shift |
wenzelm@49526 | 36 |
elif [ "$#" -eq 2 ]; then |
wenzelm@49462 | 37 |
TARGET="$1"; shift |
wenzelm@49462 | 38 |
OUTPUT="$1"; shift |
wenzelm@49462 | 39 |
else |
wenzelm@49462 | 40 |
usage |
wenzelm@49462 | 41 |
fi |
wenzelm@49375 | 42 |
|
wenzelm@49375 | 43 |
|
wenzelm@49375 | 44 |
## main |
wenzelm@49375 | 45 |
|
wenzelm@49375 | 46 |
# get compatibility file |
wenzelm@49375 | 47 |
|
wenzelm@49375 | 48 |
ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-) |
wenzelm@49375 | 49 |
[ -z "$ML_SYSTEM" ] && fail "Missing ML_SYSTEM settings!" |
wenzelm@49375 | 50 |
|
wenzelm@49375 | 51 |
COMPAT="" |
wenzelm@49375 | 52 |
[ -f "ML-Systems/${ML_SYSTEM_BASE}.ML" ] && COMPAT="ML-Systems/${ML_SYSTEM_BASE}.ML" |
wenzelm@49375 | 53 |
[ -f "ML-Systems/${ML_SYSTEM}.ML" ] && COMPAT="ML-Systems/${ML_SYSTEM}.ML" |
wenzelm@49375 | 54 |
[ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!" |
wenzelm@49375 | 55 |
|
wenzelm@49375 | 56 |
|
wenzelm@49375 | 57 |
# run isabelle |
wenzelm@49375 | 58 |
|
wenzelm@49375 | 59 |
. "$ISABELLE_HOME/lib/scripts/timestart.bash" |
wenzelm@49375 | 60 |
|
wenzelm@49388 | 61 |
if [ "$TARGET" = RAW ]; then |
wenzelm@49462 | 62 |
if [ -z "$OUTPUT" ]; then |
wenzelm@49388 | 63 |
"$ISABELLE_PROCESS" \ |
wenzelm@49432 | 64 |
-e "use\"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \ |
wenzelm@49388 | 65 |
-q RAW_ML_SYSTEM |
wenzelm@49388 | 66 |
else |
wenzelm@49388 | 67 |
"$ISABELLE_PROCESS" \ |
wenzelm@49432 | 68 |
-e "use\"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \ |
wenzelm@49388 | 69 |
-e "structure Isar = struct fun main () = () end;" \ |
wenzelm@49388 | 70 |
-e "ml_prompts \"ML> \" \"ML# \";" \ |
wenzelm@49462 | 71 |
-q -w RAW_ML_SYSTEM "$OUTPUT" |
wenzelm@49388 | 72 |
fi |
wenzelm@49388 | 73 |
else |
wenzelm@49462 | 74 |
if [ -z "$OUTPUT" ]; then |
wenzelm@49388 | 75 |
"$ISABELLE_PROCESS" \ |
wenzelm@49432 | 76 |
-e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \ |
wenzelm@49388 | 77 |
-q RAW_ML_SYSTEM |
wenzelm@49388 | 78 |
else |
wenzelm@49388 | 79 |
"$ISABELLE_PROCESS" \ |
wenzelm@49432 | 80 |
-e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \ |
wenzelm@49388 | 81 |
-e "ml_prompts \"ML> \" \"ML# \";" \ |
wenzelm@49462 | 82 |
-f -q -w RAW_ML_SYSTEM "$OUTPUT" |
wenzelm@49388 | 83 |
fi |
wenzelm@49388 | 84 |
fi |
wenzelm@49375 | 85 |
|
wenzelm@49388 | 86 |
RC="$?" |
wenzelm@49375 | 87 |
|
wenzelm@49375 | 88 |
. "$ISABELLE_HOME/lib/scripts/timestop.bash" |
wenzelm@49375 | 89 |
|
wenzelm@49375 | 90 |
if [ "$RC" -eq 0 ]; then |
wenzelm@49375 | 91 |
echo "Finished $TARGET ($TIMES_REPORT)" >&2 |
wenzelm@49375 | 92 |
fi |
wenzelm@49375 | 93 |
|
wenzelm@49375 | 94 |
exit "$RC" |