# HG changeset patch # User wenzelm # Date 1346268046 -7200 # Node ID 3a324a3f4aea864b346295e9567b8ca1c1c358cc # Parent 09a9761cf5ae1fea79e491646e0573ada94ad9c4 more formal isabelle makedist from repository; diff -r 09a9761cf5ae -r 3a324a3f4aea Admin/Release/CHECKLIST --- a/Admin/Release/CHECKLIST Wed Aug 29 21:01:05 2012 +0200 +++ b/Admin/Release/CHECKLIST Wed Aug 29 21:20:46 2012 +0200 @@ -46,7 +46,7 @@ Packaging ========= -- makedist -j jedit_build-XXXX -r DISTNAME +- hg up -r DISTNAME && isabelle makedist -r DISTNAME; - makebin (multiplatform); diff -r 09a9761cf5ae -r 3a324a3f4aea Admin/Release/makedist --- a/Admin/Release/makedist Wed Aug 29 21:01:05 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,233 +0,0 @@ -#!/usr/bin/env bash -# -# makedist -- make Isabelle source distribution - -## global settings - -REPOS_NAME="isabelle" -REPOS="${REPOS:-http://isabelle.in.tum.de/repos/${REPOS_NAME}}" -DISTPREFIX="${DISTPREFIX:-$HOME/tmp/isadist}" - -umask 022 - - -## diagnostics - -PRG="$(basename "$0")" -THIS="$(cd $(dirname "$0"); pwd)" - -function usage() -{ - cat <&2 - exit 2 -} - - -## process command line - -# options - -RELEASE="" -ISABELLE_JEDIT_BUILD_HOME="" - -while getopts "j:r:" OPT -do - case "$OPT" in - j) - ISABELLE_JEDIT_BUILD_HOME="$OPTARG" - ;; - r) - RELEASE="$OPTARG" - ;; - \?) - usage - ;; - esac -done - -shift $(($OPTIND - 1)) - - -# args - -VERSION="" -[ "$#" -gt 0 ] && { VERSION="$1"; shift; } -[ -z "$VERSION" ] && VERSION="$RELEASE" -[ -z "$VERSION" ] && VERSION="tip" - -[ "$#" -gt 0 ] && usage - - -## main - -# tmp - -TMP="tmp-$USER$$" -function purge_tmp () { rm -rf "$DISTPREFIX/$TMP"; } - - -# retrieve archive and resolve version identifier - -mkdir "$DISTPREFIX/$TMP" || fail "Failed to create fresh directory" -cd "$DISTPREFIX/$TMP" - -echo "###" -echo "### Retrieving Mercurial repository $VERSION" -echo "###" - -if expr match "$REPOS" "https\?://" > /dev/null -then - { wget -q "$REPOS/archive/${VERSION}.tar.gz" -O- | tar -xzf -; } || \ - fail "Failed to retrieve $VERSION" -else - { hg --repository "$REPOS" archive --type tgz - | tar -xzf -; } || \ - fail "Failed to retrieve $VERSION" -fi - -IDENT=$(echo * | sed "s/${REPOS_NAME}-//") - -rm -f "${REPOS_NAME}-${IDENT}/.hg_archival.txt" -rm -f "${REPOS_NAME}-${IDENT}/.hgtags" -rm -f "${REPOS_NAME}-${IDENT}/.hgignore" -rm -f "${REPOS_NAME}-${IDENT}/README_REPOSITORY" - - -# dist name - -DATE=$(env LC_ALL=C date "+%d-%b-%Y") -DISTDATE=$(env LC_ALL=C date "+%B %Y") - -if [ -z "$RELEASE" ]; then - DISTNAME="Isabelle_$DATE" - DISTVERSION="Isabelle repository snapshot $IDENT $DATE" -else - DISTNAME="$RELEASE" - DISTVERSION="$DISTNAME: $DISTDATE" -fi - -DISTBASE="$DISTPREFIX/dist-$DISTNAME" -mkdir -p "$DISTBASE" || { purge_tmp; fail "Unable to create distribution base dir $DISTBASE!"; } -[ -e "$DISTBASE/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/$DISTNAME already exists!"; } - -cd "$DISTBASE" -mv "$DISTPREFIX/$TMP/${REPOS_NAME}-${IDENT}" "$DISTNAME" -purge_tmp - -cd "$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME" - - -# prepare dist for release - -echo "###" -echo "### Preparing distribution $DISTNAME" -echo "###" - -rm -f .hgignore -find . "(" -name \*.thy -o -name \*.ML -o -name \*.scala ")" -perm +111 -print | xargs chmod -f -x -find . -print | xargs chmod -f u+rw - -perl -pi -e 's/^(ISABELLE_SCALA_BUILD_OPTIONS=")/$1-optimise /,' etc/settings - -./Admin/build all || fail "Failed to build distribution" - -cp -a src/Doc src/Doc.orig -# FIXME -# ./bin/isabelle build_doc -a || fail "Failed to build documentation" - -if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then - [ -d "$ISABELLE_JEDIT_BUILD_HOME" ] || fail "Bad jedit_build component directory: \"$ISABELLE_JEDIT_BUILD_HOME\"" - eval "$(fgrep ISABELLE_JEDIT_BUILD_VERSION "$ISABELLE_JEDIT_BUILD_HOME/etc/settings")" - [ -n "$ISABELLE_JEDIT_BUILD_VERSION" ] || fail "Bad ISABELLE_JEDIT_BUILD_VERSION" - export ISABELLE_JEDIT_BUILD_HOME ISABELLE_JEDIT_BUILD_VERSION - ./bin/isabelle jedit -b || fail "Failed to build Isabelle/jEdit" -fi - -rm -rf Admin -rm -rf src/Doc - -mv src/Doc.orig src/Doc - -mkdir -p contrib -cat >contrib/README <ANNOUNCE -else - perl -pi -e "s,val is_official = false,val is_official = true,g" src/Pure/ROOT.ML -fi - -perl -pi -e "s,ISABELLE_ID=\"\",ISABELLE_ID=\"$IDENT\",g" lib/scripts/getsettings -perl -pi -e "s,ISABELLE_IDENTIFIER=\"\",ISABELLE_IDENTIFIER=\"$DISTNAME\",g" lib/scripts/getsettings -perl -pi -e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template -perl -pi -e "s,unidentified repository version,$DISTVERSION,g" src/Pure/ROOT.ML lib/Tools/version -perl -pi -e "s,some unidentified repository version of Isabelle,$DISTVERSION,g" README - - -# create archive - -echo "###" -echo "### Creating archive ..." -echo "###" - -cd "$DISTBASE" - -echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST -echo "$IDENT" >../ISABELLE_IDENT - -chown -R "$LOGNAME" "$DISTNAME" -chmod -R u+w "$DISTNAME" -chmod -R g=o "$DISTNAME" -chgrp -R isabelle "$DISTNAME" - -echo "$DISTNAME.tar.gz" -tar -czf "$DISTNAME.tar.gz" "$DISTNAME" - - -# cleanup dist - -mv "$DISTNAME" "${DISTNAME}-old" -mkdir "$DISTNAME" - -mv "${DISTNAME}-old/README" "${DISTNAME}-old/NEWS" "${DISTNAME}-old/ANNOUNCE" \ - "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" "$DISTNAME" -mkdir "$DISTNAME/doc" -mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc" - -rm -f Isabelle && ln -sf "$DISTNAME" Isabelle - -chgrp -R isabelle "$DISTNAME" - -rm -rf "${DISTNAME}-old" - -echo "DONE" diff -r 09a9761cf5ae -r 3a324a3f4aea Admin/isatest/isatest-makedist --- a/Admin/isatest/isatest-makedist Wed Aug 29 21:01:05 2012 +0200 +++ b/Admin/isatest/isatest-makedist Wed Aug 29 21:20:46 2012 +0200 @@ -5,12 +5,11 @@ # DESCRIPTION: Build distribution and run isatest-make for lots of platforms. ## global settings -. ~/admin/isatest/isatest-settings +. "$HOME/hg-isabelle/Admin/isatest/isatest-settings" TMP=/tmp/isatest-makedist.$$ MAIL=$HOME/bin/pmail -MAKEDIST=$HOME/bin/makedist MAKEALL=$HOME/bin/isatest-makeall TAR=tar @@ -60,7 +59,7 @@ echo "### building distribution" >> $DISTLOG 2>&1 mkdir -p $DISTPREFIX -$MAKEDIST -j "/home/isabelle/contrib/jedit_build-20120813" >> $DISTLOG 2>&1 +"$HOME/hg-isabelle/bin/isabelle" makedist >> $DISTLOG 2>&1 if [ $? -ne 0 ] then diff -r 09a9761cf5ae -r 3a324a3f4aea Admin/lib/Tools/makedist --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/lib/Tools/makedist Wed Aug 29 21:20:46 2012 +0200 @@ -0,0 +1,219 @@ +#!/usr/bin/env bash +# +# Author: Makarius +# +# DESCRIPTION: make Isabelle distribution from repository + +## global parameters + +umask 022 + +HG="${HG:-hg}" + +DISTPREFIX="${DISTPREFIX:-$HOME/tmp/isadist}" + + +## diagnostics + +PRG="$(basename "$0")" + +function usage() +{ + echo + echo "Usage: isabelle $PRG [OPTIONS] [VERSION]" + echo + echo " Options are:" + echo " -d DIR global directory prefix (default: \"$DISTPREFIX\")" + echo " -j INT maximum number of parallel jobs (default 1)" + echo " -r RELEASE proper release with name" + echo + echo " Make Isabelle distribution from the local repository clone." + echo + echo " VERSION identifies the snapshot, using usual Mercurial terminology;" + echo " the default is RELEASE if given, otherwise \"tip\"." + echo + echo " Auxiliary components are that of the running Isabelle version!" + 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 "d:j:r:" OPT +do + case "$OPT" in + d) + DISTPREFIX="$OPTARG" + ;; + j) + check_number "$OPTARG" + JOBS="-j $OPTARG" + ;; + r) + RELEASE="$OPTARG" + ;; + \?) + usage + ;; + esac +done + +shift $(($OPTIND - 1)) + + +# args + +VERSION="" +[ "$#" -gt 0 ] && { VERSION="$1"; shift; } +[ -z "$VERSION" ] && VERSION="$RELEASE" +[ -z "$VERSION" ] && VERSION="tip" + +[ "$#" -gt 0 ] && usage + +IDENT=$("$HG" --repository "$ISABELLE_HOME" id -r "$VERSION" -i) +[ -z "$IDENT" ] && fail "Bad repository version: \"$VERSION\"" + + +## main + +# dist name + +DATE=$(env LC_ALL=C date "+%d-%b-%Y") +DISTDATE=$(env LC_ALL=C date "+%B %Y") + +if [ -z "$RELEASE" ]; then + DISTNAME="Isabelle_$DATE" + DISTVERSION="Isabelle repository snapshot $IDENT $DATE" +else + DISTNAME="$RELEASE" + DISTVERSION="$DISTNAME: $DISTDATE" +fi + +DISTBASE="$DISTPREFIX/dist-$DISTNAME" +mkdir -p "$DISTBASE" || fail "Unable to create distribution base dir \"$DISTBASE\"" + +DIR="$DISTBASE/$DISTNAME" +[ -e "$DIR" ] && fail "Directory \"$DIR\" already exists" + + +# retrieve repository archive + +echo "### Retrieving Mercurial repository $VERSION" + +"$HG" --repository "$ISABELLE_HOME" archive --type files -r "$IDENT" "$DIR" || \ + fail "Failed to retrieve $VERSION" + +rm -f "$DIR/.hg_archival.txt" +rm -f "$DIR/.hgtags" +rm -f "$DIR/.hgignore" +rm -f "$DIR/README_REPOSITORY" + + +# partial context switch to new version + +cd "$DIR" + +unset ISABELLE_SETTINGS_PRESENT +unset ISABELLE_SITE_SETTINGS_PRESENT + +if [ -z "$RELEASE" ]; then + { + echo + echo "IMPORTANT NOTE" + echo "==============" + echo + echo "This is snapshot of Isabelle/${IDENT} from the repository." + echo + } >ANNOUNCE +else + perl -pi -e "s,val is_official = false,val is_official = true,g" src/Pure/ROOT.ML +fi + +perl -pi -e "s,ISABELLE_ID=\"\",ISABELLE_ID=\"$IDENT\",g" lib/scripts/getsettings +perl -pi -e "s,ISABELLE_IDENTIFIER=\"\",ISABELLE_IDENTIFIER=\"$DISTNAME\",g" lib/scripts/getsettings +perl -pi -e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template +perl -pi -e "s,unidentified repository version,$DISTVERSION,g" src/Pure/ROOT.ML lib/Tools/version +perl -pi -e "s,some unidentified repository version of Isabelle,$DISTVERSION,g" README + +mkdir -p contrib +cat >contrib/README < ../ISABELLE_DIST +echo "$IDENT" >../ISABELLE_IDENT + +chown -R "$LOGNAME" "$DISTNAME" +chmod -R u+w "$DISTNAME" +chmod -R g=o "$DISTNAME" + +echo "$DISTNAME.tar.gz" +tar -czf "$DISTNAME.tar.gz" "$DISTNAME" + + +# cleanup dist + +mv "$DISTNAME" "${DISTNAME}-old" +mkdir "$DISTNAME" + +mv "${DISTNAME}-old/README" "${DISTNAME}-old/NEWS" "${DISTNAME}-old/ANNOUNCE" \ + "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" "$DISTNAME" +mkdir "$DISTNAME/doc" +mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc" + +rm -f Isabelle && ln -sf "$DISTNAME" Isabelle + +rm -rf "${DISTNAME}-old" + +echo "DONE" diff -r 09a9761cf5ae -r 3a324a3f4aea lib/browser/build --- a/lib/browser/build Wed Aug 29 21:01:05 2012 +0200 +++ b/lib/browser/build Wed Aug 29 21:20:46 2012 +0200 @@ -59,9 +59,7 @@ if [ "$OUTDATED" = true ] then - echo "###" echo "### Building graph browser ..." - echo "###" rm -rf classes && mkdir classes