lib/Tools/usedir
author wenzelm
Sat Jul 25 10:31:27 2009 +0200 (2009-07-25)
changeset 32187 cca43ca13f4f
parent 32061 11f8ee55662d
child 32641 68c53dbceffd
permissions -rwxr-xr-x
renamed structure Display_Goal to Goal_Display;
     1 #!/usr/bin/env bash
     2 #
     3 # Author: Markus Wenzel, TU Muenchen
     4 #
     5 # DESCRIPTION: build object-logic or run examples
     6 
     7 
     8 ## diagnostics
     9 
    10 PRG="$(basename "$0")"
    11 
    12 function usage()
    13 {
    14   echo
    15   echo "Usage: isabelle $PRG [OPTIONS] LOGIC NAME"
    16   echo
    17   echo "  Options are:"
    18   echo "    -C BOOL      copy existing document directory to -D PATH (default true)"
    19   echo "    -D PATH      dump generated document sources into PATH"
    20   echo "    -M MAX       multithreading: maximum number of worker threads (default 1)"
    21   echo "    -P PATH      set path for remote theory browsing information"
    22   echo "    -T LEVEL     multithreading: trace level (default 0)"
    23   echo "    -V VERSION   declare alternative document VERSION"
    24   echo "    -b           build mode (output heap image, using current dir)"
    25   echo "    -d FORMAT    build document as FORMAT (default false)"
    26   echo "    -f NAME      use ML file NAME (default ROOT.ML)"
    27   echo "    -g BOOL      generate session graph image for document (default false)"
    28   echo "    -i BOOL      generate HTML and graph browser information (default false)"
    29   echo "    -m MODE      add print mode for output"
    30   echo "    -p LEVEL     set level of detail for proof objects (default 0)"
    31   echo "    -q LEVEL     set level of parallel proof checking (default 1)"
    32   echo "    -r           reset session path"
    33   echo "    -s NAME      override session NAME"
    34   echo "    -t BOOL      internal session timing (default false)"
    35   echo "    -v BOOL      be verbose (default false)"
    36   echo
    37   echo "  Build object-logic or run examples. Also creates browsing"
    38   echo "  information (HTML etc.) according to settings."
    39   echo
    40   echo "  ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
    41   echo "  HOL_USEDIR_OPTIONS=$HOL_USEDIR_OPTIONS"
    42   echo
    43   echo "  ML_PLATFORM=$ML_PLATFORM"
    44   echo "  ML_HOME=$ML_HOME"
    45   echo "  ML_SYSTEM=$ML_SYSTEM"
    46   echo "  ML_OPTIONS=$ML_OPTIONS"
    47   echo
    48   exit 1
    49 }
    50 
    51 function fail()
    52 {
    53   echo "$1" >&2
    54   exit 2
    55 }
    56 
    57 function check_bool()
    58 {
    59   [ "$1" = true -o "$1" = false ] || fail "Bad boolean: \"$1\""
    60 }
    61 
    62 function check_number()
    63 {
    64   [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
    65 }
    66 
    67 
    68 ## process command line
    69 
    70 # options
    71 
    72 COPY_DUMP=true
    73 DUMP=""
    74 MAXTHREADS="1"
    75 RPATH=""
    76 TRACETHREADS="0"
    77 DOCUMENT_VERSIONS=""
    78 BUILD=""
    79 DOCUMENT=false
    80 ROOT_FILE="ROOT.ML"
    81 DOCUMENT_GRAPH=false
    82 INFO=false
    83 MODES=""
    84 RESET=false
    85 SESSION=""
    86 PROOFS="0"
    87 PARALLEL_PROOFS="1"
    88 TIMING=false
    89 VERBOSE=false
    90 
    91 function getoptions()
    92 {
    93   OPTIND=1
    94   while getopts "C:D:M:P:T:V:bd:f:g:i:m:p:q:rs:t:v:" OPT
    95   do
    96     case "$OPT" in
    97       C)
    98         check_bool "$OPTARG"
    99         COPY_DUMP="$OPTARG"
   100         ;;
   101       D)
   102         DUMP="$OPTARG"
   103         ;;
   104       M)
   105         if [ "$OPTARG" = max ]; then
   106           MAXTHREADS=0
   107         else
   108           check_number "$OPTARG"
   109           MAXTHREADS="$OPTARG"
   110         fi
   111         ;;
   112       P)
   113         RPATH="$OPTARG"
   114         ;;
   115       T)
   116         check_number "$OPTARG"
   117         TRACETHREADS="$OPTARG"
   118         ;;
   119       V)
   120         if [ -z "$DOCUMENT_VERSIONS" ]; then
   121           DOCUMENT_VERSIONS="\"$OPTARG\""
   122         else
   123           DOCUMENT_VERSIONS="$DOCUMENT_VERSIONS, \"$OPTARG\""
   124         fi
   125         ;;
   126       b)
   127         BUILD=true
   128         ;;
   129       d)
   130         DOCUMENT="$OPTARG"
   131         ;;
   132       f)
   133         ROOT_FILE="$OPTARG"
   134         ;;
   135       g)
   136         check_bool "$OPTARG"
   137         DOCUMENT_GRAPH="$OPTARG"
   138         ;;
   139       i)
   140         check_bool "$OPTARG"
   141         INFO="$OPTARG"
   142         ;;
   143       m)
   144         if [ -z "$MODES" ]; then
   145           MODES="\"$OPTARG\""
   146         else
   147           MODES="\"$OPTARG\", $MODES"
   148         fi
   149         ;;
   150       p)
   151         check_number "$OPTARG"
   152         PROOFS="$OPTARG"
   153         ;;
   154       q)
   155         check_number "$OPTARG"
   156         PARALLEL_PROOFS="$OPTARG"
   157         ;;
   158       r)
   159         RESET=true
   160         ;;
   161       s)
   162         SESSION="$OPTARG"
   163         ;;
   164       t)
   165         check_bool "$OPTARG"
   166         TIMING="$OPTARG"
   167         ;;
   168       v)
   169         check_bool "$OPTARG"
   170         VERBOSE="$OPTARG"
   171         ;;
   172       \?)
   173         usage
   174         ;;
   175     esac
   176   done
   177 }
   178 
   179 eval "OPTIONS=($ISABELLE_USEDIR_OPTIONS)"
   180 getoptions "${OPTIONS[@]}"
   181 
   182 getoptions "$@"
   183 shift $(($OPTIND - 1))
   184 
   185 
   186 # args
   187 
   188 [ "$#" -ne 2 ] && usage
   189 
   190 LOGIC="$1"; shift
   191 NAME="$1"; shift
   192 
   193 [ -z "$SESSION" ] && SESSION=$(basename "$NAME")
   194 
   195 
   196 
   197 ## main
   198 
   199 # prepare browser info dir
   200 
   201 if [ "$INFO" = "true" -a ! -f "$ISABELLE_BROWSER_INFO/index.html" ]; then
   202   mkdir -p "$ISABELLE_BROWSER_INFO"
   203   cp "$ISABELLE_HOME/lib/logo/isabelle.gif" "$ISABELLE_BROWSER_INFO/isabelle.gif"
   204   cat "$ISABELLE_HOME/lib/html/library_index_header.template" \
   205     "$ISABELLE_HOME/lib/html/library_index_content.template" \
   206     "$ISABELLE_HOME/lib/html/library_index_footer.template"> "$ISABELLE_BROWSER_INFO/index.html"
   207 fi
   208 
   209 
   210 # prepare log dir
   211 
   212 LOGDIR="$ISABELLE_OUTPUT/log"
   213 mkdir -p "$LOGDIR"
   214 
   215 
   216 # run isabelle
   217 
   218 PARENT=$(basename "$LOGIC")
   219 
   220 if [ -z "$BUILD" ]; then
   221   cd "$NAME" || fail "Bad session directory '$NAME'"
   222 fi
   223 
   224 if [ "$DOCUMENT" != false ]; then
   225   DOC="$DOCUMENT"
   226 else
   227   DOC=""
   228 fi
   229 
   230 
   231 . "$ISABELLE_HOME/lib/scripts/timestart.bash"
   232 
   233 if [ -n "$BUILD" ]; then
   234   ITEM="$SESSION"
   235   echo "Building $ITEM ..." >&2
   236   LOG="$LOGDIR/$ITEM"
   237 
   238   "$ISABELLE_PROCESS" \
   239     -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS;" \
   240     -q -w $LOGIC $NAME > "$LOG"
   241   RC="$?"
   242 else
   243   ITEM=$(basename "$LOGIC")-"$SESSION"
   244   echo "Running $ITEM ..." >&2
   245   LOG="$LOGDIR/$ITEM"
   246 
   247   "$ISABELLE_PROCESS" \
   248     -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS; quit();" \
   249     -r -q "$LOGIC" > "$LOG"
   250   RC="$?"
   251   cd ..
   252 fi
   253 
   254 . "$ISABELLE_HOME/lib/scripts/timestop.bash"
   255 
   256 
   257 # exit status
   258 
   259 if [ "$RC" -eq 0 ]; then
   260   echo "Finished $ITEM ($TIMES_REPORT)" >&2
   261   gzip --force "$LOG"
   262 else
   263   { echo "$ITEM FAILED";
   264     echo "(see also $LOG)";
   265     echo; tail "$LOG"; echo; } >&2
   266 fi
   267 
   268 exit "$RC"