Admin/makebin
author nipkow
Tue, 22 Mar 2011 12:49:07 +0100
changeset 42059 83f3dc509068
parent 41556 f55d564e0521
child 44877 a4761fc03ee7
permissions -rwxr-xr-x
fixed a printing problem for bounded quantifiers and bounded set operators in the case of tuples
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"
12827
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    24
  echo
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    25
  echo "  Precompile Isabelle for the current platform."
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    26
  echo
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    27
  exit 1
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    28
}
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
function fail()
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    31
{
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    32
  echo "$1" >&2
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    33
  exit 2
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
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
## process command line
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    38
12827
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    39
# options
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    40
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    41
DO_LIBRARY=""
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    42
13001
40ba2eee948e clarified -l option;
wenzelm
parents: 12985
diff changeset
    43
while getopts "ln" OPT
12827
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    44
do
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    45
  case "$OPT" in
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    46
    l)
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    47
      DO_LIBRARY=true
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    48
      ;;
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    49
    \?)
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    50
      usage
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    51
      ;;
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    52
  esac
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    53
done
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    54
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    55
shift $(($OPTIND - 1))
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    56
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    57
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    58
# args
05c13f5a515d options -l and -t;
wenzelm
parents: 12721
diff changeset
    59
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    60
[ "$#" -gt 1 ] && usage
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
ARCHIVE="$1"; shift
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    63
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
## main
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
[ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
30862
dfd77f471c22 single-threaded build;
wenzelm
parents: 28504
diff changeset
    68
ARCHIVE_BASE="$(basename "$ARCHIVE")"
dfd77f471c22 single-threaded build;
wenzelm
parents: 28504
diff changeset
    69
ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")"
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    70
ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE"
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    71
30862
dfd77f471c22 single-threaded build;
wenzelm
parents: 28504
diff changeset
    72
ISABELLE_NAME="$(basename "$ARCHIVE_BASE" .tar.gz)"
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    73
ISABELLE_HOME="$TMP/$ISABELLE_NAME"
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    74
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
# build logics
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
mkdir "$TMP" || fail "Cannot create directory $TMP"
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
cd "$TMP"
30862
dfd77f471c22 single-threaded build;
wenzelm
parents: 28504
diff changeset
    81
tar xzf "$ARCHIVE_FULL"
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    82
cd "$ISABELLE_NAME"
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    83
17575
wenzelm
parents: 17573
diff changeset
    84
perl -pi \
37286
344468462338 removed obsolete usedir -p 1 option;
wenzelm
parents: 34238
diff changeset
    85
  -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1":;' \
17575
wenzelm
parents: 17573
diff changeset
    86
  etc/settings
wenzelm
parents: 17573
diff changeset
    87
13001
40ba2eee948e clarified -l option;
wenzelm
parents: 12985
diff changeset
    88
if [ -n "$DO_LIBRARY" ]; then
37286
344468462338 removed obsolete usedir -p 1 option;
wenzelm
parents: 34238
diff changeset
    89
  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
    90
    etc/settings
40ba2eee948e clarified -l option;
wenzelm
parents: 12985
diff changeset
    91
fi
11576
c418146c4763 activate default ISABELLE_USEDIR_OPTIONS for precompiled distribution;
wenzelm
parents: 10307
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
ISABELLE_HOME_USER=$(./bin/isabelle getenv -b ISABELLE_HOME_USER)
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    94
[ -f "$ISABELLE_HOME_USER/etc/settings" ] && \
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    95
  echo "### WARNING!  Personal Isabelle settings present. " >&2
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    96
28504
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 27588
diff changeset
    97
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
    98
PLATFORM=$(./bin/isabelle getenv -b ML_PLATFORM)
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    99
37340
f3492868bbfd removed obsolete dry-run option;
wenzelm
parents: 37286
diff changeset
   100
if [ -n "$DO_LIBRARY" ]; then
13001
40ba2eee948e clarified -l option;
wenzelm
parents: 12985
diff changeset
   101
  ./build -bait
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   102
else
41556
f55d564e0521 bundle main HOL image only, to save about 300 MB disk space;
wenzelm
parents: 40779
diff changeset
   103
  ./build -b HOL
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   104
fi
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   105
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
# prepare result
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   108
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   109
cd "$TMP"
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   110
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   111
chmod -R g=o "$TMP"
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   112
chgrp -R isabelle "$TMP"
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   113
13001
40ba2eee948e clarified -l option;
wenzelm
parents: 12985
diff changeset
   114
if [ -n "$DO_LIBRARY" ]; then
37340
f3492868bbfd removed obsolete dry-run option;
wenzelm
parents: 37286
diff changeset
   115
  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
   116
else
37340
f3492868bbfd removed obsolete dry-run option;
wenzelm
parents: 37286
diff changeset
   117
  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
   118
fi
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   119
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   120
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   121
# clean up
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   122
cd /tmp
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   123
rm -rf "$TMP"