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