Admin/makebin
author wenzelm
Thu Nov 26 15:28:42 2009 +0100 (2009-11-26)
changeset 33905 5760ba045bf0
parent 30862 dfd77f471c22
child 33918 5945e023bab7
permissions -rwxr-xr-x
additional menu entries;
     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   -e 's:^HOL_USEDIR_OPTIONS=.*$:HOL_USEDIR_OPTIONS="-M 1 -p 2":;' \
    92   etc/settings
    93 
    94 if [ -n "$DO_LIBRARY" ]; then
    95   perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -p 1 -i true -d pdf -V outline=/proof,/ML":;' \
    96     etc/settings
    97 fi
    98 
    99 ISABELLE_HOME_USER=$(./bin/isabelle getenv -b ISABELLE_HOME_USER)
   100 [ -f "$ISABELLE_HOME_USER/etc/settings" ] && \
   101   echo "### WARNING!  Personal Isabelle settings present. " >&2
   102 
   103 COMPILER=$(./bin/isabelle getenv -b ML_IDENTIFIER)
   104 PLATFORM=$(./bin/isabelle getenv -b ML_PLATFORM)
   105 
   106 if [ -n "$DRY_RUN" ]; then
   107   mkdir -p "heaps/$COMPILER/log"
   108   touch "heaps/$COMPILER/HOL"
   109   touch "heaps/$COMPILER/log/HOL.gz"
   110   touch "heaps/$COMPILER/HOL-Nominal"
   111   touch "heaps/$COMPILER/log/HOL-Nominal.gz"
   112   touch "heaps/$COMPILER/ZF"
   113   touch "heaps/$COMPILER/log/ZF.gz"
   114   mkdir browser_info
   115 elif [ -n "$DO_LIBRARY" ]; then
   116   ./build -bait
   117 else
   118   ./build -b -m HOL-Nominal HOL
   119   ./build -b ZF
   120   rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL"
   121 fi
   122 
   123 
   124 # prepare result
   125 
   126 cd "$TMP"
   127 
   128 chmod -R g=o "$TMP"
   129 chgrp -R isabelle "$TMP"
   130 
   131 if [ -n "$DO_LIBRARY" ]; then
   132   tar cf "${ISABELLE_NAME}_library.tar" $ISABELLE_NAME/browser_info && \
   133     gzip -f "${ISABELLE_NAME}_library.tar"
   134     cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR"
   135 else
   136   for IMG in HOL HOL-Nominal ZF
   137   do
   138     tar cf "${IMG}_$PLATFORM.tar" \
   139       "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \
   140       "$ISABELLE_NAME/heaps/$COMPILER/log/$IMG.gz"
   141     gzip -f "${IMG}_$PLATFORM.tar"
   142     cp -f "${IMG}_$PLATFORM.tar.gz" "$ARCHIVE_DIR"
   143   done
   144 fi
   145 
   146 
   147 # clean up
   148 cd /tmp
   149 rm -rf "$TMP"