#!/usr/bin/env bash
#
# Author: Markus Wenzel, TU Muenchen
#
# DESCRIPTION: build object-logic or run examples
## diagnostics
PRG="$(basename "$0")"
function usage()
{
echo
echo "Usage: isabelle $PRG [OPTIONS] LOGIC NAME"
echo
echo " Options are:"
echo " -C BOOL copy existing document directory to -D PATH (default true)"
echo " -D PATH dump generated document sources into PATH"
echo " -M MAX multithreading: maximum number of worker threads (default 1)"
echo " -P PATH set path for remote theory browsing information"
echo " -Q BOOL check proofs in parallel (default true)"
echo " -T LEVEL multithreading: trace level (default 0)"
echo " -V VERSION declare alternative document VERSION"
echo " -b build mode (output heap image, using current dir)"
echo " -c BOOL tell ML system to compress output image (default true)"
echo " -d FORMAT build document as FORMAT (default false)"
echo " -f NAME use ML file NAME (default ROOT.ML)"
echo " -g BOOL generate session graph image for document (default false)"
echo " -i BOOL generate HTML and graph browser information (default false)"
echo " -m MODE add print mode for output"
echo " -p LEVEL set level of detail for proof objects"
echo " -r reset session path"
echo " -s NAME override session NAME"
echo " -v BOOL be verbose (default false)"
echo
echo " Build object-logic or run examples. Also creates browsing"
echo " information (HTML etc.) according to settings."
echo
echo " ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
echo " HOL_USEDIR_OPTIONS=$HOL_USEDIR_OPTIONS"
echo
echo " ML_PLATFORM=$ML_PLATFORM"
echo " ML_HOME=$ML_HOME"
echo " ML_SYSTEM=$ML_SYSTEM"
echo " ML_OPTIONS=$ML_OPTIONS"
echo
exit 1
}
function fail()
{
echo "$1" >&2
exit 2
}
function check_bool()
{
[ "$1" = true -o "$1" = false ] || fail "Bad boolean: \"$1\""
}
function check_number()
{
[ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
}
## process command line
# options
COPY_DUMP=true
DUMP=""
MAXTHREADS="1"
RPATH=""
PARALLEL_PROOFS="true"
TRACETHREADS="0"
DOCUMENT_VERSIONS=""
BUILD=""
COMPRESS=true
DOCUMENT=false
ROOT_FILE="ROOT.ML"
DOCUMENT_GRAPH=false
INFO=false
MODES=""
RESET=false
SESSION=""
PROOFS=0
VERBOSE=false
function getoptions()
{
OPTIND=1
while getopts "C:D:M:P:Q:T:V:bc:d:f:g:i:m:p:rs:v:" OPT
do
case "$OPT" in
C)
check_bool "$OPTARG"
COPY_DUMP="$OPTARG"
;;
D)
DUMP="$OPTARG"
;;
M)
if [ "$OPTARG" = max ]; then
MAXTHREADS=0
else
check_number "$OPTARG"
MAXTHREADS="$OPTARG"
fi
;;
P)
RPATH="$OPTARG"
;;
Q)
PARALLEL_PROOFS="$OPTARG"
;;
T)
check_number "$OPTARG"
TRACETHREADS="$OPTARG"
;;
V)
if [ -z "$DOCUMENT_VERSIONS" ]; then
DOCUMENT_VERSIONS="\"$OPTARG\""
else
DOCUMENT_VERSIONS="$DOCUMENT_VERSIONS, \"$OPTARG\""
fi
;;
b)
BUILD=true
;;
c)
check_bool "$OPTARG"
COMPRESS="$OPTARG"
;;
d)
DOCUMENT="$OPTARG"
;;
f)
ROOT_FILE="$OPTARG"
;;
g)
check_bool "$OPTARG"
DOCUMENT_GRAPH="$OPTARG"
;;
i)
check_bool "$OPTARG"
INFO="$OPTARG"
;;
m)
if [ -z "$MODES" ]; then
MODES="\"$OPTARG\""
else
MODES="\"$OPTARG\", $MODES"
fi
;;
p)
check_number "$OPTARG"
PROOFS="$OPTARG"
;;
r)
RESET=true
;;
s)
SESSION="$OPTARG"
;;
v)
check_bool "$OPTARG"
VERBOSE="$OPTARG"
;;
\?)
usage
;;
esac
done
}
getoptions $ISABELLE_USEDIR_OPTIONS
getoptions "$@"
shift $(($OPTIND - 1))
# args
[ "$#" -ne 2 ] && usage
LOGIC="$1"; shift
NAME="$1"; shift
[ -z "$SESSION" ] && SESSION=$(basename "$NAME")
## main
# prepare browser info dir
if [ "$INFO" = "true" -a ! -f "$ISABELLE_BROWSER_INFO/index.html" ]; then
mkdir -p "$ISABELLE_BROWSER_INFO"
cp "$ISABELLE_HOME/lib/logo/isabelle.gif" "$ISABELLE_BROWSER_INFO/isabelle.gif"
cat "$ISABELLE_HOME/lib/html/library_index_header.template" \
"$ISABELLE_HOME/lib/html/library_index_content.template" \
"$ISABELLE_HOME/lib/html/library_index_footer.template"> "$ISABELLE_BROWSER_INFO/index.html"
fi
# prepare log dir
LOGDIR="$ISABELLE_OUTPUT/log"
mkdir -p "$LOGDIR"
# run isabelle
PARENT=$(basename "$LOGIC")
if [ -z "$BUILD" ]; then
cd "$NAME" || fail "Bad session directory '$NAME'"
fi
if [ "$DOCUMENT" != false ]; then
DOC="$DOCUMENT"
else
DOC=""
fi
. "$ISABELLE_HOME/lib/scripts/timestart.bash"
if [ -n "$BUILD" ]; then
ITEM="$SESSION"
echo "Building $ITEM ..." >&2
LOG="$LOGDIR/$ITEM"
OPT_C=""
[ "$COMPRESS" = true ] && OPT_C="-c"
"$ISABELLE_PROCESS" \
-e "Session.use_dir \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS;" \
$OPT_C -q -w $LOGIC $NAME > "$LOG"
RC="$?"
else
ITEM=$(basename "$LOGIC")-"$SESSION"
echo "Running $ITEM ..." >&2
LOG="$LOGDIR/$ITEM"
"$ISABELLE_PROCESS" \
-e "Session.use_dir \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS; quit();" \
-r -q "$LOGIC" > "$LOG"
RC="$?"
cd ..
fi
. "$ISABELLE_HOME/lib/scripts/timestop.bash"
# exit status
if [ "$RC" -eq 0 ]; then
echo "Finished $ITEM ($TIMES_REPORT)" >&2
gzip --force "$LOG"
else
{ echo "$ITEM FAILED";
echo "(see also $LOG)";
echo; tail "$LOG"; echo; } >&2
fi
exit "$RC"