Admin/makebin
changeset 10082 7c2021b7c664
child 10087 4dc7edfb0b5f
equal deleted inserted replaced
10081:352412857003 10082:7c2021b7c664
       
     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"