wenzelm@3007: #!/bin/bash
wenzelm@2808: #
wenzelm@2808: # $Id$
wenzelm@9788: # Author: Markus Wenzel, TU Muenchen
wenzelm@9788: # License: GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@2808: #
wenzelm@2808: # DESCRIPTION: build object-logic or run examples
wenzelm@2808: 
wenzelm@2808: 
wenzelm@2808: ## diagnostics
wenzelm@2808: 
wenzelm@10511: PRG="$(basename "$0")"
wenzelm@2808: 
wenzelm@2808: function usage()
wenzelm@2808: {
wenzelm@2808:   echo
wenzelm@9237:   echo "Usage: $PRG [OPTIONS] LOGIC NAME"
wenzelm@2808:   echo
wenzelm@2808:   echo "  Options are:"
wenzelm@8197:   echo "    -D PATH      dump generated document sources into PATH"
wenzelm@6940:   echo "    -P PATH      set path for remote theory browsing information"
wenzelm@6212:   echo "    -b           build mode (output heap image, using current dir)"
wenzelm@8359:   echo "    -c BOOL      tell ML system to compress output image (default true)"
wenzelm@7737:   echo "    -d FORMAT    build document as FORMAT (default false)"
berghofe@3747:   echo "    -i BOOL      generate theory browsing information,"
berghofe@3747:   echo "                 i.e. HTML / graph data (default false)"
wenzelm@6212:   echo "    -r           reset session path"
wenzelm@2808:   echo "    -s NAME      override session NAME"
wenzelm@2808:   echo
wenzelm@2808:   echo "  Build object-logic or run examples. Also creates browsing"
wenzelm@2808:   echo "  information (HTML etc.) according to settings."
wenzelm@2808:   echo
wenzelm@7461:   echo "  ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
wenzelm@7461:   echo
wenzelm@2808:   exit 1
wenzelm@2808: }
wenzelm@2808: 
wenzelm@2808: 
wenzelm@2808: ## process command line
wenzelm@2808: 
wenzelm@2808: # options
wenzelm@2808: 
wenzelm@8197: DUMP=""
wenzelm@8197: RPATH=""
wenzelm@2808: BUILD=""
wenzelm@8747: COMPRESS=true
wenzelm@7737: DOCUMENT=false
berghofe@3747: INFO=false
wenzelm@6212: RESET=false
wenzelm@2808: SESSION=""
wenzelm@2808: 
wenzelm@2917: function getoptions()
wenzelm@2917: {
wenzelm@2917:   OPTIND=1
wenzelm@8197:   while getopts "D:P:bc:d:i:rs:" OPT
wenzelm@2917:   do
wenzelm@2917:     case "$OPT" in
wenzelm@8197:       D)
wenzelm@8197:         DUMP="$OPTARG"
wenzelm@8197:         ;;
wenzelm@8197:       P)
wenzelm@8197:         RPATH="$OPTARG"
wenzelm@8197:         ;;
wenzelm@2917:       b)
wenzelm@2917:         BUILD=true
wenzelm@2917:         ;;
wenzelm@8359:       c)
wenzelm@8359:         COMPRESS="$OPTARG"
wenzelm@8359:         ;;
wenzelm@7737:       d)
wenzelm@7737:         DOCUMENT="$OPTARG"
wenzelm@7737:         ;;
berghofe@3747:       i)
berghofe@3747:         INFO="$OPTARG"
wenzelm@2917:         ;;
wenzelm@6212:       r)
wenzelm@6212:         RESET=true
wenzelm@6212:         ;;
wenzelm@2917:       s)
wenzelm@2917:         SESSION="$OPTARG"
wenzelm@2917:         ;;
wenzelm@2917:       \?)
wenzelm@2917:         usage
wenzelm@2917:         ;;
wenzelm@2917:     esac
wenzelm@2917:   done
wenzelm@2917: }
wenzelm@2808: 
wenzelm@2917: getoptions $ISABELLE_USEDIR_OPTIONS
wenzelm@2917: 
wenzelm@2917: getoptions "$@"
wenzelm@2808: shift $(($OPTIND - 1))
wenzelm@2808: 
wenzelm@2808: 
wenzelm@2808: # args
wenzelm@2808: 
wenzelm@9788: [ "$#" -ne 2 ] && usage
wenzelm@2808: 
wenzelm@2808: LOGIC="$1"; shift
wenzelm@2808: NAME="$1"; shift
wenzelm@2808: 
wenzelm@9788: [ -z "$SESSION" ] && SESSION=$(basename "$NAME")
wenzelm@2808: 
wenzelm@4419: 
wenzelm@4419: 
wenzelm@4419: ## main
berghofe@3636: 
wenzelm@4451: # prepare browser info dir
wenzelm@4419: 
wenzelm@9788: if [ "$INFO" = "true" -a ! -f "$ISABELLE_BROWSER_INFO/index.html" ]; then
wenzelm@9788:   mkdir -p "$ISABELLE_BROWSER_INFO"
wenzelm@9788:   cp "$ISABELLE_HOME/lib/logo/isabelle.gif" "$ISABELLE_BROWSER_INFO/isabelle.gif"
wenzelm@9788:   cp "$ISABELLE_HOME/lib/html/index.html" "$ISABELLE_BROWSER_INFO/index.html"
berghofe@3636: fi
berghofe@3636: 
wenzelm@2808: 
wenzelm@4451: # prepare log dir
wenzelm@4451: 
wenzelm@4451: LOGDIR="$ISABELLE_OUTPUT/log"
wenzelm@4451: mkdir -p "$LOGDIR"
wenzelm@4451: 
wenzelm@4451: 
wenzelm@4451: # run isabelle
wenzelm@4451: 
wenzelm@7737: PARENT=$(basename "$LOGIC")
wenzelm@7737: 
wenzelm@7737: [ -z "$BUILD" ] && cd "$NAME"
wenzelm@4451: 
wenzelm@8568: if [ "$DOCUMENT" != false -a -d document ]; then
wenzelm@8568:   DOC="$DOCUMENT"
wenzelm@9788:   [ -n "$DUMP" -a -d "$DUMP" ] && "$ISATOOL" latex -o sty "$DUMP/root.tex" >/dev/null
wenzelm@8568: else
wenzelm@8568:   DOC=""
wenzelm@8568: fi
wenzelm@7737: 
wenzelm@7737: 
wenzelm@7737: SECONDS=0
wenzelm@6249: 
wenzelm@2808: if [ -n "$BUILD" ]; then
wenzelm@4451:   ITEM="$SESSION"
wenzelm@7275:   echo "Building $ITEM ..."
wenzelm@4451:   LOG="$LOGDIR/$ITEM"
wenzelm@4451: 
wenzelm@8359:   OPT_C=""
wenzelm@8359:   [ "$COMPRESS" = true ] && OPT_C="-c"
wenzelm@8359: 
wenzelm@9788:   "$ISABELLE" \
wenzelm@8197:     -e "Session.use_dir $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\";" \
wenzelm@9788:     $OPT_C -q -w $LOGIC $NAME > "$LOG" 2>&1
wenzelm@9788:   RC="$?"
wenzelm@2808: else
wenzelm@9788:   ITEM=$(basename "$LOGIC")-"$SESSION"
wenzelm@7275:   echo "Running $ITEM ..."
wenzelm@4451:   LOG="$LOGDIR/$ITEM"
wenzelm@4451: 
wenzelm@9788:   "$ISABELLE" \
wenzelm@8197:     -e "Session.use_dir $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\"; quit();" \
wenzelm@9788:     -r -q "$LOGIC" > "$LOG" 2>&1
wenzelm@9788:   RC="$?"
wenzelm@6212:   cd ..
wenzelm@2808: fi
wenzelm@4451: 
wenzelm@9788: ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS")
wenzelm@4451: 
wenzelm@4451: 
wenzelm@4451: # exit status
wenzelm@4451: 
wenzelm@9788: if [ "$RC" -eq 0 ]; then
wenzelm@7275:   echo "Finished $ITEM ($ELAPSED elapsed time)"
wenzelm@4451:   gzip --force "$LOG"
wenzelm@4451: else
wenzelm@7259:   echo "$ITEM FAILED"
wenzelm@4451:   echo "(see also $LOG)"
wenzelm@9788:   echo; tail "$LOG"; echo
wenzelm@4451: fi
wenzelm@4451: 
wenzelm@9788: exit "$RC"