lib/Tools/usedir
author wenzelm
Sat Jul 25 10:31:27 2009 +0200 (2009-07-25)
changeset 32187 cca43ca13f4f
parent 32061 11f8ee55662d
child 32641 68c53dbceffd
permissions -rwxr-xr-x
renamed structure Display_Goal to Goal_Display;
wenzelm@10555
     1
#!/usr/bin/env bash
wenzelm@2808
     2
#
wenzelm@9788
     3
# Author: Markus Wenzel, TU Muenchen
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@10511
    10
PRG="$(basename "$0")"
wenzelm@2808
    11
wenzelm@2808
    12
function usage()
wenzelm@2808
    13
{
wenzelm@2808
    14
  echo
wenzelm@28650
    15
  echo "Usage: isabelle $PRG [OPTIONS] LOGIC NAME"
wenzelm@2808
    16
  echo
wenzelm@2808
    17
  echo "  Options are:"
wenzelm@17194
    18
  echo "    -C BOOL      copy existing document directory to -D PATH (default true)"
wenzelm@8197
    19
  echo "    -D PATH      dump generated document sources into PATH"
wenzelm@23972
    20
  echo "    -M MAX       multithreading: maximum number of worker threads (default 1)"
wenzelm@6940
    21
  echo "    -P PATH      set path for remote theory browsing information"
wenzelm@24118
    22
  echo "    -T LEVEL     multithreading: trace level (default 0)"
wenzelm@17050
    23
  echo "    -V VERSION   declare alternative document VERSION"
wenzelm@6212
    24
  echo "    -b           build mode (output heap image, using current dir)"
wenzelm@7737
    25
  echo "    -d FORMAT    build document as FORMAT (default false)"
webertj@15269
    26
  echo "    -f NAME      use ML file NAME (default ROOT.ML)"
wenzelm@11847
    27
  echo "    -g BOOL      generate session graph image for document (default false)"
wenzelm@11847
    28
  echo "    -i BOOL      generate HTML and graph browser information (default false)"
wenzelm@10562
    29
  echo "    -m MODE      add print mode for output"
wenzelm@32061
    30
  echo "    -p LEVEL     set level of detail for proof objects (default 0)"
wenzelm@32061
    31
  echo "    -q LEVEL     set level of parallel proof checking (default 1)"
wenzelm@6212
    32
  echo "    -r           reset session path"
wenzelm@2808
    33
  echo "    -s NAME      override session NAME"
wenzelm@31688
    34
  echo "    -t BOOL      internal session timing (default false)"
wenzelm@11577
    35
  echo "    -v BOOL      be verbose (default false)"
wenzelm@2808
    36
  echo
wenzelm@2808
    37
  echo "  Build object-logic or run examples. Also creates browsing"
wenzelm@2808
    38
  echo "  information (HTML etc.) according to settings."
wenzelm@2808
    39
  echo
wenzelm@7461
    40
  echo "  ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
wenzelm@24957
    41
  echo "  HOL_USEDIR_OPTIONS=$HOL_USEDIR_OPTIONS"
wenzelm@7461
    42
  echo
wenzelm@29089
    43
  echo "  ML_PLATFORM=$ML_PLATFORM"
wenzelm@29089
    44
  echo "  ML_HOME=$ML_HOME"
wenzelm@29089
    45
  echo "  ML_SYSTEM=$ML_SYSTEM"
wenzelm@29089
    46
  echo "  ML_OPTIONS=$ML_OPTIONS"
wenzelm@29089
    47
  echo
wenzelm@2808
    48
  exit 1
wenzelm@2808
    49
}
wenzelm@2808
    50
wenzelm@11577
    51
function fail()
wenzelm@11577
    52
{
wenzelm@11577
    53
  echo "$1" >&2
wenzelm@11577
    54
  exit 2
wenzelm@11577
    55
}
wenzelm@11577
    56
wenzelm@11577
    57
function check_bool()
wenzelm@11577
    58
{
wenzelm@11577
    59
  [ "$1" = true -o "$1" = false ] || fail "Bad boolean: \"$1\""
wenzelm@11577
    60
}
wenzelm@11577
    61
wenzelm@11577
    62
function check_number()
wenzelm@11577
    63
{
wenzelm@12912
    64
  [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
wenzelm@11577
    65
}
wenzelm@11577
    66
wenzelm@2808
    67
wenzelm@2808
    68
## process command line
wenzelm@2808
    69
wenzelm@2808
    70
# options
wenzelm@2808
    71
wenzelm@24061
    72
COPY_DUMP=true
wenzelm@8197
    73
DUMP=""
wenzelm@23972
    74
MAXTHREADS="1"
wenzelm@8197
    75
RPATH=""
wenzelm@24118
    76
TRACETHREADS="0"
wenzelm@17050
    77
DOCUMENT_VERSIONS=""
wenzelm@2808
    78
BUILD=""
wenzelm@7737
    79
DOCUMENT=false
wenzelm@17050
    80
ROOT_FILE="ROOT.ML"
wenzelm@11847
    81
DOCUMENT_GRAPH=false
berghofe@3747
    82
INFO=false
wenzelm@10562
    83
MODES=""
wenzelm@6212
    84
RESET=false
wenzelm@2808
    85
SESSION=""
wenzelm@32061
    86
PROOFS="0"
wenzelm@32061
    87
PARALLEL_PROOFS="1"
wenzelm@31688
    88
TIMING=false
wenzelm@11577
    89
VERBOSE=false
wenzelm@2808
    90
wenzelm@2917
    91
function getoptions()
wenzelm@2917
    92
{
wenzelm@2917
    93
  OPTIND=1
wenzelm@32061
    94
  while getopts "C:D:M:P:T:V:bd:f:g:i:m:p:q:rs:t:v:" OPT
wenzelm@2917
    95
  do
wenzelm@2917
    96
    case "$OPT" in
wenzelm@17194
    97
      C)
wenzelm@17194
    98
        check_bool "$OPTARG"
wenzelm@17194
    99
        COPY_DUMP="$OPTARG"
wenzelm@17194
   100
        ;;
wenzelm@8197
   101
      D)
wenzelm@8197
   102
        DUMP="$OPTARG"
wenzelm@8197
   103
        ;;
wenzelm@23972
   104
      M)
wenzelm@25774
   105
        if [ "$OPTARG" = max ]; then
wenzelm@29435
   106
          MAXTHREADS=0
wenzelm@29435
   107
        else
wenzelm@25774
   108
          check_number "$OPTARG"
wenzelm@25774
   109
          MAXTHREADS="$OPTARG"
wenzelm@29435
   110
        fi
wenzelm@23972
   111
        ;;
wenzelm@8197
   112
      P)
wenzelm@8197
   113
        RPATH="$OPTARG"
wenzelm@8197
   114
        ;;
wenzelm@24061
   115
      T)
wenzelm@24118
   116
        check_number "$OPTARG"
wenzelm@24061
   117
        TRACETHREADS="$OPTARG"
wenzelm@24061
   118
        ;;
wenzelm@17050
   119
      V)
wenzelm@17050
   120
        if [ -z "$DOCUMENT_VERSIONS" ]; then
wenzelm@17050
   121
          DOCUMENT_VERSIONS="\"$OPTARG\""
wenzelm@17050
   122
        else
wenzelm@17050
   123
          DOCUMENT_VERSIONS="$DOCUMENT_VERSIONS, \"$OPTARG\""
wenzelm@17050
   124
        fi
wenzelm@17050
   125
        ;;
wenzelm@2917
   126
      b)
wenzelm@2917
   127
        BUILD=true
wenzelm@2917
   128
        ;;
wenzelm@7737
   129
      d)
wenzelm@7737
   130
        DOCUMENT="$OPTARG"
wenzelm@7737
   131
        ;;
webertj@15269
   132
      f)
webertj@15269
   133
        ROOT_FILE="$OPTARG"
webertj@15269
   134
        ;;
wenzelm@11847
   135
      g)
wenzelm@11847
   136
        check_bool "$OPTARG"
wenzelm@11847
   137
        DOCUMENT_GRAPH="$OPTARG"
wenzelm@11847
   138
        ;;
berghofe@3747
   139
      i)
wenzelm@11577
   140
        check_bool "$OPTARG"
berghofe@3747
   141
        INFO="$OPTARG"
wenzelm@2917
   142
        ;;
wenzelm@10562
   143
      m)
wenzelm@10562
   144
        if [ -z "$MODES" ]; then
wenzelm@10562
   145
          MODES="\"$OPTARG\""
wenzelm@10562
   146
        else
wenzelm@10585
   147
          MODES="\"$OPTARG\", $MODES"
wenzelm@10562
   148
        fi
wenzelm@10562
   149
        ;;
berghofe@11535
   150
      p)
wenzelm@11577
   151
        check_number "$OPTARG"
wenzelm@11543
   152
        PROOFS="$OPTARG"
berghofe@11535
   153
        ;;
wenzelm@32061
   154
      q)
wenzelm@32061
   155
        check_number "$OPTARG"
wenzelm@32061
   156
        PARALLEL_PROOFS="$OPTARG"
wenzelm@32061
   157
        ;;
wenzelm@6212
   158
      r)
wenzelm@6212
   159
        RESET=true
wenzelm@6212
   160
        ;;
wenzelm@2917
   161
      s)
wenzelm@2917
   162
        SESSION="$OPTARG"
wenzelm@2917
   163
        ;;
wenzelm@31688
   164
      t)
wenzelm@31688
   165
        check_bool "$OPTARG"
wenzelm@31688
   166
        TIMING="$OPTARG"
wenzelm@31688
   167
        ;;
wenzelm@11577
   168
      v)
wenzelm@11577
   169
        check_bool "$OPTARG"
wenzelm@11577
   170
        VERBOSE="$OPTARG"
wenzelm@11577
   171
        ;;
wenzelm@2917
   172
      \?)
wenzelm@2917
   173
        usage
wenzelm@2917
   174
        ;;
wenzelm@2917
   175
    esac
wenzelm@2917
   176
  done
wenzelm@2917
   177
}
wenzelm@2808
   178
wenzelm@31307
   179
eval "OPTIONS=($ISABELLE_USEDIR_OPTIONS)"
wenzelm@31307
   180
getoptions "${OPTIONS[@]}"
wenzelm@2917
   181
wenzelm@2917
   182
getoptions "$@"
wenzelm@2808
   183
shift $(($OPTIND - 1))
wenzelm@2808
   184
wenzelm@2808
   185
wenzelm@2808
   186
# args
wenzelm@2808
   187
wenzelm@9788
   188
[ "$#" -ne 2 ] && usage
wenzelm@2808
   189
wenzelm@2808
   190
LOGIC="$1"; shift
wenzelm@2808
   191
NAME="$1"; shift
wenzelm@2808
   192
wenzelm@9788
   193
[ -z "$SESSION" ] && SESSION=$(basename "$NAME")
wenzelm@2808
   194
wenzelm@4419
   195
wenzelm@4419
   196
wenzelm@4419
   197
## main
berghofe@3636
   198
wenzelm@4451
   199
# prepare browser info dir
wenzelm@4419
   200
haftmann@25235
   201
if [ "$INFO" = "true" -a ! -f "$ISABELLE_BROWSER_INFO/index.html" ]; then
wenzelm@9788
   202
  mkdir -p "$ISABELLE_BROWSER_INFO"
wenzelm@9788
   203
  cp "$ISABELLE_HOME/lib/logo/isabelle.gif" "$ISABELLE_BROWSER_INFO/isabelle.gif"
haftmann@25234
   204
  cat "$ISABELLE_HOME/lib/html/library_index_header.template" \
haftmann@25234
   205
    "$ISABELLE_HOME/lib/html/library_index_content.template" \
haftmann@25234
   206
    "$ISABELLE_HOME/lib/html/library_index_footer.template"> "$ISABELLE_BROWSER_INFO/index.html"
berghofe@3636
   207
fi
berghofe@3636
   208
wenzelm@2808
   209
wenzelm@4451
   210
# prepare log dir
wenzelm@4451
   211
wenzelm@4451
   212
LOGDIR="$ISABELLE_OUTPUT/log"
wenzelm@4451
   213
mkdir -p "$LOGDIR"
wenzelm@4451
   214
wenzelm@4451
   215
wenzelm@4451
   216
# run isabelle
wenzelm@4451
   217
wenzelm@7737
   218
PARENT=$(basename "$LOGIC")
wenzelm@7737
   219
wenzelm@11949
   220
if [ -z "$BUILD" ]; then
wenzelm@11949
   221
  cd "$NAME" || fail "Bad session directory '$NAME'"
wenzelm@11949
   222
fi
wenzelm@4451
   223
wenzelm@11847
   224
if [ "$DOCUMENT" != false ]; then
wenzelm@8568
   225
  DOC="$DOCUMENT"
wenzelm@8568
   226
else
wenzelm@8568
   227
  DOC=""
wenzelm@8568
   228
fi
wenzelm@7737
   229
wenzelm@7737
   230
wenzelm@18321
   231
. "$ISABELLE_HOME/lib/scripts/timestart.bash"
wenzelm@6249
   232
wenzelm@2808
   233
if [ -n "$BUILD" ]; then
wenzelm@4451
   234
  ITEM="$SESSION"
wenzelm@11577
   235
  echo "Building $ITEM ..." >&2
wenzelm@4451
   236
  LOG="$LOGDIR/$ITEM"
wenzelm@4451
   237
wenzelm@28502
   238
  "$ISABELLE_PROCESS" \
wenzelm@31688
   239
    -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS;" \
wenzelm@31317
   240
    -q -w $LOGIC $NAME > "$LOG"
wenzelm@9788
   241
  RC="$?"
wenzelm@2808
   242
else
wenzelm@9788
   243
  ITEM=$(basename "$LOGIC")-"$SESSION"
wenzelm@11577
   244
  echo "Running $ITEM ..." >&2
wenzelm@4451
   245
  LOG="$LOGDIR/$ITEM"
wenzelm@4451
   246
wenzelm@28502
   247
  "$ISABELLE_PROCESS" \
wenzelm@31688
   248
    -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS; quit();" \
wenzelm@11577
   249
    -r -q "$LOGIC" > "$LOG"
wenzelm@9788
   250
  RC="$?"
wenzelm@6212
   251
  cd ..
wenzelm@2808
   252
fi
wenzelm@4451
   253
wenzelm@18321
   254
. "$ISABELLE_HOME/lib/scripts/timestop.bash"
wenzelm@4451
   255
wenzelm@4451
   256
wenzelm@4451
   257
# exit status
wenzelm@4451
   258
wenzelm@9788
   259
if [ "$RC" -eq 0 ]; then
wenzelm@18321
   260
  echo "Finished $ITEM ($TIMES_REPORT)" >&2
wenzelm@4451
   261
  gzip --force "$LOG"
wenzelm@4451
   262
else
wenzelm@11577
   263
  { echo "$ITEM FAILED";
wenzelm@11577
   264
    echo "(see also $LOG)";
wenzelm@11577
   265
    echo; tail "$LOG"; echo; } >&2
wenzelm@4451
   266
fi
wenzelm@4451
   267
wenzelm@9788
   268
exit "$RC"