Admin/makebin
author wenzelm
Thu Jan 19 21:22:08 2006 +0100 (2006-01-19 ago)
changeset 18708 4b3dadb4fe33
parent 17660 94bbe14c088e
child 23137 ae4110f7f88f
permissions -rwxr-xr-x
setup: theory -> theory;
     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 TMP="/var/tmp/isabelle-makebin$$"
    11 
    12 TAR=tar
    13 type -path gtar >/dev/null && TAR=gtar
    14 
    15 export THIS_IS_ISABELLE_BUILD=true
    16 
    17 
    18 ## diagnostics
    19 
    20 PRG=$(basename "$0")
    21 
    22 function usage()
    23 {
    24   echo
    25   echo "Usage: $PRG [OPTIONS] ARCHIVE"
    26   echo
    27   echo "  Options are:"
    28   echo "    -l           produce library"
    29   echo "    -n           dry run"
    30   echo
    31   echo "  Precompile Isabelle for the current platform."
    32   echo
    33   exit 1
    34 }
    35 
    36 function fail()
    37 {
    38   echo "$1" >&2
    39   exit 2
    40 }
    41 
    42 
    43 ## process command line
    44 
    45 # options
    46 
    47 DO_LIBRARY=""
    48 DRY_RUN=""
    49 
    50 while getopts "ln" OPT
    51 do
    52   case "$OPT" in
    53     l)
    54       DO_LIBRARY=true
    55       ;;
    56     n)
    57       DRY_RUN=true
    58       ;;
    59     \?)
    60       usage
    61       ;;
    62   esac
    63 done
    64 
    65 shift $(($OPTIND - 1))
    66 
    67 
    68 # args
    69 
    70 [ "$#" -gt 1 ] && usage
    71 
    72 ARCHIVE="$1"; shift
    73 
    74 
    75 ## main
    76 
    77 [ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
    78 ARCHIVE_BASE=$(basename "$ARCHIVE")
    79 ARCHIVE_DIR=$(cd $(dirname "$ARCHIVE"); echo "$PWD")
    80 ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE"
    81 
    82 ISABELLE_NAME=$(basename "$ARCHIVE_BASE" .tar.gz)
    83 ISABELLE_HOME="$TMP/$ISABELLE_NAME"
    84 
    85 
    86 # build logics
    87 
    88 mkdir "$TMP" || fail "Cannot create directory $TMP"
    89 
    90 cd "$TMP"
    91 "$TAR" xzf "$ARCHIVE_FULL"
    92 cd "$ISABELLE_NAME"
    93 
    94 # FIXME: ugly hack to get proper HOL4 image
    95 # needs HOL4 proof terms installed in ~/isabelle/proofs
    96 # desperately needs fix for next release!
    97 cat > src/HOL/Import/HOL/ROOT.ML <<EOF
    98 with_path ".." use_thy "HOL4Compat";
    99 with_path ".." use_thy "HOL4Syntax";
   100 use_thy "HOL4Prob";
   101 use_thy "HOL4";
   102 EOF
   103 
   104 perl -pi \
   105   -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-p 1":;' \
   106   -e 's:^HOL_USEDIR_OPTIONS=.*$:HOL_USEDIR_OPTIONS="-p 2":;' \
   107   etc/settings
   108 
   109 if [ -n "$DO_LIBRARY" ]; then
   110   perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-p 1 -i true -d pdf -V outline=/proof,/ML":;' \
   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 -m HOL4 HOL
   137   ./build -b ZF
   138   rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL"
   139 fi
   140 
   141 
   142 # prepare result
   143 
   144 cd "$TMP"
   145 
   146 chmod -R g=o "$TMP"
   147 chgrp -R isabelle "$TMP"
   148 
   149 if [ -n "$DO_LIBRARY" ]; then
   150   "$TAR" cf "${ISABELLE_NAME}_library.tar" $ISABELLE_NAME/browser_info && \
   151     gzip -f "${ISABELLE_NAME}_library.tar"
   152     cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR"
   153 else
   154   for IMG in HOL HOL-Complex HOL4 ZF
   155   do
   156     "$TAR" cf "${IMG}_$PLATFORM.tar" \
   157       "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \
   158       "$ISABELLE_NAME/heaps/$COMPILER/log/$IMG.gz"
   159     gzip -f "${IMG}_$PLATFORM.tar"
   160     cp -f "${IMG}_$PLATFORM.tar.gz" "$ARCHIVE_DIR"
   161   done
   162 fi
   163 
   164 
   165 # clean up
   166 cd /tmp
   167 rm -rf "$TMP"