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