# HG changeset patch
# User wenzelm
# Date 1358107199 -3600
# Node ID e932198be6195c12dc95b4d3b6f9f024a58fada6
# Parent  8f6046b7f8507d8eceed222791531c69bb80fe01
updated makedist_library;

diff -r 8f6046b7f850 -r e932198be619 Admin/Release/CHECKLIST
--- a/Admin/Release/CHECKLIST	Sun Jan 13 20:30:33 2013 +0100
+++ b/Admin/Release/CHECKLIST	Sun Jan 13 20:59:59 2013 +0100
@@ -53,16 +53,16 @@
 Packaging
 =========
 
-- hg up -r DISTNAME && isabelle makedist -r DISTNAME;
+- hg up -r DISTNAME && isabelle makedist -r DISTNAME
+
+- isabelle makedist_bundles
 
-- isabelle makedist_bundles;
+- ./makedist_library DISTNAME_linux.tar.gz
 
-- Mac OS X: hdiutil create -srcfolder DIR DMG;
+- Mac OS X: hdiutil create -srcfolder DIR DMG
 
 - Windows: cat 7zsd_All.sfx sfx.txt Isabelle.7z > Isabelle.exe
 
-- makebin -l on fast machine, based on renamed bundle with deleted heaps;
-
 
 Final release stage
 ===================
diff -r 8f6046b7f850 -r e932198be619 Admin/Release/makebin
--- a/Admin/Release/makebin	Sun Jan 13 20:30:33 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,118 +0,0 @@
-#!/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"
diff -r 8f6046b7f850 -r e932198be619 Admin/Release/makedist_library
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Release/makedist_library	Sun Jan 13 20:59:59 2013 +0100
@@ -0,0 +1,96 @@
+#!/usr/bin/env bash
+#
+# makedist_library -- build Isabelle HTML library from platform bundle
+
+## diagnostics
+
+PRG=$(basename "$0")
+
+function usage()
+{
+  echo
+  echo "Usage: $PRG [OPTIONS] ARCHIVE"
+  echo
+  echo "  Options are:"
+  echo "    -j INT       maximum number of parallel jobs (default 1)"
+  echo
+  echo "  Build Isabelle HTML library from platform bundle."
+  echo
+  exit 1
+}
+
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+
+## process command line
+
+# options
+
+JOBS=""
+
+while getopts "j:" OPT
+do
+  case "$OPT" in
+    j)
+      JOBS="-j $OPTARG"
+      ;;
+    \?)
+      usage
+      ;;
+  esac
+done
+
+shift $(($OPTIND - 1))
+
+
+# args
+
+[ "$#" -ne 1 ] && usage
+
+ARCHIVE="$1"; shift
+
+[ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
+ARCHIVE_BASE="$(basename "$ARCHIVE")"
+ARCHIVE_DIR="$(cd "$(dirname "$ARCHIVE")"; echo "$PWD")"
+ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE"
+
+
+## main
+
+export COPYFILE_DISABLE=true
+
+TMP="/var/tmp/isabelle-makedist$$"
+mkdir "$TMP" || fail "Cannot create directory: \"$TMP\""
+
+cd "$TMP"
+tar -x -z -f "$ARCHIVE_FULL"
+
+cd *
+ISABELLE_NAME="$(basename "$PWD")"
+
+echo "Z3_NON_COMMERCIAL=yes" >> etc/settings
+echo "ISABELLE_FULL_TEST=true" >> etc/settings
+
+echo -n > src/Doc/ROOT
+
+env ISABELLE_IDENTIFIER="${ISABELLE_NAME}-build" \
+  ./bin/isabelle build $JOBS -s -c -a -o browser_info \
+    -o "document=pdf" -o "document_variants=document:outline=/proof,/ML"
+RC="$?"
+
+cd ..
+
+if [ "$RC" = 0 ]; then
+  chmod -R g=o "$ISABELLE_NAME"
+  tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_library.tar.gz" "$ISABELLE_NAME/browser_info"
+fi
+
+# clean up
+cd /tmp
+rm -rf "$TMP"
+
+exit "$RC"