wneuper/isa: Admin/makebin@7d30534e545b

     1 #!/usr/bin/env bash

2 #

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

     6 ## global settings

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

    11 ## diagnostics

    13 PRG=$(basename "$0")

    15 function usage()

    16 {

    17   echo

    18   echo "Usage: $PRG [OPTIONS] ARCHIVE"

    19   echo

    20   echo "  Options are:"

    21   echo "    -l           produce library"

    22   echo

    23   echo "  Precompile Isabelle for the current platform."

    24   echo

    25   exit 1

    26 }

    28 function fail()

    29 {

    30   echo "$1" >&2

    31   exit 2

    32 }

    35 ## process command line

    37 # options

    39 DO_LIBRARY=""

    41 while getopts "l" OPT

    42 do

    43   case "$OPT" in

    44     l)

    45       DO_LIBRARY=true

    46       ;;

    47     \?)

    48       usage

    49       ;;

    50   esac

    51 done

    53 shift $(($OPTIND - 1))

    56 # args

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

    60 ARCHIVE="$1"; shift

    63 ## main

    65 [ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"

    66 ARCHIVE_BASE="$(basename "$ARCHIVE")"

    67 ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")"

    68 ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE"

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

    71 ISABELLE_HOME="$TMP/$ISABELLE_NAME"

    74 # build logics

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

    78 cd "$TMP"

    79 tar xzf "$ARCHIVE_FULL"

    80 cd "$ISABELLE_NAME"

    82 perl -pi \

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

    84   etc/settings

    86 if [ -n "$DO_LIBRARY" ]; then

    87   perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -i true -d pdf -V outline=/proof,/ML":;' \

    88     etc/settings

    89 fi

    91 ISABELLE_HOME_USER=$(./bin/isabelle getenv -b ISABELLE_HOME_USER)

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

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

    96 if [ -n "$DO_LIBRARY" ]; then

    97   ./build -bait -m all

    98 else

    99   ./build -b HOL

   100 fi

   103 # prepare result

   105 cd "$TMP"

   107 chmod -R g=o "$TMP"

   108 chgrp -R isabelle "$TMP"

   110 if [ -n "$DO_LIBRARY" ]; then

   111   tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_library.tar.gz" "$ISABELLE_NAME/browser_info"

   112 else

   113   tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_heaps_${PLATFORM}.tar.gz" "$ISABELLE_NAME/heaps"

   114 fi

   117 # clean up

   118 rm -rf "$TMP"

author	wenzelm
	Wed, 23 May 2012 11:53:17 +0200
changeset 48901	7d30534e545b
parent 45997	fc3bb3a42369
permissions	-rwxr-xr-x