Admin/makebin
author wenzelm
Wed Sep 27 19:51:11 2000 +0200 (2000-09-27)
changeset 10097 1db5bd97f6a3
parent 10090 36d1218b58f4
child 10101 746263fbcbfd
permissions -rwxr-xr-x
THIS_IS_ISABELLE_BUILD;
wenzelm@10082
     1
#!/bin/bash
wenzelm@10082
     2
#
wenzelm@10082
     3
# $Id$
wenzelm@10082
     4
#
wenzelm@10082
     5
# makebin -- make Isabelle logic images for current platform.
wenzelm@10082
     6
wenzelm@10082
     7
wenzelm@10082
     8
## global settings
wenzelm@10082
     9
wenzelm@10090
    10
FAKE_BUILD=""
wenzelm@10082
    11
DISTBASE=~/tmp/isadist
wenzelm@10082
    12
TMP="/tmp/isabelle-makebin$$"
wenzelm@10082
    13
wenzelm@10082
    14
TAR=tar
wenzelm@10082
    15
type -path gtar >/dev/null && TAR=gtar
wenzelm@10082
    16
wenzelm@10097
    17
export THIS_IS_ISABELLE_BUILD=true
wenzelm@10097
    18
wenzelm@10082
    19
wenzelm@10082
    20
## diagnostics
wenzelm@10082
    21
wenzelm@10082
    22
PRG=$(basename "$0")
wenzelm@10082
    23
wenzelm@10082
    24
function usage()
wenzelm@10082
    25
{
wenzelm@10082
    26
  echo
wenzelm@10082
    27
  echo "Usage: $PRG ARCHIVE"
wenzelm@10082
    28
  echo
wenzelm@10082
    29
  echo "  Make Isabelle logic images for current platform."
wenzelm@10082
    30
  echo
wenzelm@10082
    31
  exit 1
wenzelm@10082
    32
}
wenzelm@10082
    33
wenzelm@10082
    34
function fail()
wenzelm@10082
    35
{
wenzelm@10082
    36
  echo "$1" >&2
wenzelm@10082
    37
  exit 2
wenzelm@10082
    38
}
wenzelm@10082
    39
wenzelm@10082
    40
wenzelm@10082
    41
## process command line
wenzelm@10082
    42
wenzelm@10082
    43
[ "$#" -gt 1 ] && usage
wenzelm@10082
    44
wenzelm@10082
    45
ARCHIVE="$1"; shift
wenzelm@10082
    46
wenzelm@10082
    47
wenzelm@10082
    48
## main
wenzelm@10082
    49
wenzelm@10082
    50
[ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
wenzelm@10082
    51
ARCHIVE_BASE=$(basename "$ARCHIVE")
wenzelm@10082
    52
ARCHIVE_DIR=$(cd $(dirname "$ARCHIVE"); echo "$PWD")
wenzelm@10082
    53
ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE"
wenzelm@10082
    54
wenzelm@10082
    55
ISABELLE_NAME=$(basename "$ARCHIVE_BASE" .tar.gz)
wenzelm@10082
    56
ISABELLE_HOME="$TMP/$ISABELLE_NAME"
wenzelm@10082
    57
wenzelm@10082
    58
wenzelm@10082
    59
# build logics
wenzelm@10082
    60
wenzelm@10082
    61
mkdir "$TMP" || fail "Cannot create directory $TMP"
wenzelm@10082
    62
wenzelm@10082
    63
cd "$TMP"
wenzelm@10087
    64
"$TAR" xzf "$ARCHIVE_FULL"
wenzelm@10082
    65
cd "$ISABELLE_NAME"
wenzelm@10082
    66
wenzelm@10082
    67
ISABELLE_HOME_USER=$(./bin/isatool getenv -b ISABELLE_HOME_USER)
wenzelm@10082
    68
[ -f "$ISABELLE_HOME_USER/etc/settings" ] && \
wenzelm@10082
    69
  echo "### WARNING!  Personal Isabelle settings present. " >&2
wenzelm@10082
    70
wenzelm@10082
    71
COMPILER=$(./bin/isatool getenv -b ML_IDENTIFIER)
wenzelm@10082
    72
PLATFORM=$(./bin/isatool getenv -b ML_PLATFORM)
wenzelm@10082
    73
wenzelm@10082
    74
if [ -n "$FAKE_BUILD" ]; then
wenzelm@10082
    75
  mkdir -p "heaps/$COMPILER"
wenzelm@10082
    76
  touch "heaps/$COMPILER/HOL"
wenzelm@10082
    77
  touch "heaps/$COMPILER/HOL-Real"
wenzelm@10082
    78
  touch "heaps/$COMPILER/ZF"
wenzelm@10082
    79
else
wenzelm@10082
    80
  ./build -b -m HOL-Real HOL
wenzelm@10082
    81
  ./build -b ZF
wenzelm@10082
    82
  rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL"
wenzelm@10082
    83
fi
wenzelm@10082
    84
wenzelm@10082
    85
wenzelm@10082
    86
# prepare result
wenzelm@10082
    87
wenzelm@10082
    88
cd "$TMP"
wenzelm@10082
    89
wenzelm@10082
    90
chmod -R g=o "$TMP"
wenzelm@10082
    91
chgrp -R isabelle "$TMP"
wenzelm@10082
    92
wenzelm@10082
    93
for IMG in HOL HOL-Real ZF
wenzelm@10082
    94
do
wenzelm@10082
    95
  "$TAR" cf "${IMG}_$PLATFORM.tar" "$ISABELLE_NAME/heaps/$COMPILER/$IMG"
wenzelm@10082
    96
  gzip "${IMG}_$PLATFORM.tar"
wenzelm@10087
    97
  cp -f "${IMG}_$PLATFORM.tar.gz" "$ARCHIVE_DIR"
wenzelm@10082
    98
done
wenzelm@10082
    99
wenzelm@10082
   100
wenzelm@10082
   101
# clean up
wenzelm@10082
   102
cd /tmp
wenzelm@10082
   103
rm -rf "$TMP"