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