lib/Tools/usedir
author wenzelm
Sun, 20 Jan 2013 13:59:13 +0100
changeset 50990 11996ea98bbe
parent 48445 cb4136e4cabf
permissions -rwxr-xr-x
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10555
2323ec838401 /usr/bin/env bash;
wenzelm
parents: 10511
diff changeset
     1
#!/usr/bin/env bash
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
     2
#
9788
wenzelm
parents: 9237
diff changeset
     3
# Author: Markus Wenzel, TU Muenchen
2808
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
10511
wenzelm
parents: 9788
diff changeset
    10
PRG="$(basename "$0")"
2808
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
28650
a7ba12e0d3b7 tuned usage line;
wenzelm
parents: 28502
diff changeset
    15
  echo "Usage: isabelle $PRG [OPTIONS] LOGIC NAME"
2808
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:"
17194
70d96933c210 added option -C: copy existing document directory;
wenzelm
parents: 17050
diff changeset
    18
  echo "    -C BOOL      copy existing document directory to -D PATH (default true)"
8197
baab8e487fad -D PATH: dump generated document sources into PATH;
wenzelm
parents: 7888
diff changeset
    19
  echo "    -D PATH      dump generated document sources into PATH"
23972
9c418fa38f7e added usedir option -M: max threads;
wenzelm
parents: 18321
diff changeset
    20
  echo "    -M MAX       multithreading: maximum number of worker threads (default 1)"
6940
ee6640456cbb -B option;
wenzelm
parents: 6652
diff changeset
    21
  echo "    -P PATH      set path for remote theory browsing information"
41703
d27950860514 parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents: 34261
diff changeset
    22
  echo "    -Q INT       set threshold for sub-proof parallelization (default 100)"
24118
464f260e5a20 multithreading trace: int;
wenzelm
parents: 24061
diff changeset
    23
  echo "    -T LEVEL     multithreading: trace level (default 0)"
42004
e06351ffb475 tuned terminology for document variants;
wenzelm
parents: 41703
diff changeset
    24
  echo "    -V VARIANT   declare alternative document VARIANT"
6212
974310f9ca7d Session.init;
wenzelm
parents: 5034
diff changeset
    25
  echo "    -b           build mode (output heap image, using current dir)"
7737
acaf55bee03e document preparation options: -c -d;
wenzelm
parents: 7461
diff changeset
    26
  echo "    -d FORMAT    build document as FORMAT (default false)"
15269
f856f4f3258f isatool usedir: ML root file can now be specified (previously hard-coded as ROOT.ML)
webertj
parents: 14981
diff changeset
    27
  echo "    -f NAME      use ML file NAME (default ROOT.ML)"
11847
82df5977101b option -g for document graph;
wenzelm
parents: 11577
diff changeset
    28
  echo "    -g BOOL      generate session graph image for document (default false)"
82df5977101b option -g for document graph;
wenzelm
parents: 11577
diff changeset
    29
  echo "    -i BOOL      generate HTML and graph browser information (default false)"
10562
fcd29e58c40c option -m;
wenzelm
parents: 10555
diff changeset
    30
  echo "    -m MODE      add print mode for output"
32061
11f8ee55662d parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
wenzelm
parents: 31688
diff changeset
    31
  echo "    -p LEVEL     set level of detail for proof objects (default 0)"
11f8ee55662d parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
wenzelm
parents: 31688
diff changeset
    32
  echo "    -q LEVEL     set level of parallel proof checking (default 1)"
6212
974310f9ca7d Session.init;
wenzelm
parents: 5034
diff changeset
    33
  echo "    -r           reset session path"
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    34
  echo "    -s NAME      override session NAME"
31688
f27cc190083b usedir: internal timing option;
wenzelm
parents: 31317
diff changeset
    35
  echo "    -t BOOL      internal session timing (default false)"
11577
68323aa9575d option -v;
wenzelm
parents: 11543
diff changeset
    36
  echo "    -v BOOL      be verbose (default false)"
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    37
  echo
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    38
  echo "  Build object-logic or run examples. Also creates browsing"
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    39
  echo "  information (HTML etc.) according to settings."
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    40
  echo
7461
94ae093f6706 usage: tell ISABELLE_USEDIR_OPTIONS;
wenzelm
parents: 7276
diff changeset
    41
  echo "  ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
94ae093f6706 usage: tell ISABELLE_USEDIR_OPTIONS;
wenzelm
parents: 7276
diff changeset
    42
  echo
29089
8cffa980bd93 usage: echo ML settings as well;
wenzelm
parents: 28650
diff changeset
    43
  echo "  ML_PLATFORM=$ML_PLATFORM"
8cffa980bd93 usage: echo ML settings as well;
wenzelm
parents: 28650
diff changeset
    44
  echo "  ML_HOME=$ML_HOME"
8cffa980bd93 usage: echo ML settings as well;
wenzelm
parents: 28650
diff changeset
    45
  echo "  ML_SYSTEM=$ML_SYSTEM"
8cffa980bd93 usage: echo ML settings as well;
wenzelm
parents: 28650
diff changeset
    46
  echo "  ML_OPTIONS=$ML_OPTIONS"
8cffa980bd93 usage: echo ML settings as well;
wenzelm
parents: 28650
diff changeset
    47
  echo
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    48
  exit 1
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    49
}
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    50
11577
68323aa9575d option -v;
wenzelm
parents: 11543
diff changeset
    51
function fail()
68323aa9575d option -v;
wenzelm
parents: 11543
diff changeset
    52
{
68323aa9575d option -v;
wenzelm
parents: 11543
diff changeset
    53
  echo "$1" >&2
68323aa9575d option -v;
wenzelm
parents: 11543
diff changeset
    54
  exit 2
68323aa9575d option -v;
wenzelm
parents: 11543
diff changeset
    55
}
68323aa9575d option -v;
wenzelm
parents: 11543
diff changeset
    56
68323aa9575d option -v;
wenzelm
parents: 11543
diff changeset
    57
function check_bool()
68323aa9575d option -v;
wenzelm
parents: 11543
diff changeset
    58
{
68323aa9575d option -v;
wenzelm
parents: 11543
diff changeset
    59
  [ "$1" = true -o "$1" = false ] || fail "Bad boolean: \"$1\""
68323aa9575d option -v;
wenzelm
parents: 11543
diff changeset
    60
}
68323aa9575d option -v;
wenzelm
parents: 11543
diff changeset
    61
68323aa9575d option -v;
wenzelm
parents: 11543
diff changeset
    62
function check_number()
68323aa9575d option -v;
wenzelm
parents: 11543
diff changeset
    63
{
12912
0e144958cf27 tr: quote argument;
wenzelm
parents: 11949
diff changeset
    64
  [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
11577
68323aa9575d option -v;
wenzelm
parents: 11543
diff changeset
    65
}
68323aa9575d option -v;
wenzelm
parents: 11543
diff changeset
    66
2808
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
## process command line
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
# options
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    71
24061
68d2b6cf5194 added option -T (multithreading trace mode);
wenzelm
parents: 23972
diff changeset
    72
COPY_DUMP=true
8197
baab8e487fad -D PATH: dump generated document sources into PATH;
wenzelm
parents: 7888
diff changeset
    73
DUMP=""
23972
9c418fa38f7e added usedir option -M: max threads;
wenzelm
parents: 18321
diff changeset
    74
MAXTHREADS="1"
8197
baab8e487fad -D PATH: dump generated document sources into PATH;
wenzelm
parents: 7888
diff changeset
    75
RPATH=""
24118
464f260e5a20 multithreading trace: int;
wenzelm
parents: 24061
diff changeset
    76
TRACETHREADS="0"
42004
e06351ffb475 tuned terminology for document variants;
wenzelm
parents: 41703
diff changeset
    77
DOCUMENT_VARIANTS=""
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    78
BUILD=""
7737
acaf55bee03e document preparation options: -c -d;
wenzelm
parents: 7461
diff changeset
    79
DOCUMENT=false
17050
bfb571252817 added option -V VERSION;
wenzelm
parents: 15474
diff changeset
    80
ROOT_FILE="ROOT.ML"
11847
82df5977101b option -g for document graph;
wenzelm
parents: 11577
diff changeset
    81
DOCUMENT_GRAPH=false
3747
cd9b6c86926c There is now one single option -i for generating theory browsing
berghofe
parents: 3636
diff changeset
    82
INFO=false
10562
fcd29e58c40c option -m;
wenzelm
parents: 10555
diff changeset
    83
MODES=""
6212
974310f9ca7d Session.init;
wenzelm
parents: 5034
diff changeset
    84
RESET=false
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    85
SESSION=""
32061
11f8ee55662d parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
wenzelm
parents: 31688
diff changeset
    86
PROOFS="0"
11f8ee55662d parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
wenzelm
parents: 31688
diff changeset
    87
PARALLEL_PROOFS="1"
41703
d27950860514 parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents: 34261
diff changeset
    88
PARALLEL_PROOFS_THRESHOLD="100"
31688
f27cc190083b usedir: internal timing option;
wenzelm
parents: 31317
diff changeset
    89
TIMING=false
11577
68323aa9575d option -v;
wenzelm
parents: 11543
diff changeset
    90
VERBOSE=false
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
    91
2917
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    92
function getoptions()
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    93
{
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    94
  OPTIND=1
41703
d27950860514 parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents: 34261
diff changeset
    95
  while getopts "C:D:M:P:Q:T:V:bd:f:g:i:m:p:q:rs:t:v:" OPT
2917
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    96
  do
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
    97
    case "$OPT" in
17194
70d96933c210 added option -C: copy existing document directory;
wenzelm
parents: 17050
diff changeset
    98
      C)
70d96933c210 added option -C: copy existing document directory;
wenzelm
parents: 17050
diff changeset
    99
        check_bool "$OPTARG"
70d96933c210 added option -C: copy existing document directory;
wenzelm
parents: 17050
diff changeset
   100
        COPY_DUMP="$OPTARG"
70d96933c210 added option -C: copy existing document directory;
wenzelm
parents: 17050
diff changeset
   101
        ;;
8197
baab8e487fad -D PATH: dump generated document sources into PATH;
wenzelm
parents: 7888
diff changeset
   102
      D)
baab8e487fad -D PATH: dump generated document sources into PATH;
wenzelm
parents: 7888
diff changeset
   103
        DUMP="$OPTARG"
baab8e487fad -D PATH: dump generated document sources into PATH;
wenzelm
parents: 7888
diff changeset
   104
        ;;
23972
9c418fa38f7e added usedir option -M: max threads;
wenzelm
parents: 18321
diff changeset
   105
      M)
25774
28fac5c2af54 added usedir -M max (alias for -M 0);
wenzelm
parents: 25235
diff changeset
   106
        if [ "$OPTARG" = max ]; then
29435
a5f84ac14609 added parallel_proofs flag (default true, cf. usedir option -Q), which can be disabled in low-memory situations;
wenzelm
parents: 29143
diff changeset
   107
          MAXTHREADS=0
a5f84ac14609 added parallel_proofs flag (default true, cf. usedir option -Q), which can be disabled in low-memory situations;
wenzelm
parents: 29143
diff changeset
   108
        else
25774
28fac5c2af54 added usedir -M max (alias for -M 0);
wenzelm
parents: 25235
diff changeset
   109
          check_number "$OPTARG"
28fac5c2af54 added usedir -M max (alias for -M 0);
wenzelm
parents: 25235
diff changeset
   110
          MAXTHREADS="$OPTARG"
29435
a5f84ac14609 added parallel_proofs flag (default true, cf. usedir option -Q), which can be disabled in low-memory situations;
wenzelm
parents: 29143
diff changeset
   111
        fi
23972
9c418fa38f7e added usedir option -M: max threads;
wenzelm
parents: 18321
diff changeset
   112
        ;;
8197
baab8e487fad -D PATH: dump generated document sources into PATH;
wenzelm
parents: 7888
diff changeset
   113
      P)
baab8e487fad -D PATH: dump generated document sources into PATH;
wenzelm
parents: 7888
diff changeset
   114
        RPATH="$OPTARG"
baab8e487fad -D PATH: dump generated document sources into PATH;
wenzelm
parents: 7888
diff changeset
   115
        ;;
41703
d27950860514 parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents: 34261
diff changeset
   116
      Q)
d27950860514 parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents: 34261
diff changeset
   117
        check_number "$OPTARG"
d27950860514 parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents: 34261
diff changeset
   118
        PARALLEL_PROOFS_THRESHOLD="$OPTARG"
d27950860514 parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents: 34261
diff changeset
   119
        ;;
24061
68d2b6cf5194 added option -T (multithreading trace mode);
wenzelm
parents: 23972
diff changeset
   120
      T)
24118
464f260e5a20 multithreading trace: int;
wenzelm
parents: 24061
diff changeset
   121
        check_number "$OPTARG"
24061
68d2b6cf5194 added option -T (multithreading trace mode);
wenzelm
parents: 23972
diff changeset
   122
        TRACETHREADS="$OPTARG"
68d2b6cf5194 added option -T (multithreading trace mode);
wenzelm
parents: 23972
diff changeset
   123
        ;;
17050
bfb571252817 added option -V VERSION;
wenzelm
parents: 15474
diff changeset
   124
      V)
42004
e06351ffb475 tuned terminology for document variants;
wenzelm
parents: 41703
diff changeset
   125
        if [ -z "$DOCUMENT_VARIANTS" ]; then
e06351ffb475 tuned terminology for document variants;
wenzelm
parents: 41703
diff changeset
   126
          DOCUMENT_VARIANTS="\"$OPTARG\""
17050
bfb571252817 added option -V VERSION;
wenzelm
parents: 15474
diff changeset
   127
        else
42004
e06351ffb475 tuned terminology for document variants;
wenzelm
parents: 41703
diff changeset
   128
          DOCUMENT_VARIANTS="$DOCUMENT_VARIANTS, \"$OPTARG\""
17050
bfb571252817 added option -V VERSION;
wenzelm
parents: 15474
diff changeset
   129
        fi
bfb571252817 added option -V VERSION;
wenzelm
parents: 15474
diff changeset
   130
        ;;
2917
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
   131
      b)
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
   132
        BUILD=true
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
   133
        ;;
7737
acaf55bee03e document preparation options: -c -d;
wenzelm
parents: 7461
diff changeset
   134
      d)
acaf55bee03e document preparation options: -c -d;
wenzelm
parents: 7461
diff changeset
   135
        DOCUMENT="$OPTARG"
acaf55bee03e document preparation options: -c -d;
wenzelm
parents: 7461
diff changeset
   136
        ;;
15269
f856f4f3258f isatool usedir: ML root file can now be specified (previously hard-coded as ROOT.ML)
webertj
parents: 14981
diff changeset
   137
      f)
f856f4f3258f isatool usedir: ML root file can now be specified (previously hard-coded as ROOT.ML)
webertj
parents: 14981
diff changeset
   138
        ROOT_FILE="$OPTARG"
f856f4f3258f isatool usedir: ML root file can now be specified (previously hard-coded as ROOT.ML)
webertj
parents: 14981
diff changeset
   139
        ;;
11847
82df5977101b option -g for document graph;
wenzelm
parents: 11577
diff changeset
   140
      g)
82df5977101b option -g for document graph;
wenzelm
parents: 11577
diff changeset
   141
        check_bool "$OPTARG"
82df5977101b option -g for document graph;
wenzelm
parents: 11577
diff changeset
   142
        DOCUMENT_GRAPH="$OPTARG"
82df5977101b option -g for document graph;
wenzelm
parents: 11577
diff changeset
   143
        ;;
3747
cd9b6c86926c There is now one single option -i for generating theory browsing
berghofe
parents: 3636
diff changeset
   144
      i)
11577
68323aa9575d option -v;
wenzelm
parents: 11543
diff changeset
   145
        check_bool "$OPTARG"
3747
cd9b6c86926c There is now one single option -i for generating theory browsing
berghofe
parents: 3636
diff changeset
   146
        INFO="$OPTARG"
2917
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
   147
        ;;
10562
fcd29e58c40c option -m;
wenzelm
parents: 10555
diff changeset
   148
      m)
fcd29e58c40c option -m;
wenzelm
parents: 10555
diff changeset
   149
        if [ -z "$MODES" ]; then
fcd29e58c40c option -m;
wenzelm
parents: 10555
diff changeset
   150
          MODES="\"$OPTARG\""
fcd29e58c40c option -m;
wenzelm
parents: 10555
diff changeset
   151
        else
10585
58a1ed1edb65 proper order of modes;
wenzelm
parents: 10562
diff changeset
   152
          MODES="\"$OPTARG\", $MODES"
10562
fcd29e58c40c option -m;
wenzelm
parents: 10555
diff changeset
   153
        fi
fcd29e58c40c option -m;
wenzelm
parents: 10555
diff changeset
   154
        ;;
11535
7f4c5cdea239 Added new option for setting level of detail for proof objects.
berghofe
parents: 10585
diff changeset
   155
      p)
11577
68323aa9575d option -v;
wenzelm
parents: 11543
diff changeset
   156
        check_number "$OPTARG"
11543
d61b913431c5 renamed `keep_derivs' to `proofs', and made an integer;
wenzelm
parents: 11535
diff changeset
   157
        PROOFS="$OPTARG"
11535
7f4c5cdea239 Added new option for setting level of detail for proof objects.
berghofe
parents: 10585
diff changeset
   158
        ;;
32061
11f8ee55662d parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
wenzelm
parents: 31688
diff changeset
   159
      q)
11f8ee55662d parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
wenzelm
parents: 31688
diff changeset
   160
        check_number "$OPTARG"
11f8ee55662d parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
wenzelm
parents: 31688
diff changeset
   161
        PARALLEL_PROOFS="$OPTARG"
11f8ee55662d parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
wenzelm
parents: 31688
diff changeset
   162
        ;;
6212
974310f9ca7d Session.init;
wenzelm
parents: 5034
diff changeset
   163
      r)
974310f9ca7d Session.init;
wenzelm
parents: 5034
diff changeset
   164
        RESET=true
974310f9ca7d Session.init;
wenzelm
parents: 5034
diff changeset
   165
        ;;
2917
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
   166
      s)
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
   167
        SESSION="$OPTARG"
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
   168
        ;;
31688
f27cc190083b usedir: internal timing option;
wenzelm
parents: 31317
diff changeset
   169
      t)
f27cc190083b usedir: internal timing option;
wenzelm
parents: 31317
diff changeset
   170
        check_bool "$OPTARG"
f27cc190083b usedir: internal timing option;
wenzelm
parents: 31317
diff changeset
   171
        TIMING="$OPTARG"
f27cc190083b usedir: internal timing option;
wenzelm
parents: 31317
diff changeset
   172
        ;;
11577
68323aa9575d option -v;
wenzelm
parents: 11543
diff changeset
   173
      v)
68323aa9575d option -v;
wenzelm
parents: 11543
diff changeset
   174
        check_bool "$OPTARG"
68323aa9575d option -v;
wenzelm
parents: 11543
diff changeset
   175
        VERBOSE="$OPTARG"
68323aa9575d option -v;
wenzelm
parents: 11543
diff changeset
   176
        ;;
2917
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
   177
      \?)
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
   178
        usage
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
   179
        ;;
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
   180
    esac
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
   181
  done
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
   182
}
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
   183
31307
7015fee8c3e8 ISABELLE_USEDIR_OPTIONS: proper word splitting of quoted options (via array variable and special expansion, cf. "$@");
wenzelm
parents: 29435
diff changeset
   184
eval "OPTIONS=($ISABELLE_USEDIR_OPTIONS)"
7015fee8c3e8 ISABELLE_USEDIR_OPTIONS: proper word splitting of quoted options (via array variable and special expansion, cf. "$@");
wenzelm
parents: 29435
diff changeset
   185
getoptions "${OPTIONS[@]}"
2917
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
   186
c7411fce37e4 added -g, -h options;
wenzelm
parents: 2849
diff changeset
   187
getoptions "$@"
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
   188
shift $(($OPTIND - 1))
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
   189
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
   190
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
   191
# args
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
   192
9788
wenzelm
parents: 9237
diff changeset
   193
[ "$#" -ne 2 ] && usage
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
   194
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
   195
LOGIC="$1"; shift
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
   196
NAME="$1"; shift
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
   197
9788
wenzelm
parents: 9237
diff changeset
   198
[ -z "$SESSION" ] && SESSION=$(basename "$NAME")
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
   199
4419
wenzelm
parents: 4075
diff changeset
   200
wenzelm
parents: 4075
diff changeset
   201
wenzelm
parents: 4075
diff changeset
   202
## main
3636
3f2e55e5bacc Added some code for generating theory browsing data.
berghofe
parents: 3504
diff changeset
   203
4451
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   204
# prepare browser info dir
4419
wenzelm
parents: 4075
diff changeset
   205
25235
04cb7e02ca38 split library index into templates
haftmann
parents: 25234
diff changeset
   206
if [ "$INFO" = "true" -a ! -f "$ISABELLE_BROWSER_INFO/index.html" ]; then
9788
wenzelm
parents: 9237
diff changeset
   207
  mkdir -p "$ISABELLE_BROWSER_INFO"
wenzelm
parents: 9237
diff changeset
   208
  cp "$ISABELLE_HOME/lib/logo/isabelle.gif" "$ISABELLE_BROWSER_INFO/isabelle.gif"
25234
2e91cc4ddf29 split library index into templates
haftmann
parents: 24957
diff changeset
   209
  cat "$ISABELLE_HOME/lib/html/library_index_header.template" \
2e91cc4ddf29 split library index into templates
haftmann
parents: 24957
diff changeset
   210
    "$ISABELLE_HOME/lib/html/library_index_content.template" \
2e91cc4ddf29 split library index into templates
haftmann
parents: 24957
diff changeset
   211
    "$ISABELLE_HOME/lib/html/library_index_footer.template"> "$ISABELLE_BROWSER_INFO/index.html"
3636
3f2e55e5bacc Added some code for generating theory browsing data.
berghofe
parents: 3504
diff changeset
   212
fi
3f2e55e5bacc Added some code for generating theory browsing data.
berghofe
parents: 3504
diff changeset
   213
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
   214
4451
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   215
# prepare log dir
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   216
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   217
LOGDIR="$ISABELLE_OUTPUT/log"
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   218
mkdir -p "$LOGDIR"
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   219
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   220
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   221
# run isabelle
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   222
7737
acaf55bee03e document preparation options: -c -d;
wenzelm
parents: 7461
diff changeset
   223
PARENT=$(basename "$LOGIC")
acaf55bee03e document preparation options: -c -d;
wenzelm
parents: 7461
diff changeset
   224
11949
wenzelm
parents: 11907
diff changeset
   225
if [ -z "$BUILD" ]; then
wenzelm
parents: 11907
diff changeset
   226
  cd "$NAME" || fail "Bad session directory '$NAME'"
wenzelm
parents: 11907
diff changeset
   227
fi
4451
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   228
11847
82df5977101b option -g for document graph;
wenzelm
parents: 11577
diff changeset
   229
if [ "$DOCUMENT" != false ]; then
8568
wenzelm
parents: 8565
diff changeset
   230
  DOC="$DOCUMENT"
wenzelm
parents: 8565
diff changeset
   231
else
wenzelm
parents: 8565
diff changeset
   232
  DOC=""
wenzelm
parents: 8565
diff changeset
   233
fi
7737
acaf55bee03e document preparation options: -c -d;
wenzelm
parents: 7461
diff changeset
   234
acaf55bee03e document preparation options: -c -d;
wenzelm
parents: 7461
diff changeset
   235
18321
3414557c2dda replaced lib/scripts/showtime by more advanced lib/scripts/timestart|stop.bash;
wenzelm
parents: 17194
diff changeset
   236
. "$ISABELLE_HOME/lib/scripts/timestart.bash"
6249
8bb90076cc7c Session.use_dir: check parent;
wenzelm
parents: 6212
diff changeset
   237
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
   238
if [ -n "$BUILD" ]; then
4451
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   239
  ITEM="$SESSION"
11577
68323aa9575d option -v;
wenzelm
parents: 11543
diff changeset
   240
  echo "Building $ITEM ..." >&2
4451
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   241
  LOG="$LOGDIR/$ITEM"
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   242
28502
6b0e3e4e1891 replaced ISABELLE by ISABELLE_PROCESS;
wenzelm
parents: 25774
diff changeset
   243
  "$ISABELLE_PROCESS" \
48445
cb4136e4cabf pass ISABELLE_BROWSER_INFO as explicit argument;
wenzelm
parents: 42004
diff changeset
   244
    -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$ISABELLE_BROWSER_INFO\" \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD;" \
31317
1f5740424c69 removed "compress" option from isabelle-process and isabelle usedir -- this is always enabled;
wenzelm
parents: 31307
diff changeset
   245
    -q -w $LOGIC $NAME > "$LOG"
9788
wenzelm
parents: 9237
diff changeset
   246
  RC="$?"
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
   247
else
9788
wenzelm
parents: 9237
diff changeset
   248
  ITEM=$(basename "$LOGIC")-"$SESSION"
11577
68323aa9575d option -v;
wenzelm
parents: 11543
diff changeset
   249
  echo "Running $ITEM ..." >&2
4451
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   250
  LOG="$LOGDIR/$ITEM"
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   251
28502
6b0e3e4e1891 replaced ISABELLE by ISABELLE_PROCESS;
wenzelm
parents: 25774
diff changeset
   252
  "$ISABELLE_PROCESS" \
48445
cb4136e4cabf pass ISABELLE_BROWSER_INFO as explicit argument;
wenzelm
parents: 42004
diff changeset
   253
    -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$ISABELLE_BROWSER_INFO\" \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD; quit();" \
11577
68323aa9575d option -v;
wenzelm
parents: 11543
diff changeset
   254
    -r -q "$LOGIC" > "$LOG"
9788
wenzelm
parents: 9237
diff changeset
   255
  RC="$?"
6212
974310f9ca7d Session.init;
wenzelm
parents: 5034
diff changeset
   256
  cd ..
2808
e8a224e41b9f usedir -- build object-logic or run examples;
wenzelm
parents:
diff changeset
   257
fi
4451
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   258
18321
3414557c2dda replaced lib/scripts/showtime by more advanced lib/scripts/timestart|stop.bash;
wenzelm
parents: 17194
diff changeset
   259
. "$ISABELLE_HOME/lib/scripts/timestop.bash"
4451
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   260
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   261
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   262
# exit status
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   263
9788
wenzelm
parents: 9237
diff changeset
   264
if [ "$RC" -eq 0 ]; then
18321
3414557c2dda replaced lib/scripts/showtime by more advanced lib/scripts/timestart|stop.bash;
wenzelm
parents: 17194
diff changeset
   265
  echo "Finished $ITEM ($TIMES_REPORT)" >&2
4451
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   266
  gzip --force "$LOG"
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   267
else
11577
68323aa9575d option -v;
wenzelm
parents: 11543
diff changeset
   268
  { echo "$ITEM FAILED";
68323aa9575d option -v;
wenzelm
parents: 11543
diff changeset
   269
    echo "(see also $LOG)";
34261
8e36b3ac6083 slightly shorter tail (again) -- theory loader produces less warning spam (cf. 2524c1bbd087);
wenzelm
parents: 34238
diff changeset
   270
    echo; tail -20 "$LOG"; echo; } >&2
4451
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   271
fi
f9e3e9f1af61 log file;
wenzelm
parents: 4419
diff changeset
   272
9788
wenzelm
parents: 9237
diff changeset
   273
exit "$RC"