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@13001:   echo "    -l           produce library"
wenzelm@13001:   echo "    -n           dry run"
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@13001: DRY_RUN=""
wenzelm@12827: 
wenzelm@13001: while getopts "ln" OPT
wenzelm@12827: do
wenzelm@12827:   case "$OPT" in
wenzelm@12827:     l)
wenzelm@12827:       DO_LIBRARY=true
wenzelm@12827:       ;;
wenzelm@13001:     n)
wenzelm@13001:       DRY_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: 
kleing@14633: # FIXME: ugly hack to get proper HOL4 image
kleing@14633: # needs HOL4 proof terms installed in ~/isabelle/proofs
kleing@14633: # desperately needs fix for next release!
kleing@14633: cat > src/HOL/Import/HOL/ROOT.ML <<EOF
kleing@14633: with_path ".." use_thy "HOL4Compat";
kleing@14633: with_path ".." use_thy "HOL4Syntax";
kleing@14633: use_thy "HOL4Prob";
kleing@14633: use_thy "HOL4";
kleing@14633: EOF
kleing@14633: 
wenzelm@17575: perl -pi \
wenzelm@17575:   -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-p 1":;' \
wenzelm@17575:   -e 's:^HOL_USEDIR_OPTIONS=.*$:HOL_USEDIR_OPTIONS="-p 2":;' \
wenzelm@17575:   etc/settings
wenzelm@17575: 
wenzelm@13001: if [ -n "$DO_LIBRARY" ]; then
wenzelm@17575:   perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-p 1 -i true -d pdf -V outline=/proof,/ML":;' \
wenzelm@13001:     etc/settings
wenzelm@13001: fi
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@13001: if [ -n "$DRY_RUN" ]; then
wenzelm@12827:   mkdir -p "heaps/$COMPILER/log"
wenzelm@10082:   touch "heaps/$COMPILER/HOL"
wenzelm@12827:   touch "heaps/$COMPILER/log/HOL.gz"
kleing@14024:   touch "heaps/$COMPILER/HOL-Complex"
kleing@14024:   touch "heaps/$COMPILER/log/HOL-Complex.gz"
kleing@14633:   touch "heaps/$COMPILER/HOL4"
kleing@14633:   touch "heaps/$COMPILER/log/HOL4.gz"
wenzelm@10082:   touch "heaps/$COMPILER/ZF"
wenzelm@12827:   touch "heaps/$COMPILER/log/ZF.gz"
wenzelm@12827:   mkdir browser_info
wenzelm@13001: elif [ -n "$DO_LIBRARY" ]; then
wenzelm@13001:   ./build -bait
wenzelm@10082: else
kleing@14024:   ./build -b -m HOL-Complex HOL
wenzelm@17575:   ./build -b -m HOL4 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@13001: if [ -n "$DO_LIBRARY" ]; then
wenzelm@13001:   "$TAR" cf "${ISABELLE_NAME}_library.tar" $ISABELLE_NAME/browser_info && \
wenzelm@13001:     gzip -f "${ISABELLE_NAME}_library.tar"
wenzelm@13001:     cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR"
wenzelm@13001: else
kleing@14633:   for IMG in HOL HOL-Complex HOL4 ZF
wenzelm@13001:   do
wenzelm@13001:     "$TAR" cf "${IMG}_$PLATFORM.tar" \
wenzelm@13001:       "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \
wenzelm@13001:       "$ISABELLE_NAME/heaps/$COMPILER/log/$IMG.gz"
wenzelm@13001:     gzip -f "${IMG}_$PLATFORM.tar"
wenzelm@13001:     cp -f "${IMG}_$PLATFORM.tar.gz" "$ARCHIVE_DIR"
wenzelm@13001:   done
wenzelm@13001: fi
wenzelm@10082: 
wenzelm@10082: 
wenzelm@10082: # clean up
wenzelm@10082: cd /tmp
wenzelm@10082: rm -rf "$TMP"