Admin/makebin
author nipkow
Wed Aug 04 11:25:08 2004 +0200 (2004-08-04)
changeset 15106 e8cef6993701
parent 14633 8553a957cffa
child 15971 c0c4088edccf
permissions -rwxr-xr-x
aded comment
     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 export THIS_IS_ISABELLE_ADMIN=true
    18 
    19 
    20 ## diagnostics
    21 
    22 PRG=$(basename "$0")
    23 
    24 function usage()
    25 {
    26   echo
    27   echo "Usage: $PRG [OPTIONS] ARCHIVE"
    28   echo
    29   echo "  Options are:"
    30   echo "    -l           produce library"
    31   echo "    -n           dry run"
    32   echo
    33   echo "  Precompile Isabelle for the current platform."
    34   echo
    35   exit 1
    36 }
    37 
    38 function fail()
    39 {
    40   echo "$1" >&2
    41   exit 2
    42 }
    43 
    44 
    45 ## process command line
    46 
    47 # options
    48 
    49 DO_LIBRARY=""
    50 DRY_RUN=""
    51 
    52 while getopts "ln" OPT
    53 do
    54   case "$OPT" in
    55     l)
    56       DO_LIBRARY=true
    57       ;;
    58     n)
    59       DRY_RUN=true
    60       ;;
    61     \?)
    62       usage
    63       ;;
    64   esac
    65 done
    66 
    67 shift $(($OPTIND - 1))
    68 
    69 
    70 # args
    71 
    72 [ "$#" -gt 1 ] && usage
    73 
    74 ARCHIVE="$1"; shift
    75 
    76 
    77 ## main
    78 
    79 [ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
    80 ARCHIVE_BASE=$(basename "$ARCHIVE")
    81 ARCHIVE_DIR=$(cd $(dirname "$ARCHIVE"); echo "$PWD")
    82 ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE"
    83 
    84 ISABELLE_NAME=$(basename "$ARCHIVE_BASE" .tar.gz)
    85 ISABELLE_HOME="$TMP/$ISABELLE_NAME"
    86 
    87 
    88 # build logics
    89 
    90 mkdir "$TMP" || fail "Cannot create directory $TMP"
    91 
    92 cd "$TMP"
    93 "$TAR" xzf "$ARCHIVE_FULL"
    94 cd "$ISABELLE_NAME"
    95 
    96 # FIXME: ugly hack to get proper HOL4 image
    97 # needs HOL4 proof terms installed in ~/isabelle/proofs
    98 # desperately needs fix for next release!
    99 cat > src/HOL/Import/HOL/ROOT.ML <<EOF
   100 with_path ".." use_thy "HOL4Compat";
   101 with_path ".." use_thy "HOL4Syntax";
   102 use_thy "HOL4Prob";
   103 use_thy "HOL4";
   104 EOF
   105 
   106 if [ -n "$DO_LIBRARY" ]; then
   107   perl -pi -e 's/^ISABELLE_USEDIR_OPTIONS=.*$/ISABELLE_USEDIR_OPTIONS="-i true -d pdf"/' \
   108     etc/settings
   109 else
   110   perl -pi -e 's/^ISABELLE_USEDIR_OPTIONS=.*$/ISABELLE_USEDIR_OPTIONS="-p 2"/' \
   111     etc/settings
   112 fi
   113 
   114 ISABELLE_HOME_USER=$(./bin/isatool getenv -b ISABELLE_HOME_USER)
   115 [ -f "$ISABELLE_HOME_USER/etc/settings" ] && \
   116   echo "### WARNING!  Personal Isabelle settings present. " >&2
   117 
   118 COMPILER=$(./bin/isatool getenv -b ML_IDENTIFIER)
   119 PLATFORM=$(./bin/isatool getenv -b ML_PLATFORM)
   120 
   121 if [ -n "$DRY_RUN" ]; then
   122   mkdir -p "heaps/$COMPILER/log"
   123   touch "heaps/$COMPILER/HOL"
   124   touch "heaps/$COMPILER/log/HOL.gz"
   125   touch "heaps/$COMPILER/HOL-Complex"
   126   touch "heaps/$COMPILER/log/HOL-Complex.gz"
   127   touch "heaps/$COMPILER/HOL4"
   128   touch "heaps/$COMPILER/log/HOL4.gz"
   129   touch "heaps/$COMPILER/ZF"
   130   touch "heaps/$COMPILER/log/ZF.gz"
   131   mkdir browser_info
   132 elif [ -n "$DO_LIBRARY" ]; then
   133   ./build -bait
   134 else
   135   ./build -b -m HOL-Complex HOL
   136   ./build -b ZF
   137   perl -pi -e 's/^ISABELLE_USEDIR_OPTIONS=.*$/ISABELLE_USEDIR_OPTIONS="-p 1"/' \
   138     etc/settings
   139   ./build -b -m HOL4 HOL
   140   rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL"
   141 fi
   142 
   143 
   144 # prepare result
   145 
   146 cd "$TMP"
   147 
   148 chmod -R g=o "$TMP"
   149 chgrp -R isabelle "$TMP"
   150 
   151 if [ -n "$DO_LIBRARY" ]; then
   152   "$TAR" cf "${ISABELLE_NAME}_library.tar" $ISABELLE_NAME/browser_info && \
   153     gzip -f "${ISABELLE_NAME}_library.tar"
   154     cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR"
   155 else
   156   for IMG in HOL HOL-Complex HOL4 ZF
   157   do
   158     "$TAR" cf "${IMG}_$PLATFORM.tar" \
   159       "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \
   160       "$ISABELLE_NAME/heaps/$COMPILER/log/$IMG.gz"
   161     gzip -f "${IMG}_$PLATFORM.tar"
   162     cp -f "${IMG}_$PLATFORM.tar.gz" "$ARCHIVE_DIR"
   163   done
   164 fi
   165 
   166 
   167 # clean up
   168 cd /tmp
   169 rm -rf "$TMP"