5 # makebin -- make Isabelle logic images for current platform.
10 TMP="/var/tmp/isabelle-makebin$$"
13 type -path gtar >/dev/null && TAR=gtar
15 export THIS_IS_ISABELLE_MAKEBIN=true
25 echo "Usage: $PRG [OPTIONS] ARCHIVE"
28 echo " -l produce library"
31 echo " Precompile Isabelle for the current platform."
43 ## process command line
50 while getopts "ln" OPT
65 shift $(($OPTIND - 1))
70 [ "$#" -gt 1 ] && usage
77 [ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
78 ARCHIVE_BASE=$(basename "$ARCHIVE")
79 ARCHIVE_DIR=$(cd $(dirname "$ARCHIVE"); echo "$PWD")
80 ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE"
82 ISABELLE_NAME=$(basename "$ARCHIVE_BASE" .tar.gz)
83 ISABELLE_HOME="$TMP/$ISABELLE_NAME"
88 mkdir "$TMP" || fail "Cannot create directory $TMP"
91 "$TAR" xzf "$ARCHIVE_FULL"
95 -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-p 1":;' \
96 -e 's:^HOL_USEDIR_OPTIONS=.*$:HOL_USEDIR_OPTIONS="-p 2":;' \
99 if [ -n "$DO_LIBRARY" ]; then
100 perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-p 1 -i true -d pdf -V outline=/proof,/ML":;' \
104 ISABELLE_HOME_USER=$(./bin/isatool getenv -b ISABELLE_HOME_USER)
105 [ -f "$ISABELLE_HOME_USER/etc/settings" ] && \
106 echo "### WARNING! Personal Isabelle settings present. " >&2
108 COMPILER=$(./bin/isatool getenv -b ML_IDENTIFIER)
109 PLATFORM=$(./bin/isatool getenv -b ML_PLATFORM)
111 if [ -n "$DRY_RUN" ]; then
112 mkdir -p "heaps/$COMPILER/log"
113 touch "heaps/$COMPILER/HOL"
114 touch "heaps/$COMPILER/log/HOL.gz"
115 touch "heaps/$COMPILER/HOL-Nominal"
116 touch "heaps/$COMPILER/log/HOL-Nominal.gz"
117 touch "heaps/$COMPILER/ZF"
118 touch "heaps/$COMPILER/log/ZF.gz"
120 elif [ -n "$DO_LIBRARY" ]; then
123 ./build -b -m HOL-Nominal HOL
125 rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL"
134 chgrp -R isabelle "$TMP"
136 if [ -n "$DO_LIBRARY" ]; then
137 "$TAR" cf "${ISABELLE_NAME}_library.tar" $ISABELLE_NAME/browser_info && \
138 gzip -f "${ISABELLE_NAME}_library.tar"
139 cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR"
141 for IMG in HOL HOL-Nominal ZF
143 "$TAR" cf "${IMG}_$PLATFORM.tar" \
144 "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \
145 "$ISABELLE_NAME/heaps/$COMPILER/log/$IMG.gz"
146 gzip -f "${IMG}_$PLATFORM.tar"
147 cp -f "${IMG}_$PLATFORM.tar.gz" "$ARCHIVE_DIR"