wneuper/isa: Admin/makebin@f3492868bbfd

     1 #!/usr/bin/env bash

2 #

     3 # makebin -- make Isabelle logic images for current platform

     6 ## global settings

     8 TMP="/var/tmp/isabelle-makebin$$"

    10 export THIS_IS_ISABELLE_MAKEBIN=true

    13 ## diagnostics

    15 PRG=$(basename "$0")

    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 }

    30 function fail()

    31 {

    32   echo "$1" >&2

    33   exit 2

    34 }

    37 ## process command line

    39 # options

    41 DO_LIBRARY=""

    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

    55 shift $(($OPTIND - 1))

    58 # args

    60 [ "$#" -gt 1 ] && usage

    62 ARCHIVE="$1"; shift

    65 ## main

    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"

    72 ISABELLE_NAME="$(basename "$ARCHIVE_BASE" .tar.gz)"

    73 ISABELLE_HOME="$TMP/$ISABELLE_NAME"

    76 # build logics

    78 mkdir "$TMP" || fail "Cannot create directory $TMP"

    80 cd "$TMP"

    81 tar xzf "$ARCHIVE_FULL"

    82 cd "$ISABELLE_NAME"

    84 perl -pi \

    85   -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1":;' \

    86   etc/settings

    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

    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

    97 COMPILER=$(./bin/isabelle getenv -b ML_IDENTIFIER)

    98 PLATFORM=$(./bin/isabelle getenv -b ML_PLATFORM)

   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

   109 # prepare result

   111 cd "$TMP"

   113 chmod -R g=o "$TMP"

   114 chgrp -R isabelle "$TMP"

   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

   123 # clean up

   124 cd /tmp

   125 rm -rf "$TMP"

author	wenzelm
	Sun, 06 Jun 2010 18:29:10 +0200
changeset 37340	f3492868bbfd
parent 37286	344468462338
child 41027	24851517ef15
permissions	-rwxr-xr-x