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