wenzelm@12721: #!/usr/bin/env bash
wenzelm@10082: #
wenzelm@10082: # $Id$
wenzelm@10082: #
wenzelm@10082: # makebin -- make Isabelle logic images for current platform.
wenzelm@10082: 
wenzelm@10082: 
wenzelm@10082: ## global settings
wenzelm@10082: 
wenzelm@10082: DISTBASE=~/tmp/isadist
wenzelm@12427: TMP="/var/tmp/isabelle-makebin$$"
wenzelm@10082: 
wenzelm@10082: TAR=tar
wenzelm@10082: type -path gtar >/dev/null && TAR=gtar
wenzelm@10082: 
wenzelm@10097: export THIS_IS_ISABELLE_BUILD=true
wenzelm@10097: 
wenzelm@10082: 
wenzelm@10082: ## diagnostics
wenzelm@10082: 
wenzelm@10082: PRG=$(basename "$0")
wenzelm@10082: 
wenzelm@10082: function usage()
wenzelm@10082: {
wenzelm@10082:   echo
wenzelm@12827:   echo "Usage: $PRG [OPTIONS] ARCHIVE"
wenzelm@10082:   echo
wenzelm@12827:   echo "  Options are:"
wenzelm@12827:   echo "    -l           include library"
wenzelm@12827:   echo "    -t           test run -- no build phase"
wenzelm@12827:   echo
wenzelm@12827:   echo "  Precompile Isabelle for the current platform."
wenzelm@10082:   echo
wenzelm@10082:   exit 1
wenzelm@10082: }
wenzelm@10082: 
wenzelm@10082: function fail()
wenzelm@10082: {
wenzelm@10082:   echo "$1" >&2
wenzelm@10082:   exit 2
wenzelm@10082: }
wenzelm@10082: 
wenzelm@10082: 
wenzelm@10082: ## process command line
wenzelm@10082: 
wenzelm@12827: # options
wenzelm@12827: 
wenzelm@12827: DO_LIBRARY=""
wenzelm@12827: TEST_RUN=""
wenzelm@12827: 
wenzelm@12827: while getopts "lt" OPT
wenzelm@12827: do
wenzelm@12827:   case "$OPT" in
wenzelm@12827:     l)
wenzelm@12827:       DO_LIBRARY=true
wenzelm@12827:       ;;
wenzelm@12827:     t)
wenzelm@12827:       TEST_RUN=true
wenzelm@12827:       ;;
wenzelm@12827:     \?)
wenzelm@12827:       usage
wenzelm@12827:       ;;
wenzelm@12827:   esac
wenzelm@12827: done
wenzelm@12827: 
wenzelm@12827: shift $(($OPTIND - 1))
wenzelm@12827: 
wenzelm@12827: 
wenzelm@12827: # args
wenzelm@12827: 
wenzelm@10082: [ "$#" -gt 1 ] && usage
wenzelm@10082: 
wenzelm@10082: ARCHIVE="$1"; shift
wenzelm@10082: 
wenzelm@10082: 
wenzelm@10082: ## main
wenzelm@10082: 
wenzelm@10082: [ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
wenzelm@10082: ARCHIVE_BASE=$(basename "$ARCHIVE")
wenzelm@10082: ARCHIVE_DIR=$(cd $(dirname "$ARCHIVE"); echo "$PWD")
wenzelm@10082: ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE"
wenzelm@10082: 
wenzelm@10082: ISABELLE_NAME=$(basename "$ARCHIVE_BASE" .tar.gz)
wenzelm@10082: ISABELLE_HOME="$TMP/$ISABELLE_NAME"
wenzelm@10082: 
wenzelm@10082: 
wenzelm@10082: # build logics
wenzelm@10082: 
wenzelm@10082: mkdir "$TMP" || fail "Cannot create directory $TMP"
wenzelm@10082: 
wenzelm@10082: cd "$TMP"
wenzelm@10087: "$TAR" xzf "$ARCHIVE_FULL"
wenzelm@10082: cd "$ISABELLE_NAME"
wenzelm@10082: 
wenzelm@11576: #activate default for precompiled distribution ...
wenzelm@11576: perl -pi -e 's/#ISABELLE_USEDIR_OPTIONS/ISABELLE_USEDIR_OPTIONS/' etc/settings
wenzelm@11576: 
wenzelm@10082: ISABELLE_HOME_USER=$(./bin/isatool getenv -b ISABELLE_HOME_USER)
wenzelm@10082: [ -f "$ISABELLE_HOME_USER/etc/settings" ] && \
wenzelm@10082:   echo "### WARNING!  Personal Isabelle settings present. " >&2
wenzelm@10082: 
wenzelm@10082: COMPILER=$(./bin/isatool getenv -b ML_IDENTIFIER)
wenzelm@10082: PLATFORM=$(./bin/isatool getenv -b ML_PLATFORM)
wenzelm@10082: 
wenzelm@12827: if [ -n "$TEST_RUN" ]; then
wenzelm@12827:   mkdir -p "heaps/$COMPILER/log"
wenzelm@10082:   touch "heaps/$COMPILER/HOL"
wenzelm@12827:   touch "heaps/$COMPILER/log/HOL.gz"
wenzelm@10082:   touch "heaps/$COMPILER/HOL-Real"
wenzelm@12827:   touch "heaps/$COMPILER/log/HOL-Real.gz"
wenzelm@10082:   touch "heaps/$COMPILER/ZF"
wenzelm@12827:   touch "heaps/$COMPILER/log/ZF.gz"
wenzelm@12827:   mkdir browser_info
wenzelm@10082: else
wenzelm@10082:   ./build -b -m HOL-Real HOL
wenzelm@10082:   ./build -b ZF
wenzelm@12827:   [ -n "$DO_LIBRARY" ] && ./build -bait
wenzelm@10082:   rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL"
wenzelm@10082: fi
wenzelm@10082: 
wenzelm@10082: 
wenzelm@10082: # prepare result
wenzelm@10082: 
wenzelm@10082: cd "$TMP"
wenzelm@10082: 
wenzelm@10082: chmod -R g=o "$TMP"
wenzelm@10082: chgrp -R isabelle "$TMP"
wenzelm@10082: 
wenzelm@10082: for IMG in HOL HOL-Real ZF
wenzelm@10082: do
wenzelm@10113:   "$TAR" cf "${IMG}_$PLATFORM.tar" \
wenzelm@10113:     "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \
wenzelm@10113:     "$ISABELLE_NAME/heaps/$COMPILER/log/$IMG.gz"
wenzelm@12827:   gzip -f "${IMG}_$PLATFORM.tar"
wenzelm@10087:   cp -f "${IMG}_$PLATFORM.tar.gz" "$ARCHIVE_DIR"
wenzelm@12827: 
wenzelm@12827:   if [ -n "$DO_LIBRARY" ]; then
wenzelm@12827:     "$TAR" cf "${ISABELLE_NAME}_library.tar" $ISABELLE_NAME/browser_info && \
wenzelm@12827:       gzip -f "${ISABELLE_NAME}_library.tar"
wenzelm@12827:   fi
wenzelm@10082: done
wenzelm@10082: 
wenzelm@10082: 
wenzelm@10082: # clean up
wenzelm@10082: cd /tmp
wenzelm@10082: rm -rf "$TMP"