--- a/lib/Tools/usedir Fri May 17 17:45:51 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,273 +0,0 @@
-#!/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 INT set threshold for sub-proof parallelization (default 100)"
- echo " -T LEVEL multithreading: trace level (default 0)"
- echo " -V VARIANT declare alternative document VARIANT"
- echo " -b build mode (output heap image, using current dir)"
- 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 (default 0)"
- echo " -q LEVEL set level of parallel proof checking (default 1)"
- echo " -r reset session path"
- echo " -s NAME override session NAME"
- echo " -t BOOL internal session timing (default false)"
- 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
- 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=""
-TRACETHREADS="0"
-DOCUMENT_VARIANTS=""
-BUILD=""
-DOCUMENT=false
-ROOT_FILE="ROOT.ML"
-DOCUMENT_GRAPH=false
-INFO=false
-MODES=""
-RESET=false
-SESSION=""
-PROOFS="0"
-PARALLEL_PROOFS="1"
-PARALLEL_PROOFS_THRESHOLD="100"
-TIMING=false
-VERBOSE=false
-
-function getoptions()
-{
- OPTIND=1
- while getopts "C:D:M:P:Q:T:V:bd:f:g:i:m:p:q:rs:t: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)
- check_number "$OPTARG"
- PARALLEL_PROOFS_THRESHOLD="$OPTARG"
- ;;
- T)
- check_number "$OPTARG"
- TRACETHREADS="$OPTARG"
- ;;
- V)
- if [ -z "$DOCUMENT_VARIANTS" ]; then
- DOCUMENT_VARIANTS="\"$OPTARG\""
- else
- DOCUMENT_VARIANTS="$DOCUMENT_VARIANTS, \"$OPTARG\""
- fi
- ;;
- b)
- BUILD=true
- ;;
- 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"
- ;;
- q)
- check_number "$OPTARG"
- PARALLEL_PROOFS="$OPTARG"
- ;;
- r)
- RESET=true
- ;;
- s)
- SESSION="$OPTARG"
- ;;
- t)
- check_bool "$OPTARG"
- TIMING="$OPTARG"
- ;;
- v)
- check_bool "$OPTARG"
- VERBOSE="$OPTARG"
- ;;
- \?)
- usage
- ;;
- esac
- done
-}
-
-eval "OPTIONS=($ISABELLE_USEDIR_OPTIONS)"
-getoptions "${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"
-
- "$ISABELLE_PROCESS" \
- -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$ISABELLE_BROWSER_INFO\" \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD;" \
- -q -w $LOGIC $NAME > "$LOG"
- RC="$?"
-else
- ITEM=$(basename "$LOGIC")-"$SESSION"
- echo "Running $ITEM ..." >&2
- LOG="$LOGDIR/$ITEM"
-
- "$ISABELLE_PROCESS" \
- -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$ISABELLE_BROWSER_INFO\" \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD; 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 -20 "$LOG"; echo; } >&2
-fi
-
-exit "$RC"