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