wenzelm@10082: #!/bin/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@10090: FAKE_BUILD=""
wenzelm@10082: DISTBASE=~/tmp/isadist
wenzelm@10082: TMP="/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@10082:   echo "Usage: $PRG ARCHIVE"
wenzelm@10082:   echo
wenzelm@10082:   echo "  Make Isabelle logic images for 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@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@10082: if [ -n "$FAKE_BUILD" ]; then
wenzelm@10082:   mkdir -p "heaps/$COMPILER"
wenzelm@10082:   touch "heaps/$COMPILER/HOL"
wenzelm@10082:   touch "heaps/$COMPILER/HOL-Real"
wenzelm@10082:   touch "heaps/$COMPILER/ZF"
wenzelm@10082: else
wenzelm@10082:   ./build -b -m HOL-Real HOL
wenzelm@10082:   ./build -b ZF
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@10082:   gzip "${IMG}_$PLATFORM.tar"
wenzelm@10087:   cp -f "${IMG}_$PLATFORM.tar.gz" "$ARCHIVE_DIR"
wenzelm@10082: done
wenzelm@10082: 
wenzelm@10082: 
wenzelm@10082: # clean up
wenzelm@10082: cd /tmp
wenzelm@10082: rm -rf "$TMP"