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