Admin/makebin
author wenzelm
Mon Jan 21 15:28:34 2002 +0100 (2002-01-21)
changeset 12827 05c13f5a515d
parent 12721 226fc0e2e7e3
child 12830 c037ff3e5ddf
permissions -rwxr-xr-x
options -l and -t;
tuned;
wenzelm@12721
     1
#!/usr/bin/env 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@10082
    10
DISTBASE=~/tmp/isadist
wenzelm@12427
    11
TMP="/var/tmp/isabelle-makebin$$"
wenzelm@10082
    12
wenzelm@10082
    13
TAR=tar
wenzelm@10082
    14
type -path gtar >/dev/null && TAR=gtar
wenzelm@10082
    15
wenzelm@10097
    16
export THIS_IS_ISABELLE_BUILD=true
wenzelm@10097
    17
wenzelm@10082
    18
wenzelm@10082
    19
## diagnostics
wenzelm@10082
    20
wenzelm@10082
    21
PRG=$(basename "$0")
wenzelm@10082
    22
wenzelm@10082
    23
function usage()
wenzelm@10082
    24
{
wenzelm@10082
    25
  echo
wenzelm@12827
    26
  echo "Usage: $PRG [OPTIONS] ARCHIVE"
wenzelm@10082
    27
  echo
wenzelm@12827
    28
  echo "  Options are:"
wenzelm@12827
    29
  echo "    -l           include library"
wenzelm@12827
    30
  echo "    -t           test run -- no build phase"
wenzelm@12827
    31
  echo
wenzelm@12827
    32
  echo "  Precompile Isabelle for the current platform."
wenzelm@10082
    33
  echo
wenzelm@10082
    34
  exit 1
wenzelm@10082
    35
}
wenzelm@10082
    36
wenzelm@10082
    37
function fail()
wenzelm@10082
    38
{
wenzelm@10082
    39
  echo "$1" >&2
wenzelm@10082
    40
  exit 2
wenzelm@10082
    41
}
wenzelm@10082
    42
wenzelm@10082
    43
wenzelm@10082
    44
## process command line
wenzelm@10082
    45
wenzelm@12827
    46
# options
wenzelm@12827
    47
wenzelm@12827
    48
DO_LIBRARY=""
wenzelm@12827
    49
TEST_RUN=""
wenzelm@12827
    50
wenzelm@12827
    51
while getopts "lt" OPT
wenzelm@12827
    52
do
wenzelm@12827
    53
  case "$OPT" in
wenzelm@12827
    54
    l)
wenzelm@12827
    55
      DO_LIBRARY=true
wenzelm@12827
    56
      ;;
wenzelm@12827
    57
    t)
wenzelm@12827
    58
      TEST_RUN=true
wenzelm@12827
    59
      ;;
wenzelm@12827
    60
    \?)
wenzelm@12827
    61
      usage
wenzelm@12827
    62
      ;;
wenzelm@12827
    63
  esac
wenzelm@12827
    64
done
wenzelm@12827
    65
wenzelm@12827
    66
shift $(($OPTIND - 1))
wenzelm@12827
    67
wenzelm@12827
    68
wenzelm@12827
    69
# args
wenzelm@12827
    70
wenzelm@10082
    71
[ "$#" -gt 1 ] && usage
wenzelm@10082
    72
wenzelm@10082
    73
ARCHIVE="$1"; shift
wenzelm@10082
    74
wenzelm@10082
    75
wenzelm@10082
    76
## main
wenzelm@10082
    77
wenzelm@10082
    78
[ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
wenzelm@10082
    79
ARCHIVE_BASE=$(basename "$ARCHIVE")
wenzelm@10082
    80
ARCHIVE_DIR=$(cd $(dirname "$ARCHIVE"); echo "$PWD")
wenzelm@10082
    81
ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE"
wenzelm@10082
    82
wenzelm@10082
    83
ISABELLE_NAME=$(basename "$ARCHIVE_BASE" .tar.gz)
wenzelm@10082
    84
ISABELLE_HOME="$TMP/$ISABELLE_NAME"
wenzelm@10082
    85
wenzelm@10082
    86
wenzelm@10082
    87
# build logics
wenzelm@10082
    88
wenzelm@10082
    89
mkdir "$TMP" || fail "Cannot create directory $TMP"
wenzelm@10082
    90
wenzelm@10082
    91
cd "$TMP"
wenzelm@10087
    92
"$TAR" xzf "$ARCHIVE_FULL"
wenzelm@10082
    93
cd "$ISABELLE_NAME"
wenzelm@10082
    94
wenzelm@11576
    95
#activate default for precompiled distribution ...
wenzelm@11576
    96
perl -pi -e 's/#ISABELLE_USEDIR_OPTIONS/ISABELLE_USEDIR_OPTIONS/' etc/settings
wenzelm@11576
    97
wenzelm@10082
    98
ISABELLE_HOME_USER=$(./bin/isatool getenv -b ISABELLE_HOME_USER)
wenzelm@10082
    99
[ -f "$ISABELLE_HOME_USER/etc/settings" ] && \
wenzelm@10082
   100
  echo "### WARNING!  Personal Isabelle settings present. " >&2
wenzelm@10082
   101
wenzelm@10082
   102
COMPILER=$(./bin/isatool getenv -b ML_IDENTIFIER)
wenzelm@10082
   103
PLATFORM=$(./bin/isatool getenv -b ML_PLATFORM)
wenzelm@10082
   104
wenzelm@12827
   105
if [ -n "$TEST_RUN" ]; then
wenzelm@12827
   106
  mkdir -p "heaps/$COMPILER/log"
wenzelm@10082
   107
  touch "heaps/$COMPILER/HOL"
wenzelm@12827
   108
  touch "heaps/$COMPILER/log/HOL.gz"
wenzelm@10082
   109
  touch "heaps/$COMPILER/HOL-Real"
wenzelm@12827
   110
  touch "heaps/$COMPILER/log/HOL-Real.gz"
wenzelm@10082
   111
  touch "heaps/$COMPILER/ZF"
wenzelm@12827
   112
  touch "heaps/$COMPILER/log/ZF.gz"
wenzelm@12827
   113
  mkdir browser_info
wenzelm@10082
   114
else
wenzelm@10082
   115
  ./build -b -m HOL-Real HOL
wenzelm@10082
   116
  ./build -b ZF
wenzelm@12827
   117
  [ -n "$DO_LIBRARY" ] && ./build -bait
wenzelm@10082
   118
  rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL"
wenzelm@10082
   119
fi
wenzelm@10082
   120
wenzelm@10082
   121
wenzelm@10082
   122
# prepare result
wenzelm@10082
   123
wenzelm@10082
   124
cd "$TMP"
wenzelm@10082
   125
wenzelm@10082
   126
chmod -R g=o "$TMP"
wenzelm@10082
   127
chgrp -R isabelle "$TMP"
wenzelm@10082
   128
wenzelm@10082
   129
for IMG in HOL HOL-Real ZF
wenzelm@10082
   130
do
wenzelm@10113
   131
  "$TAR" cf "${IMG}_$PLATFORM.tar" \
wenzelm@10113
   132
    "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \
wenzelm@10113
   133
    "$ISABELLE_NAME/heaps/$COMPILER/log/$IMG.gz"
wenzelm@12827
   134
  gzip -f "${IMG}_$PLATFORM.tar"
wenzelm@10087
   135
  cp -f "${IMG}_$PLATFORM.tar.gz" "$ARCHIVE_DIR"
wenzelm@12827
   136
wenzelm@12827
   137
  if [ -n "$DO_LIBRARY" ]; then
wenzelm@12827
   138
    "$TAR" cf "${ISABELLE_NAME}_library.tar" $ISABELLE_NAME/browser_info && \
wenzelm@12827
   139
      gzip -f "${ISABELLE_NAME}_library.tar"
wenzelm@12827
   140
  fi
wenzelm@10082
   141
done
wenzelm@10082
   142
wenzelm@10082
   143
wenzelm@10082
   144
# clean up
wenzelm@10082
   145
cd /tmp
wenzelm@10082
   146
rm -rf "$TMP"