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" +