Admin/makebin
author Cezary Kaliszyk <kaliszyk@in.tum.de>
Fri Oct 15 21:46:45 2010 +0900 (2010-10-15)
changeset 39994 7bd8013b903f
parent 37340 f3492868bbfd
child 40779 24851517ef15
permissions -rwxr-xr-x
FSet: give names to respectfulness theorems, rename list_all2_refl to avoid clash
     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
    25   echo "  Precompile Isabelle for the current platform."
    26   echo
    27   exit 1
    28 }
    29 
    30 function fail()
    31 {
    32   echo "$1" >&2
    33   exit 2
    34 }
    35 
    36 
    37 ## process command line
    38 
    39 # options
    40 
    41 DO_LIBRARY=""
    42 
    43 while getopts "ln" OPT
    44 do
    45   case "$OPT" in
    46     l)
    47       DO_LIBRARY=true
    48       ;;
    49     \?)
    50       usage
    51       ;;
    52   esac
    53 done
    54 
    55 shift $(($OPTIND - 1))
    56 
    57 
    58 # args
    59 
    60 [ "$#" -gt 1 ] && usage
    61 
    62 ARCHIVE="$1"; shift
    63 
    64 
    65 ## main
    66 
    67 [ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
    68 ARCHIVE_BASE="$(basename "$ARCHIVE")"
    69 ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")"
    70 ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE"
    71 
    72 ISABELLE_NAME="$(basename "$ARCHIVE_BASE" .tar.gz)"
    73 ISABELLE_HOME="$TMP/$ISABELLE_NAME"
    74 
    75 
    76 # build logics
    77 
    78 mkdir "$TMP" || fail "Cannot create directory $TMP"
    79 
    80 cd "$TMP"
    81 tar xzf "$ARCHIVE_FULL"
    82 cd "$ISABELLE_NAME"
    83 
    84 perl -pi \
    85   -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1":;' \
    86   etc/settings
    87 
    88 if [ -n "$DO_LIBRARY" ]; then
    89   perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -i true -d pdf -V outline=/proof,/ML":;' \
    90     etc/settings
    91 fi
    92 
    93 ISABELLE_HOME_USER=$(./bin/isabelle getenv -b ISABELLE_HOME_USER)
    94 [ -f "$ISABELLE_HOME_USER/etc/settings" ] && \
    95   echo "### WARNING!  Personal Isabelle settings present. " >&2
    96 
    97 COMPILER=$(./bin/isabelle getenv -b ML_IDENTIFIER)
    98 PLATFORM=$(./bin/isabelle getenv -b ML_PLATFORM)
    99 
   100 if [ -n "$DO_LIBRARY" ]; then
   101   ./build -bait
   102 else
   103   ./build -b -m HOL-Nominal HOL
   104   ./build -b HOLCF
   105   ./build -b ZF
   106 fi
   107 
   108 
   109 # prepare result
   110 
   111 cd "$TMP"
   112 
   113 chmod -R g=o "$TMP"
   114 chgrp -R isabelle "$TMP"
   115 
   116 if [ -n "$DO_LIBRARY" ]; then
   117   tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_library.tar.gz" "$ISABELLE_NAME/browser_info"
   118 else
   119   tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_heaps_${PLATFORM}.tar.gz" "$ISABELLE_NAME/heaps"
   120 fi
   121 
   122 
   123 # clean up
   124 cd /tmp
   125 rm -rf "$TMP"