3 # makebin -- make Isabelle logic images for current platform
8 TMP="/var/tmp/isabelle-makebin$$"
18 echo "Usage: $PRG [OPTIONS] ARCHIVE"
21 echo " -l produce library"
23 echo " Precompile Isabelle for the current platform."
35 ## process command line
53 shift $(($OPTIND - 1))
58 [ "$#" -gt 1 ] && usage
65 [ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
66 ARCHIVE_BASE="$(basename "$ARCHIVE")"
67 ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")"
68 ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE"
70 ISABELLE_NAME="$(basename "$ARCHIVE_BASE" .tar.gz)"
71 ISABELLE_HOME="$TMP/$ISABELLE_NAME"
76 mkdir "$TMP" || fail "Cannot create directory $TMP"
79 tar xzf "$ARCHIVE_FULL"
83 -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1":;' \
86 if [ -n "$DO_LIBRARY" ]; then
87 perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -i true -d pdf -V outline=/proof,/ML":;' \
91 ISABELLE_HOME_USER=$(./bin/isabelle getenv -b ISABELLE_HOME_USER)
93 COMPILER=$(./bin/isabelle getenv -b ML_IDENTIFIER)
94 PLATFORM=$(./bin/isabelle getenv -b ML_PLATFORM)
96 if [ -n "$DO_LIBRARY" ]; then
108 chgrp -R isabelle "$TMP"
110 if [ -n "$DO_LIBRARY" ]; then
111 tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_library.tar.gz" "$ISABELLE_NAME/browser_info"
113 tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_heaps_${PLATFORM}.tar.gz" "$ISABELLE_NAME/heaps"