lib/Tools/usedir
author wenzelm
Thu, 01 Jul 1999 21:28:49 +0200
changeset 6880 ce2b19e4402d
parent 6652 401f14f25648
child 6940 ee6640456cbb
permissions -rwxr-xr-x
Isar_examples/KnasterTarski.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$
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:"
6212
974310f9ca7d Session.init;
wenzelm
parents: 5034
diff changeset
    18
  echo "    -b           build mode (output heap image, using current 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)"
6652
401f14f25648 usedir now recognizes additional option -P which is used to
berghofe
parents: 6249
diff changeset
    21
  echo "    -P PATH      set path for remote theory browsing information"
6212
974310f9ca7d Session.init;
wenzelm
parents: 5034
diff changeset
    22
  echo "    -r           reset session path"
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    23
  echo "    -s NAME      override session NAME"
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    24
  echo
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    25
  echo "  Build object-logic or run examples. Also creates browsing"
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    26
  echo "  information (HTML etc.) according to settings."
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    27
  echo
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    28
  exit 1
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
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
## process command line
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
# options
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    35
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    36
BUILD=""
3747
cd9b6c86926c There is now one single option -i for generating theory browsing
berghofe
parents: 3636
diff changeset
    37
INFO=false
6212
974310f9ca7d Session.init;
wenzelm
parents: 5034
diff changeset
    38
RESET=false
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    39
SESSION=""
6652
401f14f25648 usedir now recognizes additional option -P which is used to
berghofe
parents: 6249
diff changeset
    40
RPATH=""
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    41
2917
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    42
function getoptions()
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    43
{
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    44
  OPTIND=1
6652
401f14f25648 usedir now recognizes additional option -P which is used to
berghofe
parents: 6249
diff changeset
    45
  while getopts "bi:rs:P:" OPT
2917
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    46
  do
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    47
    case "$OPT" in
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    48
      b)
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    49
        BUILD=true
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    50
        ;;
3747
cd9b6c86926c There is now one single option -i for generating theory browsing
berghofe
parents: 3636
diff changeset
    51
      i)
cd9b6c86926c There is now one single option -i for generating theory browsing
berghofe
parents: 3636
diff changeset
    52
        INFO="$OPTARG"
2917
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    53
        ;;
6212
974310f9ca7d Session.init;
wenzelm
parents: 5034
diff changeset
    54
      r)
974310f9ca7d Session.init;
wenzelm
parents: 5034
diff changeset
    55
        RESET=true
974310f9ca7d Session.init;
wenzelm
parents: 5034
diff changeset
    56
        ;;
2917
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    57
      s)
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    58
        SESSION="$OPTARG"
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    59
        ;;
6652
401f14f25648 usedir now recognizes additional option -P which is used to
berghofe
parents: 6249
diff changeset
    60
      P)
401f14f25648 usedir now recognizes additional option -P which is used to
berghofe
parents: 6249
diff changeset
    61
        RPATH="$OPTARG"
401f14f25648 usedir now recognizes additional option -P which is used to
berghofe
parents: 6249
diff changeset
    62
        ;;
2917
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    63
      \?)
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    64
        usage
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    65
        ;;
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    66
    esac
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    67
  done
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    68
}
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    69
2917
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    70
getoptions $ISABELLE_USEDIR_OPTIONS
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    71
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    72
getoptions "$@"
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    73
shift $(($OPTIND - 1))
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    74
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    75
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    76
# args
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    77
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    78
[ $# -ne 2 ] && usage
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    79
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    80
LOGIC="$1"; shift
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    81
NAME="$1"; shift
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    82
4419
wenzelm
parents: 4075
diff changeset
    83
[ -z "$SESSION" ] && SESSION=$(basename $NAME)
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    84
4419
wenzelm
parents: 4075
diff changeset
    85
wenzelm
parents: 4075
diff changeset
    86
wenzelm
parents: 4075
diff changeset
    87
## main
3636
3f2e55e5bacc Added some code for generating theory browsing data.
berghofe
parents: 3504
diff changeset
    88
4451
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
    89
# prepare browser info dir
4419
wenzelm
parents: 4075
diff changeset
    90
4586
wenzelm
parents: 4492
diff changeset
    91
if [ "$INFO" = "true" -a ! -f $ISABELLE_BROWSER_INFO/index.html ]; then
4419
wenzelm
parents: 4075
diff changeset
    92
3747
cd9b6c86926c There is now one single option -i for generating theory browsing
berghofe
parents: 3636
diff changeset
    93
  mkdir -p $ISABELLE_BROWSER_INFO/gif
3848
97bb3ff3c771 non-transparent logo;
wenzelm
parents: 3844
diff changeset
    94
  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
    95
  cp $ISABELLE_HOME/lib/html/index1.html $ISABELLE_BROWSER_INFO/index.html
4419
wenzelm
parents: 4075
diff changeset
    96
3636
3f2e55e5bacc Added some code for generating theory browsing data.
berghofe
parents: 3504
diff changeset
    97
  mkdir -p $ISABELLE_BROWSER_INFO/graph
3f2e55e5bacc Added some code for generating theory browsing data.
berghofe
parents: 3504
diff changeset
    98
  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
    99
  mkdir $ISABELLE_BROWSER_INFO/graph/GraphBrowser
3f2e55e5bacc Added some code for generating theory browsing data.
berghofe
parents: 3504
diff changeset
   100
  mkdir $ISABELLE_BROWSER_INFO/graph/awtUtilities
4419
wenzelm
parents: 4075
diff changeset
   101
  cp $ISABELLE_HOME/lib/browser/GraphBrowser/*.class $ISABELLE_BROWSER_INFO/graph/GraphBrowser
wenzelm
parents: 4075
diff changeset
   102
  cp $ISABELLE_HOME/lib/browser/awtUtilities/*.class $ISABELLE_BROWSER_INFO/graph/awtUtilities
wenzelm
parents: 4075
diff changeset
   103
3636
3f2e55e5bacc Added some code for generating theory browsing data.
berghofe
parents: 3504
diff changeset
   104
fi
3f2e55e5bacc Added some code for generating theory browsing data.
berghofe
parents: 3504
diff changeset
   105
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
   106
4451
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   107
# prepare log dir
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   108
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   109
LOGDIR="$ISABELLE_OUTPUT/log"
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   110
mkdir -p "$LOGDIR"
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   111
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   112
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   113
# run isabelle
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   114
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   115
SECONDS=0
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   116
6249
8bb90076cc7c Session.use_dir: check parent;
wenzelm
parents: 6212
diff changeset
   117
PARENT=$(basename "$LOGIC")
8bb90076cc7c Session.use_dir: check parent;
wenzelm
parents: 6212
diff changeset
   118
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
   119
if [ -n "$BUILD" ]; then
4451
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   120
  ITEM="$SESSION"
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   121
  echo -n "Building $ITEM ... "
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   122
  LOG="$LOGDIR/$ITEM"
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   123
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   124
  $ISABELLE \
6652
401f14f25648 usedir now recognizes additional option -P which is used to
berghofe
parents: 6249
diff changeset
   125
    -e "Session.use_dir $RESET $INFO \"$PARENT\" \"$SESSION\" \"$RPATH\";" \
4492
ab441d89a2cb stderr to $LOG;
wenzelm
parents: 4451
diff changeset
   126
    -q -w $LOGIC $NAME > $LOG 2>&1
6249
8bb90076cc7c Session.use_dir: check parent;
wenzelm
parents: 6212
diff changeset
   127
  RC=$?
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
   128
else
4451
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   129
  ITEM=$(basename $LOGIC)-"$SESSION"
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   130
  echo -n "Running $ITEM ... "
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   131
  LOG="$LOGDIR/$ITEM"
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   132
6212
974310f9ca7d Session.init;
wenzelm
parents: 5034
diff changeset
   133
  cd "$NAME"
4451
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   134
  $ISABELLE \
6652
401f14f25648 usedir now recognizes additional option -P which is used to
berghofe
parents: 6249
diff changeset
   135
    -e "Session.use_dir $RESET $INFO \"$PARENT\" \"$SESSION\" \"$RPATH\"; quit();" \
4492
ab441d89a2cb stderr to $LOG;
wenzelm
parents: 4451
diff changeset
   136
    -r -q $LOGIC > $LOG 2>&1
6249
8bb90076cc7c Session.use_dir: check parent;
wenzelm
parents: 6212
diff changeset
   137
  RC=$?
6212
974310f9ca7d Session.init;
wenzelm
parents: 5034
diff changeset
   138
  cd ..
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
   139
fi
4451
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   140
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   141
ELAPSED=$($ISABELLE_HOME/lib/scripts/showtime $SECONDS)
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   142
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   143
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   144
# exit status
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   145
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   146
if [ $RC -eq 0 ]; then
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   147
  echo "OK  ($ELAPSED elapsed time)"
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   148
  gzip --force "$LOG"
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   149
else
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   150
  echo "FAILED"
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   151
  echo "(see also $LOG)"
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   152
  echo; tail $LOG; echo
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   153
fi
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   154
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   155
exit $RC