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