lib/Tools/usedir
author wenzelm
Tue Oct 05 15:42:44 1999 +0200 (1999-10-05)
changeset 7737 acaf55bee03e
parent 7461 94ae093f6706
child 7787 b43b1c4f27ce
permissions -rwxr-xr-x
document preparation options: -c -d;
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@6940
    18
  echo "    -B           build mode with THIS_IS_ISABELLE_BUILD indication"
wenzelm@6940
    19
  echo "    -P PATH      set path for remote theory browsing information"
wenzelm@7737
    20
  echo "    -c BOOL      clean document source after build (default true)"
wenzelm@6212
    21
  echo "    -b           build mode (output heap image, using current dir)"
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@2808
    41
BUILD=""
wenzelm@7737
    42
CLEANDOC=true
wenzelm@7737
    43
DOCUMENT=false
berghofe@3747
    44
INFO=false
wenzelm@6212
    45
RESET=false
wenzelm@2808
    46
SESSION=""
berghofe@6652
    47
RPATH=""
wenzelm@2808
    48
wenzelm@2917
    49
function getoptions()
wenzelm@2917
    50
{
wenzelm@2917
    51
  OPTIND=1
wenzelm@7737
    52
  while getopts "BP:bc:d:i:rs:" OPT
wenzelm@2917
    53
  do
wenzelm@2917
    54
    case "$OPT" in
wenzelm@6940
    55
      B)
wenzelm@6940
    56
        BUILD=true
wenzelm@6940
    57
        export THIS_IS_ISABELLE_BUILD=true
wenzelm@6940
    58
        ;;
wenzelm@2917
    59
      b)
wenzelm@2917
    60
        BUILD=true
wenzelm@2917
    61
        ;;
wenzelm@7737
    62
      c)
wenzelm@7737
    63
        CLEANDOC="$OPTARG"
wenzelm@7737
    64
        ;;
wenzelm@7737
    65
      d)
wenzelm@7737
    66
        DOCUMENT="$OPTARG"
wenzelm@7737
    67
        ;;
berghofe@3747
    68
      i)
berghofe@3747
    69
        INFO="$OPTARG"
wenzelm@2917
    70
        ;;
wenzelm@6212
    71
      r)
wenzelm@6212
    72
        RESET=true
wenzelm@6212
    73
        ;;
wenzelm@2917
    74
      s)
wenzelm@2917
    75
        SESSION="$OPTARG"
wenzelm@2917
    76
        ;;
berghofe@6652
    77
      P)
berghofe@6652
    78
        RPATH="$OPTARG"
berghofe@6652
    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
berghofe@3747
   110
  mkdir -p $ISABELLE_BROWSER_INFO/gif
wenzelm@3848
   111
  cp $ISABELLE_HOME/lib/logo/isabelle.gif $ISABELLE_BROWSER_INFO/gif/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@7737
   136
if [ "$DOCUMENT" != false -a -d document -a -f document/root.tex ]
wenzelm@7737
   137
then DOC="$DOCUMENT"
wenzelm@7737
   138
else DOC=""; fi
wenzelm@7737
   139
wenzelm@7737
   140
wenzelm@7737
   141
SECONDS=0
wenzelm@6249
   142
wenzelm@2808
   143
if [ -n "$BUILD" ]; then
wenzelm@4451
   144
  ITEM="$SESSION"
wenzelm@7275
   145
  echo "Building $ITEM ..."
wenzelm@4451
   146
  LOG="$LOGDIR/$ITEM"
wenzelm@4451
   147
wenzelm@4451
   148
  $ISABELLE \
wenzelm@7737
   149
    -e "Session.use_dir $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$RPATH\";" \
wenzelm@4492
   150
    -q -w $LOGIC $NAME > $LOG 2>&1
wenzelm@6249
   151
  RC=$?
wenzelm@2808
   152
else
wenzelm@4451
   153
  ITEM=$(basename $LOGIC)-"$SESSION"
wenzelm@7275
   154
  echo "Running $ITEM ..."
wenzelm@4451
   155
  LOG="$LOGDIR/$ITEM"
wenzelm@4451
   156
wenzelm@4451
   157
  $ISABELLE \
wenzelm@7737
   158
    -e "Session.use_dir $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$RPATH\"; quit();" \
wenzelm@4492
   159
    -r -q $LOGIC > $LOG 2>&1
wenzelm@6249
   160
  RC=$?
wenzelm@6212
   161
  cd ..
wenzelm@2808
   162
fi
wenzelm@4451
   163
wenzelm@4451
   164
ELAPSED=$($ISABELLE_HOME/lib/scripts/showtime $SECONDS)
wenzelm@4451
   165
wenzelm@4451
   166
wenzelm@4451
   167
# exit status
wenzelm@4451
   168
wenzelm@4451
   169
if [ $RC -eq 0 ]; then
wenzelm@7275
   170
  echo "Finished $ITEM ($ELAPSED elapsed time)"
wenzelm@4451
   171
  gzip --force "$LOG"
wenzelm@4451
   172
else
wenzelm@7259
   173
  echo "$ITEM FAILED"
wenzelm@4451
   174
  echo "(see also $LOG)"
wenzelm@4451
   175
  echo; tail $LOG; echo
wenzelm@4451
   176
fi
wenzelm@4451
   177
wenzelm@4451
   178
exit $RC