explicit option to build library, which takes most of the time;
authorwenzelm
Wed, 07 May 2014 18:09:08 +0200
changeset 56902 f901a08c5653
parent 56901 2f73ef9eb272
child 56903 69b6369a98fa
child 56905 fb38a767a78b
explicit option to build library, which takes most of the time; produce minimal index, e.g. for test web page;
Admin/Release/CHECKLIST
Admin/Release/build
--- a/Admin/Release/CHECKLIST	Wed May 07 14:54:06 2014 +0200
+++ b/Admin/Release/CHECKLIST	Wed May 07 18:09:08 2014 +0200
@@ -70,7 +70,7 @@
 
 - fully-automated packaging (requires Mac OS X):
 
-  hg up -r DISTNAME && Admin/Release/build -r DISTNAME /home/isabelle/dist
+  hg up -r DISTNAME && Admin/Release/build -l -r DISTNAME /home/isabelle/dist
 
 
 Final release stage
--- a/Admin/Release/build	Wed May 07 14:54:06 2014 +0200
+++ b/Admin/Release/build	Wed May 07 18:09:08 2014 +0200
@@ -19,6 +19,7 @@
   echo
   echo "  Options are:"
   echo "    -j INT       maximum number of parallel jobs (default 1)"
+  echo "    -l           build library"
   echo "    -r RELEASE   proper release with name"
   echo
   echo "  Make Isabelle distribution DIR, using the local repository clone."
@@ -46,15 +47,19 @@
 # options
 
 JOBS=""
+LIBRARY=""
 RELEASE=""
 
-while getopts "j:r:" OPT
+while getopts "j:lr:" OPT
 do
   case "$OPT" in
     j)
       check_number "$OPTARG"
       JOBS="-j $OPTARG"
       ;;
+    l)
+      LIBRARY="true"
+      ;;
     r)
       RELEASE="$OPTARG"
       ;;
@@ -89,6 +94,8 @@
 
 ## main
 
+# make dist
+
 if [ -z "$RELEASE" ]; then
   DISTNAME="Isabelle_$(env LC_ALL=C date "+%d-%b-%Y")"
   "$ISABELLE_TOOL" makedist -d "$BASE_DIR" $JOBS
@@ -101,6 +108,8 @@
 DISTBASE="$BASE_DIR/dist-${DISTNAME}"
 
 
+# make bundles
+
 for PLATFORM_FAMILY in linux macos windows
 do
 
@@ -112,5 +121,32 @@
 
 done
 
-"$THIS/build_library" $JOBS "$DISTBASE/${DISTNAME}_${ISABELLE_PLATFORM_FAMILY}.tar.gz"
+
+# minimal index
+
+cat > "$DISTBASE/index.html" <<EOF
+<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 3.2//EN">
+<html>
+<head>
+<title>${DISTNAME}</title>
+</head>
 
+<body>
+<h1>${DISTNAME}</h1>
+<ul>
+<li><a href="${DISTNAME}_linux.tar.gz">Linux</a></li>
+<li><a href="${DISTNAME}.exe">Windows</a></li>
+<li><a href="${DISTNAME}.dmg">Mac OS X</a></li>
+</ul>
+</body>
+
+</html>
+EOF
+
+
+# HTML library
+
+if [ -n "$LIBRARY" ]; then
+  "$THIS/build_library" $JOBS "$DISTBASE/${DISTNAME}_${ISABELLE_PLATFORM_FAMILY}.tar.gz"
+fi
+