--- a/Admin/makebin Mon Apr 19 14:04:41 2004 +0200
+++ b/Admin/makebin Tue Apr 20 04:09:19 2004 +0200
@@ -93,6 +93,16 @@
"$TAR" xzf "$ARCHIVE_FULL"
cd "$ISABELLE_NAME"
+# FIXME: ugly hack to get proper HOL4 image
+# needs HOL4 proof terms installed in ~/isabelle/proofs
+# desperately needs fix for next release!
+cat > src/HOL/Import/HOL/ROOT.ML <<EOF
+with_path ".." use_thy "HOL4Compat";
+with_path ".." use_thy "HOL4Syntax";
+use_thy "HOL4Prob";
+use_thy "HOL4";
+EOF
+
if [ -n "$DO_LIBRARY" ]; then
perl -pi -e 's/^ISABELLE_USEDIR_OPTIONS=.*$/ISABELLE_USEDIR_OPTIONS="-i true -d pdf"/' \
etc/settings
@@ -114,6 +124,8 @@
touch "heaps/$COMPILER/log/HOL.gz"
touch "heaps/$COMPILER/HOL-Complex"
touch "heaps/$COMPILER/log/HOL-Complex.gz"
+ touch "heaps/$COMPILER/HOL4"
+ touch "heaps/$COMPILER/log/HOL4.gz"
touch "heaps/$COMPILER/ZF"
touch "heaps/$COMPILER/log/ZF.gz"
mkdir browser_info
@@ -122,6 +134,9 @@
else
./build -b -m HOL-Complex HOL
./build -b ZF
+ perl -pi -e 's/^ISABELLE_USEDIR_OPTIONS=.*$/ISABELLE_USEDIR_OPTIONS="-p 1"/' \
+ etc/settings
+ ./build -b -m HOL4 HOL
rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL"
fi
@@ -138,7 +153,7 @@
gzip -f "${ISABELLE_NAME}_library.tar"
cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR"
else
- for IMG in HOL HOL-Complex ZF
+ for IMG in HOL HOL-Complex HOL4 ZF
do
"$TAR" cf "${IMG}_$PLATFORM.tar" \
"$ISABELLE_NAME/heaps/$COMPILER/$IMG" \