Admin/makebin
author wenzelm
Wed Mar 19 22:28:17 2008 +0100 (2008-03-19 ago)
changeset 26338 f8ed02f22433
parent 26209 79c8d7277f33
child 27030 8c558af86e21
permissions -rwxr-xr-x
auxiliary dynamic_thm(s) for fact lookup;
renamed local dynamic_thm(s) to goal_thm(s);
     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 
    16 ## diagnostics
    17 
    18 PRG=$(basename "$0")
    19 
    20 function usage()
    21 {
    22   echo
    23   echo "Usage: $PRG [OPTIONS] ARCHIVE"
    24   echo
    25   echo "  Options are:"
    26   echo "    -l           produce library"
    27   echo "    -n           dry run"
    28   echo
    29   echo "  Precompile Isabelle for the current platform."
    30   echo
    31   exit 1
    32 }
    33 
    34 function fail()
    35 {
    36   echo "$1" >&2
    37   exit 2
    38 }
    39 
    40 
    41 ## process command line
    42 
    43 # options
    44 
    45 DO_LIBRARY=""
    46 DRY_RUN=""
    47 
    48 while getopts "ln" OPT
    49 do
    50   case "$OPT" in
    51     l)
    52       DO_LIBRARY=true
    53       ;;
    54     n)
    55       DRY_RUN=true
    56       ;;
    57     \?)
    58       usage
    59       ;;
    60   esac
    61 done
    62 
    63 shift $(($OPTIND - 1))
    64 
    65 
    66 # args
    67 
    68 [ "$#" -gt 1 ] && usage
    69 
    70 ARCHIVE="$1"; shift
    71 
    72 
    73 ## main
    74 
    75 [ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
    76 ARCHIVE_BASE=$(basename "$ARCHIVE")
    77 ARCHIVE_DIR=$(cd $(dirname "$ARCHIVE"); echo "$PWD")
    78 ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE"
    79 
    80 ISABELLE_NAME=$(basename "$ARCHIVE_BASE" .tar.gz)
    81 ISABELLE_HOME="$TMP/$ISABELLE_NAME"
    82 
    83 
    84 # build logics
    85 
    86 mkdir "$TMP" || fail "Cannot create directory $TMP"
    87 
    88 cd "$TMP"
    89 "$TAR" xzf "$ARCHIVE_FULL"
    90 cd "$ISABELLE_NAME"
    91 
    92 perl -pi \
    93   -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-p 1":;' \
    94   -e 's:^HOL_USEDIR_OPTIONS=.*$:HOL_USEDIR_OPTIONS="-p 2":;' \
    95   etc/settings
    96 
    97 if [ -n "$DO_LIBRARY" ]; then
    98   perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-p 1 -i true -d pdf -V outline=/proof,/ML":;' \
    99     etc/settings
   100 fi
   101 
   102 ISABELLE_HOME_USER=$(./bin/isatool getenv -b ISABELLE_HOME_USER)
   103 [ -f "$ISABELLE_HOME_USER/etc/settings" ] && \
   104   echo "### WARNING!  Personal Isabelle settings present. " >&2
   105 
   106 COMPILER=$(./bin/isatool getenv -b ML_IDENTIFIER)
   107 PLATFORM=$(./bin/isatool getenv -b ML_PLATFORM)
   108 
   109 if [ -n "$DRY_RUN" ]; then
   110   mkdir -p "heaps/$COMPILER/log"
   111   touch "heaps/$COMPILER/HOL"
   112   touch "heaps/$COMPILER/log/HOL.gz"
   113   touch "heaps/$COMPILER/HOL-Complex"
   114   touch "heaps/$COMPILER/log/HOL-Complex.gz"
   115   touch "heaps/$COMPILER/ZF"
   116   touch "heaps/$COMPILER/log/ZF.gz"
   117   mkdir browser_info
   118 elif [ -n "$DO_LIBRARY" ]; then
   119   ./build -bait
   120 else
   121   ./build -b -m HOL-Complex HOL
   122   ./build -b ZF
   123   rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL"
   124 fi
   125 
   126 
   127 # prepare result
   128 
   129 cd "$TMP"
   130 
   131 chmod -R g=o "$TMP"
   132 chgrp -R isabelle "$TMP"
   133 
   134 if [ -n "$DO_LIBRARY" ]; then
   135   "$TAR" cf "${ISABELLE_NAME}_library.tar" $ISABELLE_NAME/browser_info && \
   136     gzip -f "${ISABELLE_NAME}_library.tar"
   137     cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR"
   138 else
   139   for IMG in HOL HOL-Complex ZF
   140   do
   141     "$TAR" cf "${IMG}_$PLATFORM.tar" \
   142       "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \
   143       "$ISABELLE_NAME/heaps/$COMPILER/log/$IMG.gz"
   144     gzip -f "${IMG}_$PLATFORM.tar"
   145     cp -f "${IMG}_$PLATFORM.tar.gz" "$ARCHIVE_DIR"
   146   done
   147 fi
   148 
   149 
   150 # clean up
   151 cd /tmp
   152 rm -rf "$TMP"