Admin/makebin
author haftmann
Sun Jun 05 14:33:02 2005 +0200 (2005-06-05)
changeset 16275 951803bff5b1
parent 15971 c0c4088edccf
child 17571 5f83a635dce0
permissions -rwxr-xr-x
a more spohisticated symlink handling
     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           produce library"
    30   echo "    -n           dry run"
    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 DRY_RUN=""
    50 
    51 while getopts "ln" OPT
    52 do
    53   case "$OPT" in
    54     l)
    55       DO_LIBRARY=true
    56       ;;
    57     n)
    58       DRY_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 # FIXME: ugly hack to get proper HOL4 image
    96 # needs HOL4 proof terms installed in ~/isabelle/proofs
    97 # desperately needs fix for next release!
    98 cat > src/HOL/Import/HOL/ROOT.ML <<EOF
    99 with_path ".." use_thy "HOL4Compat";
   100 with_path ".." use_thy "HOL4Syntax";
   101 use_thy "HOL4Prob";
   102 use_thy "HOL4";
   103 EOF
   104 
   105 if [ -n "$DO_LIBRARY" ]; then
   106   perl -pi -e 's/^ISABELLE_USEDIR_OPTIONS=.*$/ISABELLE_USEDIR_OPTIONS="-i true -d pdf"/' \
   107     etc/settings
   108 else
   109   perl -pi -e 's/^ISABELLE_USEDIR_OPTIONS=.*$/ISABELLE_USEDIR_OPTIONS="-p 2"/' \
   110     etc/settings
   111 fi
   112 
   113 ISABELLE_HOME_USER=$(./bin/isatool getenv -b ISABELLE_HOME_USER)
   114 [ -f "$ISABELLE_HOME_USER/etc/settings" ] && \
   115   echo "### WARNING!  Personal Isabelle settings present. " >&2
   116 
   117 COMPILER=$(./bin/isatool getenv -b ML_IDENTIFIER)
   118 PLATFORM=$(./bin/isatool getenv -b ML_PLATFORM)
   119 
   120 if [ -n "$DRY_RUN" ]; then
   121   mkdir -p "heaps/$COMPILER/log"
   122   touch "heaps/$COMPILER/HOL"
   123   touch "heaps/$COMPILER/log/HOL.gz"
   124   touch "heaps/$COMPILER/HOL-Complex"
   125   touch "heaps/$COMPILER/log/HOL-Complex.gz"
   126   touch "heaps/$COMPILER/HOL4"
   127   touch "heaps/$COMPILER/log/HOL4.gz"
   128   touch "heaps/$COMPILER/ZF"
   129   touch "heaps/$COMPILER/log/ZF.gz"
   130   mkdir browser_info
   131 elif [ -n "$DO_LIBRARY" ]; then
   132   ./build -bait
   133 else
   134   ./build -b -m HOL-Complex HOL
   135   ./build -b ZF
   136   perl -pi -e 's/^ISABELLE_USEDIR_OPTIONS=.*$/ISABELLE_USEDIR_OPTIONS="-p 1"/' \
   137     etc/settings
   138   ./build -b -m HOL4 HOL
   139   rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL"
   140 fi
   141 
   142 
   143 # prepare result
   144 
   145 cd "$TMP"
   146 
   147 chmod -R g=o "$TMP"
   148 chgrp -R isabelle "$TMP"
   149 
   150 if [ -n "$DO_LIBRARY" ]; then
   151   "$TAR" cf "${ISABELLE_NAME}_library.tar" $ISABELLE_NAME/browser_info && \
   152     gzip -f "${ISABELLE_NAME}_library.tar"
   153     cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR"
   154 else
   155   for IMG in HOL HOL-Complex HOL4 ZF
   156   do
   157     "$TAR" cf "${IMG}_$PLATFORM.tar" \
   158       "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \
   159       "$ISABELLE_NAME/heaps/$COMPILER/log/$IMG.gz"
   160     gzip -f "${IMG}_$PLATFORM.tar"
   161     cp -f "${IMG}_$PLATFORM.tar.gz" "$ARCHIVE_DIR"
   162   done
   163 fi
   164 
   165 
   166 # clean up
   167 cd /tmp
   168 rm -rf "$TMP"