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