Admin/Release/makebin
author wenzelm
Fri, 17 Aug 2012 11:23:57 +0200
changeset 48835 574042d14fd9
parent 48190 76b6207eb000
permissions -rwxr-xr-x
tuned;
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
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    10
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    11
## diagnostics
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
PRG=$(basename "$0")
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
function usage()
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
  echo
12827
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    18
  echo "Usage: $PRG [OPTIONS] ARCHIVE"
10082
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 "  Options are:"
13001
40ba2eee948e clarified -l option;
wenzelm
parents: 12985
diff changeset
    21
  echo "    -l           produce library"
12827
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    22
  echo
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    23
  echo "  Precompile Isabelle for the current platform."
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    24
  echo
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    25
  exit 1
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    26
}
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    27
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    28
function fail()
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
  echo "$1" >&2
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    31
  exit 2
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
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    34
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    35
## process command line
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    36
12827
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    37
# options
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    38
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    39
DO_LIBRARY=""
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    40
44877
a4761fc03ee7 misc tuning and clarification (NB: settings are already local for named snapshots/releases);
wenzelm
parents: 41556
diff changeset
    41
while getopts "l" OPT
12827
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    42
do
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    43
  case "$OPT" in
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    44
    l)
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    45
      DO_LIBRARY=true
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    46
      ;;
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    47
    \?)
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    48
      usage
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    49
      ;;
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    50
  esac
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    51
done
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    52
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    53
shift $(($OPTIND - 1))
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    54
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    55
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    56
# args
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    57
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    58
[ "$#" -gt 1 ] && usage
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    59
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    60
ARCHIVE="$1"; shift
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    61
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    62
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    63
## main
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    64
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    65
[ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
30862
dfd77f471c22 single-threaded build;
wenzelm
parents: 28504
diff changeset
    66
ARCHIVE_BASE="$(basename "$ARCHIVE")"
dfd77f471c22 single-threaded build;
wenzelm
parents: 28504
diff changeset
    67
ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")"
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    68
ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE"
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    69
30862
dfd77f471c22 single-threaded build;
wenzelm
parents: 28504
diff changeset
    70
ISABELLE_NAME="$(basename "$ARCHIVE_BASE" .tar.gz)"
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    71
ISABELLE_HOME="$TMP/$ISABELLE_NAME"
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    72
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    73
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    74
# build logics
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    75
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    76
mkdir "$TMP" || fail "Cannot create directory $TMP"
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    77
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    78
cd "$TMP"
30862
dfd77f471c22 single-threaded build;
wenzelm
parents: 28504
diff changeset
    79
tar xzf "$ARCHIVE_FULL"
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    80
cd "$ISABELLE_NAME"
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    81
17575
wenzelm
parents: 17573
diff changeset
    82
perl -pi \
37286
344468462338 removed obsolete usedir -p 1 option;
wenzelm
parents: 34238
diff changeset
    83
  -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1":;' \
17575
wenzelm
parents: 17573
diff changeset
    84
  etc/settings
wenzelm
parents: 17573
diff changeset
    85
13001
40ba2eee948e clarified -l option;
wenzelm
parents: 12985
diff changeset
    86
if [ -n "$DO_LIBRARY" ]; then
37286
344468462338 removed obsolete usedir -p 1 option;
wenzelm
parents: 34238
diff changeset
    87
  perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -i true -d pdf -V outline=/proof,/ML":;' \
13001
40ba2eee948e clarified -l option;
wenzelm
parents: 12985
diff changeset
    88
    etc/settings
40ba2eee948e clarified -l option;
wenzelm
parents: 12985
diff changeset
    89
fi
11576
c418146c4763 activate default ISABELLE_USEDIR_OPTIONS for precompiled distribution;
wenzelm
parents: 10307
diff changeset
    90
28504
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 27588
diff changeset
    91
ISABELLE_HOME_USER=$(./bin/isabelle getenv -b ISABELLE_HOME_USER)
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    92
28504
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 27588
diff changeset
    93
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
    94
PLATFORM=$(./bin/isabelle getenv -b ML_PLATFORM)
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    95
37340
f3492868bbfd removed obsolete dry-run option;
wenzelm
parents: 37286
diff changeset
    96
if [ -n "$DO_LIBRARY" ]; then
45126
fc3bb3a42369 include no-smlnj targets into library (cf. e54a985daa61);
wenzelm
parents: 44877
diff changeset
    97
  ./build -bait -m all
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    98
else
41556
f55d564e0521 bundle main HOL image only, to save about 300 MB disk space;
wenzelm
parents: 40779
diff changeset
    99
  ./build -b HOL
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   100
fi
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   101
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   102
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   103
# prepare result
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   104
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   105
cd "$TMP"
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   106
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   107
chmod -R g=o "$TMP"
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   108
chgrp -R isabelle "$TMP"
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   109
13001
40ba2eee948e clarified -l option;
wenzelm
parents: 12985
diff changeset
   110
if [ -n "$DO_LIBRARY" ]; then
37340
f3492868bbfd removed obsolete dry-run option;
wenzelm
parents: 37286
diff changeset
   111
  tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_library.tar.gz" "$ISABELLE_NAME/browser_info"
13001
40ba2eee948e clarified -l option;
wenzelm
parents: 12985
diff changeset
   112
else
37340
f3492868bbfd removed obsolete dry-run option;
wenzelm
parents: 37286
diff changeset
   113
  tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_heaps_${PLATFORM}.tar.gz" "$ISABELLE_NAME/heaps"
13001
40ba2eee948e clarified -l option;
wenzelm
parents: 12985
diff changeset
   114
fi
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   115
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   116
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   117
# clean up
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   118
rm -rf "$TMP"