Admin/makebin
author wenzelm
Fri, 10 Nov 2000 19:02:37 +0100
changeset 10432 3dfbc913d184
parent 10307 0df0bbd7e324
child 11576 c418146c4763
permissions -rwxr-xr-x
added axclass inverse and consts inverse, divide (infix "/"); moved axclass power to Nat.thy;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
     1
#!/bin/bash
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
     2
#
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
     3
# $Id$
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
# makebin -- make Isabelle logic images for current platform.
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
     6
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
     7
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
     8
## global settings
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
     9
10090
36d1218b58f4 FAKE_BUILD="";
wenzelm
parents: 10087
diff changeset
    10
FAKE_BUILD=""
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    11
DISTBASE=~/tmp/isadist
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    12
TMP="/tmp/isabelle-makebin$$"
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    13
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    14
TAR=tar
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    15
type -path gtar >/dev/null && TAR=gtar
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    16
10097
1db5bd97f6a3 THIS_IS_ISABELLE_BUILD;
wenzelm
parents: 10090
diff changeset
    17
export THIS_IS_ISABELLE_BUILD=true
1db5bd97f6a3 THIS_IS_ISABELLE_BUILD;
wenzelm
parents: 10090
diff changeset
    18
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    19
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    20
## diagnostics
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    21
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    22
PRG=$(basename "$0")
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    23
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    24
function usage()
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    25
{
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
  echo "Usage: $PRG ARCHIVE"
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    28
  echo
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    29
  echo "  Make Isabelle logic images for current platform."
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    30
  echo
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    31
  exit 1
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
function fail()
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
  echo "$1" >&2
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    37
  exit 2
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    38
}
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    39
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    40
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    41
## process command line
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    42
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    43
[ "$#" -gt 1 ] && usage
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    44
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    45
ARCHIVE="$1"; shift
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    46
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    47
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    48
## main
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    49
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    50
[ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    51
ARCHIVE_BASE=$(basename "$ARCHIVE")
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    52
ARCHIVE_DIR=$(cd $(dirname "$ARCHIVE"); echo "$PWD")
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    53
ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE"
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    54
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    55
ISABELLE_NAME=$(basename "$ARCHIVE_BASE" .tar.gz)
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    56
ISABELLE_HOME="$TMP/$ISABELLE_NAME"
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    57
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    58
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    59
# build logics
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    60
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    61
mkdir "$TMP" || fail "Cannot create directory $TMP"
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
cd "$TMP"
10087
wenzelm
parents: 10082
diff changeset
    64
"$TAR" xzf "$ARCHIVE_FULL"
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    65
cd "$ISABELLE_NAME"
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
ISABELLE_HOME_USER=$(./bin/isatool getenv -b ISABELLE_HOME_USER)
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    68
[ -f "$ISABELLE_HOME_USER/etc/settings" ] && \
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    69
  echo "### WARNING!  Personal Isabelle settings present. " >&2
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    70
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    71
COMPILER=$(./bin/isatool getenv -b ML_IDENTIFIER)
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    72
PLATFORM=$(./bin/isatool getenv -b ML_PLATFORM)
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
if [ -n "$FAKE_BUILD" ]; then
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    75
  mkdir -p "heaps/$COMPILER"
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    76
  touch "heaps/$COMPILER/HOL"
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    77
  touch "heaps/$COMPILER/HOL-Real"
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    78
  touch "heaps/$COMPILER/ZF"
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    79
else
10307
0df0bbd7e324 comment out Pure-copied target;
wenzelm
parents: 10113
diff changeset
    80
  #FIXME for Poly/ML 3.x only ...
0df0bbd7e324 comment out Pure-copied target;
wenzelm
parents: 10113
diff changeset
    81
  #./build -b -m Pure-copied Pure
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    82
  ./build -b -m HOL-Real HOL
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    83
  ./build -b ZF
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    84
  rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL"
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    85
fi
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    86
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    87
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    88
# prepare result
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    89
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    90
cd "$TMP"
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    91
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    92
chmod -R g=o "$TMP"
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    93
chgrp -R isabelle "$TMP"
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    94
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    95
for IMG in HOL HOL-Real ZF
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
    96
do
10113
a1f8d7d4084b include log files;
wenzelm
parents: 10101
diff changeset
    97
  "$TAR" cf "${IMG}_$PLATFORM.tar" \
a1f8d7d4084b include log files;
wenzelm
parents: 10101
diff changeset
    98
    "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \
a1f8d7d4084b include log files;
wenzelm
parents: 10101
diff changeset
    99
    "$ISABELLE_NAME/heaps/$COMPILER/log/$IMG.gz"
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   100
  gzip "${IMG}_$PLATFORM.tar"
10087
wenzelm
parents: 10082
diff changeset
   101
  cp -f "${IMG}_$PLATFORM.tar.gz" "$ARCHIVE_DIR"
10082
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   102
done
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   103
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
# clean up
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   106
cd /tmp
7c2021b7c664 make Isabelle logic images for current platform;
wenzelm
parents:
diff changeset
   107
rm -rf "$TMP"