# HG changeset patch # User wenzelm # Date 1358249423 -3600 # Node ID 506ff6abfde0614b7de1c0ea5355d72641a03e3a # Parent 3a1edaa0dc6d9e371a2af4224ee6944a21982097 grand-unified Admin/Release/build script (excluding .app and .exe); diff -r 3a1edaa0dc6d -r 506ff6abfde0 Admin/Release/CHECKLIST --- a/Admin/Release/CHECKLIST Mon Jan 14 23:08:40 2013 +0100 +++ b/Admin/Release/CHECKLIST Tue Jan 15 12:30:23 2013 +0100 @@ -53,11 +53,7 @@ Packaging ========= -- hg up -r DISTNAME && isabelle makedist -r DISTNAME - -- isabelle makedist_bundles - -- ./makedist_library DISTNAME_linux.tar.gz +- hg up -r DISTNAME && Admin/Release/build -r DISTNAME /home/isabelle/dist - Mac OS X: hdiutil create -srcfolder DIR DMG diff -r 3a1edaa0dc6d -r 506ff6abfde0 Admin/Release/build --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/Release/build Tue Jan 15 12:30:23 2013 +0100 @@ -0,0 +1,107 @@ +#!/usr/bin/env bash +# +# Author: Makarius +# +# build full Isabelle distribution from repository + +THIS="$(cd "$(dirname "$0")"; pwd)" +PRG="$(basename "$0")" + + +## diagnostics + +PRG="$(basename "$0")" + +function usage() +{ + echo + echo "Usage: isabelle $PRG [OPTIONS] DIR [VERSION]" + echo + echo " Options are:" + echo " -j INT maximum number of parallel jobs (default 1)" + echo " -r RELEASE proper release with name" + echo + echo " Make Isabelle distribution DIR, using the local repository clone." + echo + echo " VERSION identifies the snapshot, using usual Mercurial terminology;" + echo " the default is RELEASE if given, otherwise \"tip\"." + echo + exit 1 +} + +function fail() +{ + echo "$1" >&2 + exit 2 +} + +function check_number() +{ + [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\"" +} + + +## process command line + +# options + +JOBS="" +RELEASE="" + +while getopts "j:r:" OPT +do + case "$OPT" in + j) + check_number "$OPTARG" + JOBS="-j $OPTARG" + ;; + r) + RELEASE="$OPTARG" + ;; + \?) + usage + ;; + esac +done + +shift $(($OPTIND - 1)) + + +# args + +BASE_DIR="" +[ "$#" -gt 0 ] && { BASE_DIR="$1"; shift; } +[ -z "$BASE_DIR" ] && usage + +VERSION="" +[ "$#" -gt 0 ] && { VERSION="$1"; shift; } +[ -z "$VERSION" ] && VERSION="$RELEASE" +[ -z "$VERSION" ] && VERSION="tip" + +[ "$#" -gt 0 ] && usage + + +## Isabelle settings + +ISABELLE_TOOL="$THIS/../../bin/isabelle" +ISABELLE_PLATFORM_FAMILY="$("$ISABELLE_TOOL" getenv -b ISABELLE_PLATFORM_FAMILY)" + + +## main + +if [ -z "$RELEASE" ]; then + DISTNAME="Isabelle_$(env LC_ALL=C date "+%d-%b-%Y")" + "$ISABELLE_TOOL" makedist -d "$BASE_DIR" $JOBS +else + DISTNAME="$RELEASE" + "$ISABELLE_TOOL" makedist -d "$BASE_DIR" $JOBS -r "$RELEASE" +fi +[ "$?" = 0 ] || exit "$?" + +DISTBASE="$BASE_DIR/dist-${DISTNAME}" + +"$ISABELLE_TOOL" makedist_bundles "$DISTBASE/${DISTNAME}.tar.gz" +[ "$?" = 0 ] || exit "$?" + +"$THIS/build_library" $JOBS "$DISTBASE/${DISTNAME}_${ISABELLE_PLATFORM_FAMILY}.tar.gz" + diff -r 3a1edaa0dc6d -r 506ff6abfde0 Admin/Release/build_library --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/Release/build_library Tue Jan 15 12:30:23 2013 +0100 @@ -0,0 +1,96 @@ +#!/usr/bin/env bash +# +# 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" diff -r 3a1edaa0dc6d -r 506ff6abfde0 Admin/Release/makedist_library --- a/Admin/Release/makedist_library Mon Jan 14 23:08:40 2013 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,96 +0,0 @@ -#!/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" diff -r 3a1edaa0dc6d -r 506ff6abfde0 Admin/lib/Tools/makedist --- a/Admin/lib/Tools/makedist Mon Jan 14 23:08:40 2013 +0100 +++ b/Admin/lib/Tools/makedist Tue Jan 15 12:30:23 2013 +0100 @@ -197,6 +197,7 @@ echo "$DISTBASE/$DISTNAME.tar.gz" env COPYFILE_DISABLE=true tar -c -z -f "$DISTNAME.tar.gz" "$DISTNAME" +[ "$?" = 0 ] || exit "$?" # cleanup dist @@ -213,4 +214,3 @@ rm -rf "${DISTNAME}-old" -echo "DONE" diff -r 3a1edaa0dc6d -r 506ff6abfde0 Admin/lib/Tools/makedist_bundles --- a/Admin/lib/Tools/makedist_bundles Mon Jan 14 23:08:40 2013 +0100 +++ b/Admin/lib/Tools/makedist_bundles Tue Jan 15 12:30:23 2013 +0100 @@ -177,7 +177,7 @@ BUNDLE_ARCHIVE="${ARCHIVE_DIR}/${ISABELLE_NAME}_${PLATFORM_FAMILY}.tar.gz" echo "packaging $(basename "$BUNDLE_ARCHIVE")" -tar -C "$TMP" -c -z -f "$BUNDLE_ARCHIVE" "$ISABELLE_NAME" +tar -C "$TMP" -c -z -f "$BUNDLE_ARCHIVE" "$ISABELLE_NAME" || exit 2 # clean up