lib/Tools/usedir
author wenzelm
Wed Nov 22 21:41:39 2000 +0100 (2000-11-22)
changeset 10511 efb3428c9879
parent 9788 df671fa2562a
child 10555 2323ec838401
permissions -rwxr-xr-x
tuned;
     1 #!/bin/bash
     2 #
     3 # $Id$
     4 # Author: Markus Wenzel, TU Muenchen
     5 # License: GPL (GNU GENERAL PUBLIC LICENSE)
     6 #
     7 # DESCRIPTION: build object-logic or run examples
     8 
     9 
    10 ## diagnostics
    11 
    12 PRG="$(basename "$0")"
    13 
    14 function usage()
    15 {
    16   echo
    17   echo "Usage: $PRG [OPTIONS] LOGIC NAME"
    18   echo
    19   echo "  Options are:"
    20   echo "    -D PATH      dump generated document sources into PATH"
    21   echo "    -P PATH      set path for remote theory browsing information"
    22   echo "    -b           build mode (output heap image, using current dir)"
    23   echo "    -c BOOL      tell ML system to compress output image (default true)"
    24   echo "    -d FORMAT    build document as FORMAT (default false)"
    25   echo "    -i BOOL      generate theory browsing information,"
    26   echo "                 i.e. HTML / graph data (default false)"
    27   echo "    -r           reset session path"
    28   echo "    -s NAME      override session NAME"
    29   echo
    30   echo "  Build object-logic or run examples. Also creates browsing"
    31   echo "  information (HTML etc.) according to settings."
    32   echo
    33   echo "  ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
    34   echo
    35   exit 1
    36 }
    37 
    38 
    39 ## process command line
    40 
    41 # options
    42 
    43 DUMP=""
    44 RPATH=""
    45 BUILD=""
    46 COMPRESS=true
    47 DOCUMENT=false
    48 INFO=false
    49 RESET=false
    50 SESSION=""
    51 
    52 function getoptions()
    53 {
    54   OPTIND=1
    55   while getopts "D:P:bc:d:i:rs:" OPT
    56   do
    57     case "$OPT" in
    58       D)
    59         DUMP="$OPTARG"
    60         ;;
    61       P)
    62         RPATH="$OPTARG"
    63         ;;
    64       b)
    65         BUILD=true
    66         ;;
    67       c)
    68         COMPRESS="$OPTARG"
    69         ;;
    70       d)
    71         DOCUMENT="$OPTARG"
    72         ;;
    73       i)
    74         INFO="$OPTARG"
    75         ;;
    76       r)
    77         RESET=true
    78         ;;
    79       s)
    80         SESSION="$OPTARG"
    81         ;;
    82       \?)
    83         usage
    84         ;;
    85     esac
    86   done
    87 }
    88 
    89 getoptions $ISABELLE_USEDIR_OPTIONS
    90 
    91 getoptions "$@"
    92 shift $(($OPTIND - 1))
    93 
    94 
    95 # args
    96 
    97 [ "$#" -ne 2 ] && usage
    98 
    99 LOGIC="$1"; shift
   100 NAME="$1"; shift
   101 
   102 [ -z "$SESSION" ] && SESSION=$(basename "$NAME")
   103 
   104 
   105 
   106 ## main
   107 
   108 # prepare browser info dir
   109 
   110 if [ "$INFO" = "true" -a ! -f "$ISABELLE_BROWSER_INFO/index.html" ]; then
   111   mkdir -p "$ISABELLE_BROWSER_INFO"
   112   cp "$ISABELLE_HOME/lib/logo/isabelle.gif" "$ISABELLE_BROWSER_INFO/isabelle.gif"
   113   cp "$ISABELLE_HOME/lib/html/index.html" "$ISABELLE_BROWSER_INFO/index.html"
   114 fi
   115 
   116 
   117 # prepare log dir
   118 
   119 LOGDIR="$ISABELLE_OUTPUT/log"
   120 mkdir -p "$LOGDIR"
   121 
   122 
   123 # run isabelle
   124 
   125 PARENT=$(basename "$LOGIC")
   126 
   127 [ -z "$BUILD" ] && cd "$NAME"
   128 
   129 if [ "$DOCUMENT" != false -a -d document ]; then
   130   DOC="$DOCUMENT"
   131   [ -n "$DUMP" -a -d "$DUMP" ] && "$ISATOOL" latex -o sty "$DUMP/root.tex" >/dev/null
   132 else
   133   DOC=""
   134 fi
   135 
   136 
   137 SECONDS=0
   138 
   139 if [ -n "$BUILD" ]; then
   140   ITEM="$SESSION"
   141   echo "Building $ITEM ..."
   142   LOG="$LOGDIR/$ITEM"
   143 
   144   OPT_C=""
   145   [ "$COMPRESS" = true ] && OPT_C="-c"
   146 
   147   "$ISABELLE" \
   148     -e "Session.use_dir $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\";" \
   149     $OPT_C -q -w $LOGIC $NAME > "$LOG" 2>&1
   150   RC="$?"
   151 else
   152   ITEM=$(basename "$LOGIC")-"$SESSION"
   153   echo "Running $ITEM ..."
   154   LOG="$LOGDIR/$ITEM"
   155 
   156   "$ISABELLE" \
   157     -e "Session.use_dir $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\"; quit();" \
   158     -r -q "$LOGIC" > "$LOG" 2>&1
   159   RC="$?"
   160   cd ..
   161 fi
   162 
   163 ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS")
   164 
   165 
   166 # exit status
   167 
   168 if [ "$RC" -eq 0 ]; then
   169   echo "Finished $ITEM ($ELAPSED elapsed time)"
   170   gzip --force "$LOG"
   171 else
   172   echo "$ITEM FAILED"
   173   echo "(see also $LOG)"
   174   echo; tail "$LOG"; echo
   175 fi
   176 
   177 exit "$RC"