Admin/makebin
author wenzelm
Tue, 15 Sep 2009 23:57:07 +0200
changeset 32576 20b261654e33
parent 30862 dfd77f471c22
child 33918 5945e023bab7
permissions -rwxr-xr-x
double linking for improved performance of "prev"; misc tuning;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12721
226fc0e2e7e3 #!/usr/bin/env bash;
wenzelm
parents: 12427
diff changeset
     1
#!/usr/bin/env bash
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
     2
#
30862
dfd77f471c22 single-threaded build;
wenzelm
parents: 28504
diff changeset
     3
# makebin -- make Isabelle logic images for current platform
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
     4
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
     5
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
     6
## global settings
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
     7
12427
37cfec8dfe8e use /var/tmp (which happens to be more spacious on atbroy37);
wenzelm
parents: 11576
diff changeset
     8
TMP="/var/tmp/isabelle-makebin$$"
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
     9
27030
8c558af86e21 THIS_IS_ISABELLE_MAKEBIN is back;
wenzelm
parents: 26209
diff changeset
    10
export THIS_IS_ISABELLE_MAKEBIN=true
8c558af86e21 THIS_IS_ISABELLE_MAKEBIN is back;
wenzelm
parents: 26209
diff changeset
    11
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    12
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    13
## diagnostics
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    14
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    15
PRG=$(basename "$0")
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    16
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    17
function usage()
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    18
{
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    19
  echo
12827
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    20
  echo "Usage: $PRG [OPTIONS] ARCHIVE"
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    21
  echo
12827
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    22
  echo "  Options are:"
13001
40ba2eee948e clarified -l option;
wenzelm
parents: 12985
diff changeset
    23
  echo "    -l           produce library"
40ba2eee948e clarified -l option;
wenzelm
parents: 12985
diff changeset
    24
  echo "    -n           dry run"
12827
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    25
  echo
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    26
  echo "  Precompile Isabelle for the current platform."
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    27
  echo
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    28
  exit 1
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    29
}
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    30
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    31
function fail()
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    32
{
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    33
  echo "$1" >&2
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    34
  exit 2
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    35
}
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    36
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    37
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    38
## process command line
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    39
12827
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    40
# options
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    41
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    42
DO_LIBRARY=""
13001
40ba2eee948e clarified -l option;
wenzelm
parents: 12985
diff changeset
    43
DRY_RUN=""
12827
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    44
13001
40ba2eee948e clarified -l option;
wenzelm
parents: 12985
diff changeset
    45
while getopts "ln" OPT
12827
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    46
do
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    47
  case "$OPT" in
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    48
    l)
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    49
      DO_LIBRARY=true
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    50
      ;;
13001
40ba2eee948e clarified -l option;
wenzelm
parents: 12985
diff changeset
    51
    n)
40ba2eee948e clarified -l option;
wenzelm
parents: 12985
diff changeset
    52
      DRY_RUN=true
12827
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    53
      ;;
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    54
    \?)
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    55
      usage
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    56
      ;;
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    57
  esac
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    58
done
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    59
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    60
shift $(($OPTIND - 1))
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    61
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    62
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    63
# args
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    64
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    65
[ "$#" -gt 1 ] && usage
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    66
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    67
ARCHIVE="$1"; shift
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    68
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    69
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    70
## main
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    71
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    72
[ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
30862
dfd77f471c22 single-threaded build;
wenzelm
parents: 28504
diff changeset
    73
ARCHIVE_BASE="$(basename "$ARCHIVE")"
dfd77f471c22 single-threaded build;
wenzelm
parents: 28504
diff changeset
    74
ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")"
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    75
ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE"
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    76
30862
dfd77f471c22 single-threaded build;
wenzelm
parents: 28504
diff changeset
    77
ISABELLE_NAME="$(basename "$ARCHIVE_BASE" .tar.gz)"
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    78
ISABELLE_HOME="$TMP/$ISABELLE_NAME"
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    79
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    80
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    81
# build logics
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    82
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    83
mkdir "$TMP" || fail "Cannot create directory $TMP"
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    84
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    85
cd "$TMP"
30862
dfd77f471c22 single-threaded build;
wenzelm
parents: 28504
diff changeset
    86
tar xzf "$ARCHIVE_FULL"
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    87
cd "$ISABELLE_NAME"
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    88
17575
wenzelm
parents: 17573
diff changeset
    89
perl -pi \
30862
dfd77f471c22 single-threaded build;
wenzelm
parents: 28504
diff changeset
    90
  -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -p 1":;' \
dfd77f471c22 single-threaded build;
wenzelm
parents: 28504
diff changeset
    91
  -e 's:^HOL_USEDIR_OPTIONS=.*$:HOL_USEDIR_OPTIONS="-M 1 -p 2":;' \
17575
wenzelm
parents: 17573
diff changeset
    92
  etc/settings
wenzelm
parents: 17573
diff changeset
    93
13001
40ba2eee948e clarified -l option;
wenzelm
parents: 12985
diff changeset
    94
if [ -n "$DO_LIBRARY" ]; then
30862
dfd77f471c22 single-threaded build;
wenzelm
parents: 28504
diff changeset
    95
  perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -p 1 -i true -d pdf -V outline=/proof,/ML":;' \
13001
40ba2eee948e clarified -l option;
wenzelm
parents: 12985
diff changeset
    96
    etc/settings
40ba2eee948e clarified -l option;
wenzelm
parents: 12985
diff changeset
    97
fi
11576
c418146c4763 activate default ISABELLE_USEDIR_OPTIONS for precompiled distribution;
wenzelm
parents: 10307
diff changeset
    98
28504
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 27588
diff changeset
    99
ISABELLE_HOME_USER=$(./bin/isabelle getenv -b ISABELLE_HOME_USER)
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   100
[ -f "$ISABELLE_HOME_USER/etc/settings" ] && \
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   101
  echo "### WARNING!  Personal Isabelle settings present. " >&2
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   102
28504
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 27588
diff changeset
   103
COMPILER=$(./bin/isabelle getenv -b ML_IDENTIFIER)
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 27588
diff changeset
   104
PLATFORM=$(./bin/isabelle getenv -b ML_PLATFORM)
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   105
13001
40ba2eee948e clarified -l option;
wenzelm
parents: 12985
diff changeset
   106
if [ -n "$DRY_RUN" ]; then
12827
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
   107
  mkdir -p "heaps/$COMPILER/log"
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   108
  touch "heaps/$COMPILER/HOL"
12827
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
   109
  touch "heaps/$COMPILER/log/HOL.gz"
27587
6f469a8aff10 added HOL-Nominal image;
wenzelm
parents: 27030
diff changeset
   110
  touch "heaps/$COMPILER/HOL-Nominal"
6f469a8aff10 added HOL-Nominal image;
wenzelm
parents: 27030
diff changeset
   111
  touch "heaps/$COMPILER/log/HOL-Nominal.gz"
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   112
  touch "heaps/$COMPILER/ZF"
12827
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
   113
  touch "heaps/$COMPILER/log/ZF.gz"
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
   114
  mkdir browser_info
13001
40ba2eee948e clarified -l option;
wenzelm
parents: 12985
diff changeset
   115
elif [ -n "$DO_LIBRARY" ]; then
40ba2eee948e clarified -l option;
wenzelm
parents: 12985
diff changeset
   116
  ./build -bait
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   117
else
27587
6f469a8aff10 added HOL-Nominal image;
wenzelm
parents: 27030
diff changeset
   118
  ./build -b -m HOL-Nominal HOL
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   119
  ./build -b ZF
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   120
  rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL"
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   121
fi
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   122
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   123
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   124
# prepare result
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   125
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   126
cd "$TMP"
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   127
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   128
chmod -R g=o "$TMP"
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   129
chgrp -R isabelle "$TMP"
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   130
13001
40ba2eee948e clarified -l option;
wenzelm
parents: 12985
diff changeset
   131
if [ -n "$DO_LIBRARY" ]; then
30862
dfd77f471c22 single-threaded build;
wenzelm
parents: 28504
diff changeset
   132
  tar cf "${ISABELLE_NAME}_library.tar" $ISABELLE_NAME/browser_info && \
13001
40ba2eee948e clarified -l option;
wenzelm
parents: 12985
diff changeset
   133
    gzip -f "${ISABELLE_NAME}_library.tar"
40ba2eee948e clarified -l option;
wenzelm
parents: 12985
diff changeset
   134
    cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR"
40ba2eee948e clarified -l option;
wenzelm
parents: 12985
diff changeset
   135
else
27588
0dd8d4c558f9 removed HOL-Complex, which has been discontinued after Isabelle2008;
wenzelm
parents: 27587
diff changeset
   136
  for IMG in HOL HOL-Nominal ZF
13001
40ba2eee948e clarified -l option;
wenzelm
parents: 12985
diff changeset
   137
  do
30862
dfd77f471c22 single-threaded build;
wenzelm
parents: 28504
diff changeset
   138
    tar cf "${IMG}_$PLATFORM.tar" \
13001
40ba2eee948e clarified -l option;
wenzelm
parents: 12985
diff changeset
   139
      "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \
40ba2eee948e clarified -l option;
wenzelm
parents: 12985
diff changeset
   140
      "$ISABELLE_NAME/heaps/$COMPILER/log/$IMG.gz"
40ba2eee948e clarified -l option;
wenzelm
parents: 12985
diff changeset
   141
    gzip -f "${IMG}_$PLATFORM.tar"
40ba2eee948e clarified -l option;
wenzelm
parents: 12985
diff changeset
   142
    cp -f "${IMG}_$PLATFORM.tar.gz" "$ARCHIVE_DIR"
40ba2eee948e clarified -l option;
wenzelm
parents: 12985
diff changeset
   143
  done
40ba2eee948e clarified -l option;
wenzelm
parents: 12985
diff changeset
   144
fi
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   145
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   146
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   147
# clean up
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   148
cd /tmp
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   149
rm -rf "$TMP"