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