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