lib/Tools/usedir
author wenzelm
Wed Feb 03 17:30:17 1999 +0100 (1999-02-03)
changeset 6212 974310f9ca7d
parent 5034 8e43dab90429
child 6249 8bb90076cc7c
permissions -rwxr-xr-x
Session.init;
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@6212
    18
  echo "    -b           build mode (output heap image, using current dir)"
berghofe@3747
    19
  echo "    -i BOOL      generate theory browsing information,"
berghofe@3747
    20
  echo "                 i.e. HTML / graph data (default false)"
wenzelm@6212
    21
  echo "    -r           reset session path"
wenzelm@2808
    22
  echo "    -s NAME      override session NAME"
wenzelm@2808
    23
  echo
wenzelm@2808
    24
  echo "  Build object-logic or run examples. Also creates browsing"
wenzelm@2808
    25
  echo "  information (HTML etc.) according to settings."
wenzelm@2808
    26
  echo
wenzelm@2808
    27
  exit 1
wenzelm@2808
    28
}
wenzelm@2808
    29
wenzelm@2808
    30
wenzelm@2808
    31
## process command line
wenzelm@2808
    32
wenzelm@2808
    33
# options
wenzelm@2808
    34
wenzelm@2808
    35
BUILD=""
berghofe@3747
    36
INFO=false
wenzelm@6212
    37
RESET=false
wenzelm@2808
    38
SESSION=""
wenzelm@2808
    39
wenzelm@2917
    40
function getoptions()
wenzelm@2917
    41
{
wenzelm@2917
    42
  OPTIND=1
wenzelm@6212
    43
  while getopts "bi:rs:" OPT
wenzelm@2917
    44
  do
wenzelm@2917
    45
    case "$OPT" in
wenzelm@2917
    46
      b)
wenzelm@2917
    47
        BUILD=true
wenzelm@2917
    48
        ;;
berghofe@3747
    49
      i)
berghofe@3747
    50
        INFO="$OPTARG"
wenzelm@2917
    51
        ;;
wenzelm@6212
    52
      r)
wenzelm@6212
    53
        RESET=true
wenzelm@6212
    54
        ;;
wenzelm@2917
    55
      s)
wenzelm@2917
    56
        SESSION="$OPTARG"
wenzelm@2917
    57
        ;;
wenzelm@2917
    58
      \?)
wenzelm@2917
    59
        usage
wenzelm@2917
    60
        ;;
wenzelm@2917
    61
    esac
wenzelm@2917
    62
  done
wenzelm@2917
    63
}
wenzelm@2808
    64
wenzelm@2917
    65
getoptions $ISABELLE_USEDIR_OPTIONS
wenzelm@2917
    66
wenzelm@2917
    67
getoptions "$@"
wenzelm@2808
    68
shift $(($OPTIND - 1))
wenzelm@2808
    69
wenzelm@2808
    70
wenzelm@2808
    71
# args
wenzelm@2808
    72
wenzelm@2808
    73
[ $# -ne 2 ] && usage
wenzelm@2808
    74
wenzelm@2808
    75
LOGIC="$1"; shift
wenzelm@2808
    76
NAME="$1"; shift
wenzelm@2808
    77
wenzelm@4419
    78
[ -z "$SESSION" ] && SESSION=$(basename $NAME)
wenzelm@2808
    79
wenzelm@4419
    80
wenzelm@4419
    81
wenzelm@4419
    82
## main
berghofe@3636
    83
wenzelm@4451
    84
# prepare browser info dir
wenzelm@4419
    85
wenzelm@4586
    86
if [ "$INFO" = "true" -a ! -f $ISABELLE_BROWSER_INFO/index.html ]; then
wenzelm@4419
    87
berghofe@3747
    88
  mkdir -p $ISABELLE_BROWSER_INFO/gif
wenzelm@4419
    89
  cp $ISABELLE_HOME/lib/images/blue_arrow.gif $ISABELLE_BROWSER_INFO/gif
wenzelm@4419
    90
  cp $ISABELLE_HOME/lib/images/red_arrow.gif $ISABELLE_BROWSER_INFO/gif
wenzelm@3848
    91
  cp $ISABELLE_HOME/lib/logo/isabelle.gif $ISABELLE_BROWSER_INFO/gif/isabelle.gif
berghofe@3747
    92
  cp $ISABELLE_HOME/lib/html/index1.html $ISABELLE_BROWSER_INFO/index.html
wenzelm@4419
    93
berghofe@3636
    94
  mkdir -p $ISABELLE_BROWSER_INFO/graph
berghofe@3636
    95
  cp $ISABELLE_HOME/lib/html/index2.html $ISABELLE_BROWSER_INFO/graph/index.html
berghofe@3636
    96
  mkdir $ISABELLE_BROWSER_INFO/graph/GraphBrowser
berghofe@3636
    97
  mkdir $ISABELLE_BROWSER_INFO/graph/awtUtilities
wenzelm@4419
    98
  cp $ISABELLE_HOME/lib/browser/GraphBrowser/*.class $ISABELLE_BROWSER_INFO/graph/GraphBrowser
wenzelm@4419
    99
  cp $ISABELLE_HOME/lib/browser/awtUtilities/*.class $ISABELLE_BROWSER_INFO/graph/awtUtilities
wenzelm@4419
   100
berghofe@3636
   101
fi
berghofe@3636
   102
wenzelm@2808
   103
wenzelm@4451
   104
# prepare log dir
wenzelm@4451
   105
wenzelm@4451
   106
LOGDIR="$ISABELLE_OUTPUT/log"
wenzelm@4451
   107
mkdir -p "$LOGDIR"
wenzelm@4451
   108
wenzelm@4451
   109
wenzelm@4451
   110
# run isabelle
wenzelm@4451
   111
wenzelm@4451
   112
SECONDS=0
wenzelm@4451
   113
wenzelm@2808
   114
if [ -n "$BUILD" ]; then
wenzelm@4451
   115
  ITEM="$SESSION"
wenzelm@4451
   116
  echo -n "Building $ITEM ... "
wenzelm@4451
   117
  LOG="$LOGDIR/$ITEM"
wenzelm@4451
   118
wenzelm@4451
   119
  $ISABELLE \
wenzelm@6212
   120
    -e "Session.use_dir $RESET $INFO \"$SESSION\";" \
wenzelm@4492
   121
    -q -w $LOGIC $NAME > $LOG 2>&1
wenzelm@2808
   122
else
wenzelm@4451
   123
  ITEM=$(basename $LOGIC)-"$SESSION"
wenzelm@4451
   124
  echo -n "Running $ITEM ... "
wenzelm@4451
   125
  LOG="$LOGDIR/$ITEM"
wenzelm@4451
   126
wenzelm@6212
   127
  cd "$NAME"
wenzelm@4451
   128
  $ISABELLE \
wenzelm@6212
   129
    -e "Session.use_dir $RESET $INFO \"$SESSION\"; quit();" \
wenzelm@4492
   130
    -r -q $LOGIC > $LOG 2>&1
wenzelm@6212
   131
  cd ..
wenzelm@2808
   132
fi
wenzelm@4451
   133
wenzelm@4451
   134
RC=$?
wenzelm@4451
   135
wenzelm@4451
   136
ELAPSED=$($ISABELLE_HOME/lib/scripts/showtime $SECONDS)
wenzelm@4451
   137
wenzelm@4451
   138
wenzelm@4451
   139
# exit status
wenzelm@4451
   140
wenzelm@4451
   141
if [ $RC -eq 0 ]; then
wenzelm@4451
   142
  echo "OK  ($ELAPSED elapsed time)"
wenzelm@4451
   143
  gzip --force "$LOG"
wenzelm@4451
   144
else
wenzelm@4451
   145
  echo "FAILED"
wenzelm@4451
   146
  echo "(see also $LOG)"
wenzelm@4451
   147
  echo; tail $LOG; echo
wenzelm@4451
   148
fi
wenzelm@4451
   149
wenzelm@4451
   150
exit $RC