lib/Tools/usedir
author wenzelm
Fri, 10 Nov 2000 19:02:37 +0100
changeset 10432 3dfbc913d184
parent 9788 df671fa2562a
child 10511 efb3428c9879
permissions -rwxr-xr-x
added axclass inverse and consts inverse, divide (infix "/"); moved axclass power to Nat.thy;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3007
e5efa177ee0c removed -norc;
wenzelm
parents: 2917
diff changeset
     1
#!/bin/bash
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
     2
#
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
     3
# $Id$
9788
wenzelm
parents: 9237
diff changeset
     4
# Author: Markus Wenzel, TU Muenchen
wenzelm
parents: 9237
diff changeset
     5
# License: GPL (GNU GENERAL PUBLIC LICENSE)
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
     6
#
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
     7
# DESCRIPTION: build object-logic or run examples
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
     8
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
     9
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    10
## diagnostics
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    11
9788
wenzelm
parents: 9237
diff changeset
    12
PRG=$(basename "$0")
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    13
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    14
function usage()
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    15
{
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    16
  echo
9237
161fb7f00414 fixed usage;
wenzelm
parents: 9047
diff changeset
    17
  echo "Usage: $PRG [OPTIONS] LOGIC NAME"
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    18
  echo
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    19
  echo "  Options are:"
8197
baab8e487fad -D PATH: dump generated document sources into PATH;
wenzelm
parents: 7888
diff changeset
    20
  echo "    -D PATH      dump generated document sources into PATH"
6940
ee6640456cbb -B option;
wenzelm
parents: 6652
diff changeset
    21
  echo "    -P PATH      set path for remote theory browsing information"
6212
974310f9ca7d Session.init;
wenzelm
parents: 5034
diff changeset
    22
  echo "    -b           build mode (output heap image, using current dir)"
8359
124ad46105dd option -c: tell ML system to compress output image;
wenzelm
parents: 8241
diff changeset
    23
  echo "    -c BOOL      tell ML system to compress output image (default true)"
7737
acaf55bee03e document preparation options: -c -d;
wenzelm
parents: 7461
diff changeset
    24
  echo "    -d FORMAT    build document as FORMAT (default false)"
3747
cd9b6c86926c There is now one single option -i for generating theory browsing
berghofe
parents: 3636
diff changeset
    25
  echo "    -i BOOL      generate theory browsing information,"
cd9b6c86926c There is now one single option -i for generating theory browsing
berghofe
parents: 3636
diff changeset
    26
  echo "                 i.e. HTML / graph data (default false)"
6212
974310f9ca7d Session.init;
wenzelm
parents: 5034
diff changeset
    27
  echo "    -r           reset session path"
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    28
  echo "    -s NAME      override session NAME"
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    29
  echo
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    30
  echo "  Build object-logic or run examples. Also creates browsing"
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    31
  echo "  information (HTML etc.) according to settings."
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    32
  echo
7461
94ae093f6706 usage: tell ISABELLE_USEDIR_OPTIONS;
wenzelm
parents: 7276
diff changeset
    33
  echo "  ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
94ae093f6706 usage: tell ISABELLE_USEDIR_OPTIONS;
wenzelm
parents: 7276
diff changeset
    34
  echo
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    35
  exit 1
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    36
}
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    37
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    38
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    39
## process command line
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    40
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    41
# options
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    42
8197
baab8e487fad -D PATH: dump generated document sources into PATH;
wenzelm
parents: 7888
diff changeset
    43
DUMP=""
baab8e487fad -D PATH: dump generated document sources into PATH;
wenzelm
parents: 7888
diff changeset
    44
RPATH=""
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    45
BUILD=""
8747
22580c8bc62f fixed -c default value;
wenzelm
parents: 8568
diff changeset
    46
COMPRESS=true
7737
acaf55bee03e document preparation options: -c -d;
wenzelm
parents: 7461
diff changeset
    47
DOCUMENT=false
3747
cd9b6c86926c There is now one single option -i for generating theory browsing
berghofe
parents: 3636
diff changeset
    48
INFO=false
6212
974310f9ca7d Session.init;
wenzelm
parents: 5034
diff changeset
    49
RESET=false
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    50
SESSION=""
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    51
2917
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    52
function getoptions()
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    53
{
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    54
  OPTIND=1
8197
baab8e487fad -D PATH: dump generated document sources into PATH;
wenzelm
parents: 7888
diff changeset
    55
  while getopts "D:P:bc:d:i:rs:" OPT
2917
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    56
  do
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    57
    case "$OPT" in
8197
baab8e487fad -D PATH: dump generated document sources into PATH;
wenzelm
parents: 7888
diff changeset
    58
      D)
baab8e487fad -D PATH: dump generated document sources into PATH;
wenzelm
parents: 7888
diff changeset
    59
        DUMP="$OPTARG"
baab8e487fad -D PATH: dump generated document sources into PATH;
wenzelm
parents: 7888
diff changeset
    60
        ;;
baab8e487fad -D PATH: dump generated document sources into PATH;
wenzelm
parents: 7888
diff changeset
    61
      P)
baab8e487fad -D PATH: dump generated document sources into PATH;
wenzelm
parents: 7888
diff changeset
    62
        RPATH="$OPTARG"
baab8e487fad -D PATH: dump generated document sources into PATH;
wenzelm
parents: 7888
diff changeset
    63
        ;;
2917
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    64
      b)
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    65
        BUILD=true
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    66
        ;;
8359
124ad46105dd option -c: tell ML system to compress output image;
wenzelm
parents: 8241
diff changeset
    67
      c)
124ad46105dd option -c: tell ML system to compress output image;
wenzelm
parents: 8241
diff changeset
    68
        COMPRESS="$OPTARG"
124ad46105dd option -c: tell ML system to compress output image;
wenzelm
parents: 8241
diff changeset
    69
        ;;
7737
acaf55bee03e document preparation options: -c -d;
wenzelm
parents: 7461
diff changeset
    70
      d)
acaf55bee03e document preparation options: -c -d;
wenzelm
parents: 7461
diff changeset
    71
        DOCUMENT="$OPTARG"
acaf55bee03e document preparation options: -c -d;
wenzelm
parents: 7461
diff changeset
    72
        ;;
3747
cd9b6c86926c There is now one single option -i for generating theory browsing
berghofe
parents: 3636
diff changeset
    73
      i)
cd9b6c86926c There is now one single option -i for generating theory browsing
berghofe
parents: 3636
diff changeset
    74
        INFO="$OPTARG"
2917
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    75
        ;;
6212
974310f9ca7d Session.init;
wenzelm
parents: 5034
diff changeset
    76
      r)
974310f9ca7d Session.init;
wenzelm
parents: 5034
diff changeset
    77
        RESET=true
974310f9ca7d Session.init;
wenzelm
parents: 5034
diff changeset
    78
        ;;
2917
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    79
      s)
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    80
        SESSION="$OPTARG"
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    81
        ;;
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    82
      \?)
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    83
        usage
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    84
        ;;
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    85
    esac
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    86
  done
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    87
}
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    88
2917
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    89
getoptions $ISABELLE_USEDIR_OPTIONS
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    90
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    91
getoptions "$@"
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    92
shift $(($OPTIND - 1))
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    93
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    94
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    95
# args
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    96
9788
wenzelm
parents: 9237
diff changeset
    97
[ "$#" -ne 2 ] && usage
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    98
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    99
LOGIC="$1"; shift
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
   100
NAME="$1"; shift
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
   101
9788
wenzelm
parents: 9237
diff changeset
   102
[ -z "$SESSION" ] && SESSION=$(basename "$NAME")
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
   103
4419
wenzelm
parents: 4075
diff changeset
   104
wenzelm
parents: 4075
diff changeset
   105
wenzelm
parents: 4075
diff changeset
   106
## main
3636
3f2e55e5bacc Added some code for generating theory browsing data.
berghofe
parents: 3504
diff changeset
   107
4451
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   108
# prepare browser info dir
4419
wenzelm
parents: 4075
diff changeset
   109
9788
wenzelm
parents: 9237
diff changeset
   110
if [ "$INFO" = "true" -a ! -f "$ISABELLE_BROWSER_INFO/index.html" ]; then
wenzelm
parents: 9237
diff changeset
   111
  mkdir -p "$ISABELLE_BROWSER_INFO"
wenzelm
parents: 9237
diff changeset
   112
  cp "$ISABELLE_HOME/lib/logo/isabelle.gif" "$ISABELLE_BROWSER_INFO/isabelle.gif"
wenzelm
parents: 9237
diff changeset
   113
  cp "$ISABELLE_HOME/lib/html/index.html" "$ISABELLE_BROWSER_INFO/index.html"
3636
3f2e55e5bacc Added some code for generating theory browsing data.
berghofe
parents: 3504
diff changeset
   114
fi
3f2e55e5bacc Added some code for generating theory browsing data.
berghofe
parents: 3504
diff changeset
   115
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
   116
4451
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   117
# prepare log dir
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   118
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   119
LOGDIR="$ISABELLE_OUTPUT/log"
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   120
mkdir -p "$LOGDIR"
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   121
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   122
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   123
# run isabelle
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   124
7737
acaf55bee03e document preparation options: -c -d;
wenzelm
parents: 7461
diff changeset
   125
PARENT=$(basename "$LOGIC")
acaf55bee03e document preparation options: -c -d;
wenzelm
parents: 7461
diff changeset
   126
acaf55bee03e document preparation options: -c -d;
wenzelm
parents: 7461
diff changeset
   127
[ -z "$BUILD" ] && cd "$NAME"
4451
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   128
8568
wenzelm
parents: 8565
diff changeset
   129
if [ "$DOCUMENT" != false -a -d document ]; then
wenzelm
parents: 8565
diff changeset
   130
  DOC="$DOCUMENT"
9788
wenzelm
parents: 9237
diff changeset
   131
  [ -n "$DUMP" -a -d "$DUMP" ] && "$ISATOOL" latex -o sty "$DUMP/root.tex" >/dev/null
8568
wenzelm
parents: 8565
diff changeset
   132
else
wenzelm
parents: 8565
diff changeset
   133
  DOC=""
wenzelm
parents: 8565
diff changeset
   134
fi
7737
acaf55bee03e document preparation options: -c -d;
wenzelm
parents: 7461
diff changeset
   135
acaf55bee03e document preparation options: -c -d;
wenzelm
parents: 7461
diff changeset
   136
acaf55bee03e document preparation options: -c -d;
wenzelm
parents: 7461
diff changeset
   137
SECONDS=0
6249
8bb90076cc7c Session.use_dir: check parent;
wenzelm
parents: 6212
diff changeset
   138
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
   139
if [ -n "$BUILD" ]; then
4451
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   140
  ITEM="$SESSION"
7275
3a001f2148f7 removed -m option;
wenzelm
parents: 7259
diff changeset
   141
  echo "Building $ITEM ..."
4451
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   142
  LOG="$LOGDIR/$ITEM"
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   143
8359
124ad46105dd option -c: tell ML system to compress output image;
wenzelm
parents: 8241
diff changeset
   144
  OPT_C=""
124ad46105dd option -c: tell ML system to compress output image;
wenzelm
parents: 8241
diff changeset
   145
  [ "$COMPRESS" = true ] && OPT_C="-c"
124ad46105dd option -c: tell ML system to compress output image;
wenzelm
parents: 8241
diff changeset
   146
9788
wenzelm
parents: 9237
diff changeset
   147
  "$ISABELLE" \
8197
baab8e487fad -D PATH: dump generated document sources into PATH;
wenzelm
parents: 7888
diff changeset
   148
    -e "Session.use_dir $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\";" \
9788
wenzelm
parents: 9237
diff changeset
   149
    $OPT_C -q -w $LOGIC $NAME > "$LOG" 2>&1
wenzelm
parents: 9237
diff changeset
   150
  RC="$?"
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
   151
else
9788
wenzelm
parents: 9237
diff changeset
   152
  ITEM=$(basename "$LOGIC")-"$SESSION"
7275
3a001f2148f7 removed -m option;
wenzelm
parents: 7259
diff changeset
   153
  echo "Running $ITEM ..."
4451
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   154
  LOG="$LOGDIR/$ITEM"
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   155
9788
wenzelm
parents: 9237
diff changeset
   156
  "$ISABELLE" \
8197
baab8e487fad -D PATH: dump generated document sources into PATH;
wenzelm
parents: 7888
diff changeset
   157
    -e "Session.use_dir $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\"; quit();" \
9788
wenzelm
parents: 9237
diff changeset
   158
    -r -q "$LOGIC" > "$LOG" 2>&1
wenzelm
parents: 9237
diff changeset
   159
  RC="$?"
6212
974310f9ca7d Session.init;
wenzelm
parents: 5034
diff changeset
   160
  cd ..
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
   161
fi
4451
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   162
9788
wenzelm
parents: 9237
diff changeset
   163
ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS")
4451
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   164
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   165
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   166
# exit status
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   167
9788
wenzelm
parents: 9237
diff changeset
   168
if [ "$RC" -eq 0 ]; then
7275
3a001f2148f7 removed -m option;
wenzelm
parents: 7259
diff changeset
   169
  echo "Finished $ITEM ($ELAPSED elapsed time)"
4451
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   170
  gzip --force "$LOG"
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   171
else
7259
e75aa311788c tuned messages;
wenzelm
parents: 7226
diff changeset
   172
  echo "$ITEM FAILED"
4451
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   173
  echo "(see also $LOG)"
9788
wenzelm
parents: 9237
diff changeset
   174
  echo; tail "$LOG"; echo
4451
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   175
fi
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   176
9788
wenzelm
parents: 9237
diff changeset
   177
exit "$RC"