wenzelm@12721: #!/usr/bin/env bash wenzelm@10082: # wenzelm@30862: # makebin -- make Isabelle logic images for current platform wenzelm@10082: wenzelm@10082: wenzelm@10082: ## global settings wenzelm@10082: wenzelm@12427: TMP="/var/tmp/isabelle-makebin$$" wenzelm@10082: wenzelm@27030: export THIS_IS_ISABELLE_MAKEBIN=true wenzelm@27030: 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@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: 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@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@30862: ARCHIVE_BASE="$(basename "$ARCHIVE")" wenzelm@30862: ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")" wenzelm@10082: ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE" wenzelm@10082: wenzelm@30862: 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@30862: tar xzf "$ARCHIVE_FULL" wenzelm@10082: cd "$ISABELLE_NAME" wenzelm@10082: wenzelm@17575: perl -pi \ wenzelm@37286: -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1":;' \ wenzelm@17575: etc/settings wenzelm@17575: wenzelm@13001: if [ -n "$DO_LIBRARY" ]; then wenzelm@37286: perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -i true -d pdf -V outline=/proof,/ML":;' \ wenzelm@13001: etc/settings wenzelm@13001: fi wenzelm@11576: wenzelm@28504: ISABELLE_HOME_USER=$(./bin/isabelle 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@28504: COMPILER=$(./bin/isabelle getenv -b ML_IDENTIFIER) wenzelm@28504: PLATFORM=$(./bin/isabelle getenv -b ML_PLATFORM) wenzelm@10082: wenzelm@37340: if [ -n "$DO_LIBRARY" ]; then wenzelm@13001: ./build -bait wenzelm@10082: else wenzelm@27587: ./build -b -m HOL-Nominal HOL wenzelm@33918: ./build -b HOLCF wenzelm@10082: ./build -b ZF 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@37340: tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_library.tar.gz" "$ISABELLE_NAME/browser_info" wenzelm@13001: else wenzelm@37340: tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_heaps_${PLATFORM}.tar.gz" "$ISABELLE_NAME/heaps" wenzelm@13001: fi wenzelm@10082: wenzelm@10082: wenzelm@10082: # clean up wenzelm@10082: cd /tmp wenzelm@10082: rm -rf "$TMP"