lib/Tools/usedir
author wenzelm
Mon Jan 04 11:55:23 2010 +0100 (2010-01-04 ago)
changeset 34238 b28be884edda
parent 33830 1b634d37aa64
child 34261 8e36b3ac6083
permissions -rwxr-xr-x
discontinued special HOL_USEDIR_OPTIONS;
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@7461
    41
  echo
wenzelm@29089
    42
  echo "  ML_PLATFORM=$ML_PLATFORM"
wenzelm@29089
    43
  echo "  ML_HOME=$ML_HOME"
wenzelm@29089
    44
  echo "  ML_SYSTEM=$ML_SYSTEM"
wenzelm@29089
    45
  echo "  ML_OPTIONS=$ML_OPTIONS"
wenzelm@29089
    46
  echo
wenzelm@2808
    47
  exit 1
wenzelm@2808
    48
}
wenzelm@2808
    49
wenzelm@11577
    50
function fail()
wenzelm@11577
    51
{
wenzelm@11577
    52
  echo "$1" >&2
wenzelm@11577
    53
  exit 2
wenzelm@11577
    54
}
wenzelm@11577
    55
wenzelm@11577
    56
function check_bool()
wenzelm@11577
    57
{
wenzelm@11577
    58
  [ "$1" = true -o "$1" = false ] || fail "Bad boolean: \"$1\""
wenzelm@11577
    59
}
wenzelm@11577
    60
wenzelm@11577
    61
function check_number()
wenzelm@11577
    62
{
wenzelm@12912
    63
  [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
wenzelm@11577
    64
}
wenzelm@11577
    65
wenzelm@2808
    66
wenzelm@2808
    67
## process command line
wenzelm@2808
    68
wenzelm@2808
    69
# options
wenzelm@2808
    70
wenzelm@24061
    71
COPY_DUMP=true
wenzelm@8197
    72
DUMP=""
wenzelm@23972
    73
MAXTHREADS="1"
wenzelm@8197
    74
RPATH=""
wenzelm@24118
    75
TRACETHREADS="0"
wenzelm@17050
    76
DOCUMENT_VERSIONS=""
wenzelm@2808
    77
BUILD=""
wenzelm@7737
    78
DOCUMENT=false
wenzelm@17050
    79
ROOT_FILE="ROOT.ML"
wenzelm@11847
    80
DOCUMENT_GRAPH=false
berghofe@3747
    81
INFO=false
wenzelm@10562
    82
MODES=""
wenzelm@6212
    83
RESET=false
wenzelm@2808
    84
SESSION=""
wenzelm@32061
    85
PROOFS="0"
wenzelm@32061
    86
PARALLEL_PROOFS="1"
wenzelm@31688
    87
TIMING=false
wenzelm@11577
    88
VERBOSE=false
wenzelm@2808
    89
wenzelm@2917
    90
function getoptions()
wenzelm@2917
    91
{
wenzelm@2917
    92
  OPTIND=1
wenzelm@32061
    93
  while getopts "C:D:M:P:T:V:bd:f:g:i:m:p:q:rs:t:v:" OPT
wenzelm@2917
    94
  do
wenzelm@2917
    95
    case "$OPT" in
wenzelm@17194
    96
      C)
wenzelm@17194
    97
        check_bool "$OPTARG"
wenzelm@17194
    98
        COPY_DUMP="$OPTARG"
wenzelm@17194
    99
        ;;
wenzelm@8197
   100
      D)
wenzelm@8197
   101
        DUMP="$OPTARG"
wenzelm@8197
   102
        ;;
wenzelm@23972
   103
      M)
wenzelm@25774
   104
        if [ "$OPTARG" = max ]; then
wenzelm@29435
   105
          MAXTHREADS=0
wenzelm@29435
   106
        else
wenzelm@25774
   107
          check_number "$OPTARG"
wenzelm@25774
   108
          MAXTHREADS="$OPTARG"
wenzelm@29435
   109
        fi
wenzelm@23972
   110
        ;;
wenzelm@8197
   111
      P)
wenzelm@8197
   112
        RPATH="$OPTARG"
wenzelm@8197
   113
        ;;
wenzelm@24061
   114
      T)
wenzelm@24118
   115
        check_number "$OPTARG"
wenzelm@24061
   116
        TRACETHREADS="$OPTARG"
wenzelm@24061
   117
        ;;
wenzelm@17050
   118
      V)
wenzelm@17050
   119
        if [ -z "$DOCUMENT_VERSIONS" ]; then
wenzelm@17050
   120
          DOCUMENT_VERSIONS="\"$OPTARG\""
wenzelm@17050
   121
        else
wenzelm@17050
   122
          DOCUMENT_VERSIONS="$DOCUMENT_VERSIONS, \"$OPTARG\""
wenzelm@17050
   123
        fi
wenzelm@17050
   124
        ;;
wenzelm@2917
   125
      b)
wenzelm@2917
   126
        BUILD=true
wenzelm@2917
   127
        ;;
wenzelm@7737
   128
      d)
wenzelm@7737
   129
        DOCUMENT="$OPTARG"
wenzelm@7737
   130
        ;;
webertj@15269
   131
      f)
webertj@15269
   132
        ROOT_FILE="$OPTARG"
webertj@15269
   133
        ;;
wenzelm@11847
   134
      g)
wenzelm@11847
   135
        check_bool "$OPTARG"
wenzelm@11847
   136
        DOCUMENT_GRAPH="$OPTARG"
wenzelm@11847
   137
        ;;
berghofe@3747
   138
      i)
wenzelm@11577
   139
        check_bool "$OPTARG"
berghofe@3747
   140
        INFO="$OPTARG"
wenzelm@2917
   141
        ;;
wenzelm@10562
   142
      m)
wenzelm@10562
   143
        if [ -z "$MODES" ]; then
wenzelm@10562
   144
          MODES="\"$OPTARG\""
wenzelm@10562
   145
        else
wenzelm@10585
   146
          MODES="\"$OPTARG\", $MODES"
wenzelm@10562
   147
        fi
wenzelm@10562
   148
        ;;
berghofe@11535
   149
      p)
wenzelm@11577
   150
        check_number "$OPTARG"
wenzelm@11543
   151
        PROOFS="$OPTARG"
berghofe@11535
   152
        ;;
wenzelm@32061
   153
      q)
wenzelm@32061
   154
        check_number "$OPTARG"
wenzelm@32061
   155
        PARALLEL_PROOFS="$OPTARG"
wenzelm@32061
   156
        ;;
wenzelm@6212
   157
      r)
wenzelm@6212
   158
        RESET=true
wenzelm@6212
   159
        ;;
wenzelm@2917
   160
      s)
wenzelm@2917
   161
        SESSION="$OPTARG"
wenzelm@2917
   162
        ;;
wenzelm@31688
   163
      t)
wenzelm@31688
   164
        check_bool "$OPTARG"
wenzelm@31688
   165
        TIMING="$OPTARG"
wenzelm@31688
   166
        ;;
wenzelm@11577
   167
      v)
wenzelm@11577
   168
        check_bool "$OPTARG"
wenzelm@11577
   169
        VERBOSE="$OPTARG"
wenzelm@11577
   170
        ;;
wenzelm@2917
   171
      \?)
wenzelm@2917
   172
        usage
wenzelm@2917
   173
        ;;
wenzelm@2917
   174
    esac
wenzelm@2917
   175
  done
wenzelm@2917
   176
}
wenzelm@2808
   177
wenzelm@31307
   178
eval "OPTIONS=($ISABELLE_USEDIR_OPTIONS)"
wenzelm@31307
   179
getoptions "${OPTIONS[@]}"
wenzelm@2917
   180
wenzelm@2917
   181
getoptions "$@"
wenzelm@2808
   182
shift $(($OPTIND - 1))
wenzelm@2808
   183
wenzelm@2808
   184
wenzelm@2808
   185
# args
wenzelm@2808
   186
wenzelm@9788
   187
[ "$#" -ne 2 ] && usage
wenzelm@2808
   188
wenzelm@2808
   189
LOGIC="$1"; shift
wenzelm@2808
   190
NAME="$1"; shift
wenzelm@2808
   191
wenzelm@9788
   192
[ -z "$SESSION" ] && SESSION=$(basename "$NAME")
wenzelm@2808
   193
wenzelm@4419
   194
wenzelm@4419
   195
wenzelm@4419
   196
## main
berghofe@3636
   197
wenzelm@4451
   198
# prepare browser info dir
wenzelm@4419
   199
haftmann@25235
   200
if [ "$INFO" = "true" -a ! -f "$ISABELLE_BROWSER_INFO/index.html" ]; then
wenzelm@9788
   201
  mkdir -p "$ISABELLE_BROWSER_INFO"
wenzelm@9788
   202
  cp "$ISABELLE_HOME/lib/logo/isabelle.gif" "$ISABELLE_BROWSER_INFO/isabelle.gif"
haftmann@25234
   203
  cat "$ISABELLE_HOME/lib/html/library_index_header.template" \
haftmann@25234
   204
    "$ISABELLE_HOME/lib/html/library_index_content.template" \
haftmann@25234
   205
    "$ISABELLE_HOME/lib/html/library_index_footer.template"> "$ISABELLE_BROWSER_INFO/index.html"
berghofe@3636
   206
fi
berghofe@3636
   207
wenzelm@2808
   208
wenzelm@4451
   209
# prepare log dir
wenzelm@4451
   210
wenzelm@4451
   211
LOGDIR="$ISABELLE_OUTPUT/log"
wenzelm@4451
   212
mkdir -p "$LOGDIR"
wenzelm@4451
   213
wenzelm@4451
   214
wenzelm@4451
   215
# run isabelle
wenzelm@4451
   216
wenzelm@7737
   217
PARENT=$(basename "$LOGIC")
wenzelm@7737
   218
wenzelm@11949
   219
if [ -z "$BUILD" ]; then
wenzelm@11949
   220
  cd "$NAME" || fail "Bad session directory '$NAME'"
wenzelm@11949
   221
fi
wenzelm@4451
   222
wenzelm@11847
   223
if [ "$DOCUMENT" != false ]; then
wenzelm@8568
   224
  DOC="$DOCUMENT"
wenzelm@8568
   225
else
wenzelm@8568
   226
  DOC=""
wenzelm@8568
   227
fi
wenzelm@7737
   228
wenzelm@7737
   229
wenzelm@18321
   230
. "$ISABELLE_HOME/lib/scripts/timestart.bash"
wenzelm@6249
   231
wenzelm@2808
   232
if [ -n "$BUILD" ]; then
wenzelm@4451
   233
  ITEM="$SESSION"
wenzelm@11577
   234
  echo "Building $ITEM ..." >&2
wenzelm@4451
   235
  LOG="$LOGDIR/$ITEM"
wenzelm@4451
   236
wenzelm@28502
   237
  "$ISABELLE_PROCESS" \
wenzelm@31688
   238
    -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
   239
    -q -w $LOGIC $NAME > "$LOG"
wenzelm@9788
   240
  RC="$?"
wenzelm@2808
   241
else
wenzelm@9788
   242
  ITEM=$(basename "$LOGIC")-"$SESSION"
wenzelm@11577
   243
  echo "Running $ITEM ..." >&2
wenzelm@4451
   244
  LOG="$LOGDIR/$ITEM"
wenzelm@4451
   245
wenzelm@28502
   246
  "$ISABELLE_PROCESS" \
wenzelm@31688
   247
    -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
   248
    -r -q "$LOGIC" > "$LOG"
wenzelm@9788
   249
  RC="$?"
wenzelm@6212
   250
  cd ..
wenzelm@2808
   251
fi
wenzelm@4451
   252
wenzelm@18321
   253
. "$ISABELLE_HOME/lib/scripts/timestop.bash"
wenzelm@4451
   254
wenzelm@4451
   255
wenzelm@4451
   256
# exit status
wenzelm@4451
   257
wenzelm@9788
   258
if [ "$RC" -eq 0 ]; then
wenzelm@18321
   259
  echo "Finished $ITEM ($TIMES_REPORT)" >&2
wenzelm@4451
   260
  gzip --force "$LOG"
wenzelm@4451
   261
else
wenzelm@11577
   262
  { echo "$ITEM FAILED";
wenzelm@11577
   263
    echo "(see also $LOG)";
wenzelm@33830
   264
    echo; tail -40 "$LOG"; echo; } >&2
wenzelm@4451
   265
fi
wenzelm@4451
   266
wenzelm@9788
   267
exit "$RC"