#!/usr/bin/env bash
#
# Author: Markus Wenzel, TU Muenchen
#
# mk - build Isabelle/Pure.
#
# Requires proper Isabelle settings environment.
## diagnostics
function usage()
{
echo
echo "Usage: $PRG [OPTIONS]"
echo
echo " Make Pure Isabelle."
echo
echo " -R DIR/FILE run RAW session"
echo " -r build RAW image"
echo
exit 1
}
function fail()
{
echo "$1" >&2
exit 2
}
## process command line
# options
RAW_SESSION=""
RAW=""
while getopts "R:r" OPT
do
case "$OPT" in
R)
RAW_SESSION="$OPTARG"
;;
r)
RAW=true
;;
\?)
usage
;;
esac
done
shift $(($OPTIND - 1))
# args
[ "$#" -ne 0 ] && usage
## main
# get compatibility file
ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
[ -z "$ML_SYSTEM" ] && fail "Missing ML_SYSTEM settings!"
COMPAT=""
[ -f "ML-Systems/$ML_SYSTEM_BASE.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM_BASE.ML"
[ -f "ML-Systems/$ML_SYSTEM.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM.ML"
[ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
# prepare log dir
LOGDIR="$ISABELLE_OUTPUT/log"
mkdir -p "$LOGDIR"
# run isabelle
. "$ISABELLE_HOME/lib/scripts/timestart.bash"
if [ -n "$RAW" ]; then
ITEM="RAW"
echo "Building $ITEM ..."
LOG="$LOGDIR/$ITEM"
"$ISABELLE_PROCESS" \
-e "val ml_system = \"$ML_SYSTEM\";" \
-e "val ml_platform = \"$ML_PLATFORM\";" \
-e "use\"$COMPAT\" handle _ => exit 1;" \
-e "structure Isar = struct fun main () = () end;" \
-e "ml_prompts \"ML> \" \"ML# \";" \
-q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1
RC="$?"
elif [ -n "$RAW_SESSION" ]; then
ITEM="RAW-$(basename $(dirname "$RAW_SESSION"))"
echo "Running $ITEM ..."
LOG="$LOGDIR/$ITEM"
"$ISABELLE_PROCESS" \
-e "use\"$RAW_SESSION\" handle _ => exit 1;" \
-q RAW > "$LOG" 2>&1
RC="$?"
else
ITEM="Pure"
echo "Building $ITEM ..."
LOG="$LOGDIR/$ITEM"
"$ISABELLE_PROCESS" \
-e "val ml_system = \"$ML_SYSTEM\";" \
-e "val ml_platform = \"$ML_PLATFORM\";" \
-e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
-e "ml_prompts \"ML> \" \"ML# \";" \
-f -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1
RC="$?"
fi
. "$ISABELLE_HOME/lib/scripts/timestop.bash"
# exit status
if [ "$RC" -eq 0 ]; then
echo "Finished $ITEM ($TIMES_REPORT)"
gzip --force "$LOG"
else
echo "$ITEM FAILED"
echo "(see also $LOG)"
echo; tail "$LOG"; echo
fi
exit "$RC"