Admin/makebin

clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
more uniform Generic_Target.theory_notes/locale_notes: apply facts to all target contexts;

+
−#!/usr/bin/env bash
+
−#
+
−# makebin -- make Isabelle logic images for current platform
+
−
+
−
+
−## global settings
+
−
+
−TMP="/var/tmp/isabelle-makebin$$"
+
−
+
−
+
−## diagnostics
+
−
+
−PRG=$(basename "$0")
+
−
+
−function usage()
+
−{
+
−  echo
+
−  echo "Usage: $PRG [OPTIONS] ARCHIVE"
+
−  echo
+
−  echo "  Options are:"
+
−  echo "    -l           produce library"
+
−  echo
+
−  echo "  Precompile Isabelle for the current platform."
+
−  echo
+
−  exit 1
+
−}
+
−
+
−function fail()
+
−{
+
−  echo "$1" >&2
+
−  exit 2
+
−}
+
−
+
−
+
−## process command line
+
−
+
−# options
+
−
+
−DO_LIBRARY=""
+
−
+
−while getopts "l" OPT
+
−do
+
−  case "$OPT" in
+
−    l)
+
−      DO_LIBRARY=true
+
−      ;;
+
−    \?)
+
−      usage
+
−      ;;
+
−  esac
+
−done
+
−
+
−shift $(($OPTIND - 1))
+
−
+
−
+
−# args
+
−
+
−[ "$#" -gt 1 ] && usage
+
−
+
−ARCHIVE="$1"; shift
+
−
+
−
+
−## main
+
−
+
−[ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
+
−ARCHIVE_BASE="$(basename "$ARCHIVE")"
+
−ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")"
+
−ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE"
+
−
+
−ISABELLE_NAME="$(basename "$ARCHIVE_BASE" .tar.gz)"
+
−ISABELLE_HOME="$TMP/$ISABELLE_NAME"
+
−
+
−
+
−# build logics
+
−
+
−mkdir "$TMP" || fail "Cannot create directory $TMP"
+
−
+
−cd "$TMP"
+
−tar xzf "$ARCHIVE_FULL"
+
−cd "$ISABELLE_NAME"
+
−
+
−perl -pi \
+
−  -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1":;' \
+
−  etc/settings
+
−
+
−if [ -n "$DO_LIBRARY" ]; then
+
−  perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -i true -d pdf -V outline=/proof,/ML":;' \
+
−    etc/settings
+
−fi
+
−
+
−ISABELLE_HOME_USER=$(./bin/isabelle getenv -b ISABELLE_HOME_USER)
+
−
+
−COMPILER=$(./bin/isabelle getenv -b ML_IDENTIFIER)
+
−PLATFORM=$(./bin/isabelle getenv -b ML_PLATFORM)
+
−
+
−if [ -n "$DO_LIBRARY" ]; then
+
−  ./build -bait -m all
+
−else
+
−  ./build -b HOL
+
−fi
+
−
+
−
+
−# prepare result
+
−
+
−cd "$TMP"
+
−
+
−chmod -R g=o "$TMP"
+
−chgrp -R isabelle "$TMP"
+
−
+
−if [ -n "$DO_LIBRARY" ]; then
+
−  tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_library.tar.gz" "$ISABELLE_NAME/browser_info"
+
−else
+
−  tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_heaps_${PLATFORM}.tar.gz" "$ISABELLE_NAME/heaps"
+
−fi
+
−
+
−
+
−# clean up
+
−rm -rf "$TMP"