lib/Tools/usedir
author wenzelm
Mon Jan 04 11:55:23 2010 +0100 (2010-01-04 ago)
changeset 34238 b28be884edda
parent 33830 1b634d37aa64
child 34261 8e36b3ac6083
permissions -rwxr-xr-x
discontinued special HOL_USEDIR_OPTIONS;
     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
    42   echo "  ML_PLATFORM=$ML_PLATFORM"
    43   echo "  ML_HOME=$ML_HOME"
    44   echo "  ML_SYSTEM=$ML_SYSTEM"
    45   echo "  ML_OPTIONS=$ML_OPTIONS"
    46   echo
    47   exit 1
    48 }
    49 
    50 function fail()
    51 {
    52   echo "$1" >&2
    53   exit 2
    54 }
    55 
    56 function check_bool()
    57 {
    58   [ "$1" = true -o "$1" = false ] || fail "Bad boolean: \"$1\""
    59 }
    60 
    61 function check_number()
    62 {
    63   [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
    64 }
    65 
    66 
    67 ## process command line
    68 
    69 # options
    70 
    71 COPY_DUMP=true
    72 DUMP=""
    73 MAXTHREADS="1"
    74 RPATH=""
    75 TRACETHREADS="0"
    76 DOCUMENT_VERSIONS=""
    77 BUILD=""
    78 DOCUMENT=false
    79 ROOT_FILE="ROOT.ML"
    80 DOCUMENT_GRAPH=false
    81 INFO=false
    82 MODES=""
    83 RESET=false
    84 SESSION=""
    85 PROOFS="0"
    86 PARALLEL_PROOFS="1"
    87 TIMING=false
    88 VERBOSE=false
    89 
    90 function getoptions()
    91 {
    92   OPTIND=1
    93   while getopts "C:D:M:P:T:V:bd:f:g:i:m:p:q:rs:t:v:" OPT
    94   do
    95     case "$OPT" in
    96       C)
    97         check_bool "$OPTARG"
    98         COPY_DUMP="$OPTARG"
    99         ;;
   100       D)
   101         DUMP="$OPTARG"
   102         ;;
   103       M)
   104         if [ "$OPTARG" = max ]; then
   105           MAXTHREADS=0
   106         else
   107           check_number "$OPTARG"
   108           MAXTHREADS="$OPTARG"
   109         fi
   110         ;;
   111       P)
   112         RPATH="$OPTARG"
   113         ;;
   114       T)
   115         check_number "$OPTARG"
   116         TRACETHREADS="$OPTARG"
   117         ;;
   118       V)
   119         if [ -z "$DOCUMENT_VERSIONS" ]; then
   120           DOCUMENT_VERSIONS="\"$OPTARG\""
   121         else
   122           DOCUMENT_VERSIONS="$DOCUMENT_VERSIONS, \"$OPTARG\""
   123         fi
   124         ;;
   125       b)
   126         BUILD=true
   127         ;;
   128       d)
   129         DOCUMENT="$OPTARG"
   130         ;;
   131       f)
   132         ROOT_FILE="$OPTARG"
   133         ;;
   134       g)
   135         check_bool "$OPTARG"
   136         DOCUMENT_GRAPH="$OPTARG"
   137         ;;
   138       i)
   139         check_bool "$OPTARG"
   140         INFO="$OPTARG"
   141         ;;
   142       m)
   143         if [ -z "$MODES" ]; then
   144           MODES="\"$OPTARG\""
   145         else
   146           MODES="\"$OPTARG\", $MODES"
   147         fi
   148         ;;
   149       p)
   150         check_number "$OPTARG"
   151         PROOFS="$OPTARG"
   152         ;;
   153       q)
   154         check_number "$OPTARG"
   155         PARALLEL_PROOFS="$OPTARG"
   156         ;;
   157       r)
   158         RESET=true
   159         ;;
   160       s)
   161         SESSION="$OPTARG"
   162         ;;
   163       t)
   164         check_bool "$OPTARG"
   165         TIMING="$OPTARG"
   166         ;;
   167       v)
   168         check_bool "$OPTARG"
   169         VERBOSE="$OPTARG"
   170         ;;
   171       \?)
   172         usage
   173         ;;
   174     esac
   175   done
   176 }
   177 
   178 eval "OPTIONS=($ISABELLE_USEDIR_OPTIONS)"
   179 getoptions "${OPTIONS[@]}"
   180 
   181 getoptions "$@"
   182 shift $(($OPTIND - 1))
   183 
   184 
   185 # args
   186 
   187 [ "$#" -ne 2 ] && usage
   188 
   189 LOGIC="$1"; shift
   190 NAME="$1"; shift
   191 
   192 [ -z "$SESSION" ] && SESSION=$(basename "$NAME")
   193 
   194 
   195 
   196 ## main
   197 
   198 # prepare browser info dir
   199 
   200 if [ "$INFO" = "true" -a ! -f "$ISABELLE_BROWSER_INFO/index.html" ]; then
   201   mkdir -p "$ISABELLE_BROWSER_INFO"
   202   cp "$ISABELLE_HOME/lib/logo/isabelle.gif" "$ISABELLE_BROWSER_INFO/isabelle.gif"
   203   cat "$ISABELLE_HOME/lib/html/library_index_header.template" \
   204     "$ISABELLE_HOME/lib/html/library_index_content.template" \
   205     "$ISABELLE_HOME/lib/html/library_index_footer.template"> "$ISABELLE_BROWSER_INFO/index.html"
   206 fi
   207 
   208 
   209 # prepare log dir
   210 
   211 LOGDIR="$ISABELLE_OUTPUT/log"
   212 mkdir -p "$LOGDIR"
   213 
   214 
   215 # run isabelle
   216 
   217 PARENT=$(basename "$LOGIC")
   218 
   219 if [ -z "$BUILD" ]; then
   220   cd "$NAME" || fail "Bad session directory '$NAME'"
   221 fi
   222 
   223 if [ "$DOCUMENT" != false ]; then
   224   DOC="$DOCUMENT"
   225 else
   226   DOC=""
   227 fi
   228 
   229 
   230 . "$ISABELLE_HOME/lib/scripts/timestart.bash"
   231 
   232 if [ -n "$BUILD" ]; then
   233   ITEM="$SESSION"
   234   echo "Building $ITEM ..." >&2
   235   LOG="$LOGDIR/$ITEM"
   236 
   237   "$ISABELLE_PROCESS" \
   238     -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;" \
   239     -q -w $LOGIC $NAME > "$LOG"
   240   RC="$?"
   241 else
   242   ITEM=$(basename "$LOGIC")-"$SESSION"
   243   echo "Running $ITEM ..." >&2
   244   LOG="$LOGDIR/$ITEM"
   245 
   246   "$ISABELLE_PROCESS" \
   247     -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();" \
   248     -r -q "$LOGIC" > "$LOG"
   249   RC="$?"
   250   cd ..
   251 fi
   252 
   253 . "$ISABELLE_HOME/lib/scripts/timestop.bash"
   254 
   255 
   256 # exit status
   257 
   258 if [ "$RC" -eq 0 ]; then
   259   echo "Finished $ITEM ($TIMES_REPORT)" >&2
   260   gzip --force "$LOG"
   261 else
   262   { echo "$ITEM FAILED";
   263     echo "(see also $LOG)";
   264     echo; tail -40 "$LOG"; echo; } >&2
   265 fi
   266 
   267 exit "$RC"