1#!/usr/bin/env bash 2# 3# Author: Makarius 4# 5# DESCRIPTION: make Isabelle distribution from repository 6 7## global parameters 8 9umask 022 10 11HG="${HG:-hg}" 12 13DISTPREFIX="${DISTPREFIX:-$HOME/tmp/isadist}" 14 15 16## diagnostics 17 18PRG="$(basename "$0")" 19 20function usage() 21{ 22 echo 23 echo "Usage: isabelle $PRG [OPTIONS] [VERSION]" 24 echo 25 echo " Options are:" 26 echo " -O official release (not release-candidate)" 27 echo " -d DIR global directory prefix (default: \"$DISTPREFIX\")" 28 echo " -j INT maximum number of parallel jobs (default 1)" 29 echo " -r RELEASE proper release with name" 30 echo 31 echo " Make Isabelle distribution from the local repository clone." 32 echo 33 echo " VERSION identifies the snapshot, using usual Mercurial terminology;" 34 echo " the default is RELEASE if given, otherwise \"tip\"." 35 echo 36 echo " Add-on components are that of the running Isabelle version!" 37 echo 38 exit 1 39} 40 41function fail() 42{ 43 echo "$1" >&2 44 exit 2 45} 46 47function check_number() 48{ 49 [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\"" 50} 51 52 53## process command line 54 55# options 56 57OFFICIAL_RELEASE="false" 58JOBS="" 59RELEASE="" 60 61while getopts "Od:j:r:" OPT 62do 63 case "$OPT" in 64 O) 65 OFFICIAL_RELEASE="true" 66 ;; 67 d) 68 DISTPREFIX="$OPTARG" 69 ;; 70 j) 71 check_number "$OPTARG" 72 JOBS="-j $OPTARG" 73 ;; 74 r) 75 RELEASE="$OPTARG" 76 ;; 77 \?) 78 usage 79 ;; 80 esac 81done 82 83shift $(($OPTIND - 1)) 84 85 86# args 87 88VERSION="" 89[ "$#" -gt 0 ] && { VERSION="$1"; shift; } 90[ -z "$VERSION" ] && VERSION="$RELEASE" 91[ -z "$VERSION" ] && VERSION="tip" 92 93[ "$#" -gt 0 ] && usage 94 95IDENT=$("$HG" --repository "$ISABELLE_HOME" id -r "$VERSION" -i) 96[ -z "$IDENT" ] && fail "Bad repository version: \"$VERSION\"" 97 98 99## main 100 101# dist name 102 103DATE=$(env LC_ALL=C date "+%d-%b-%Y") 104DISTDATE=$(env LC_ALL=C date "+%B %Y") 105 106if [ -z "$RELEASE" ]; then 107 DISTNAME="Isabelle_$DATE" 108 DISTVERSION="Isabelle repository snapshot $IDENT $DATE" 109else 110 DISTNAME="$RELEASE" 111 DISTVERSION="$DISTNAME: $DISTDATE" 112fi 113 114DISTPREFIX="$(cd "$DISTPREFIX"; pwd)" 115DISTBASE="$DISTPREFIX/dist-$DISTNAME" 116mkdir -p "$DISTBASE" || fail "Unable to create distribution base dir \"$DISTBASE\"" 117 118DIR="$DISTBASE/$DISTNAME" 119[ -e "$DIR" ] && fail "Directory \"$DIR\" already exists" 120 121rm -f "$DISTPREFIX/ISABELLE_DIST" "$DISTPREFIX/ISABELLE_IDENT" 122 123 124# retrieve repository archive 125 126echo "### Retrieving Mercurial repository version $VERSION" 127 128"$HG" --repository "$ISABELLE_HOME" archive --type files -r "$IDENT" "$DIR" || \ 129 fail "Failed to retrieve $VERSION" 130 131rm -f "$DIR/.hg_archival.txt" 132rm -f "$DIR/.hgtags" 133rm -f "$DIR/.hgignore" 134rm -f "$DIR/README_REPOSITORY" 135 136 137# partial context switch to new version 138 139cd "$DIR" 140 141unset ISABELLE_SETTINGS_PRESENT 142unset ISABELLE_SITE_SETTINGS_PRESENT 143 144if [ -z "$RELEASE" ]; then 145 { 146 echo 147 echo "IMPORTANT NOTE" 148 echo "==============" 149 echo 150 echo "This is a snapshot of Isabelle/${IDENT} from the repository." 151 echo 152 } >ANNOUNCE 153fi 154 155if [ -n "$RELEASE" -a "$OFFICIAL_RELEASE" = true ]; then 156 IS_OFFICIAL="true" 157else 158 IS_OFFICIAL="false" 159fi 160 161perl -pi \ 162 -e "s,val is_identified = false,val is_identified = true,g;" \ 163 -e "s,val is_official = false,val is_official = ${IS_OFFICIAL},g;" \ 164 src/Pure/System/distribution.ML src/Pure/System/distribution.scala 165 166perl -pi -e "s,ISABELLE_ID=\"\",ISABELLE_ID=\"$IDENT\",g" lib/scripts/getsettings 167perl -pi -e "s,ISABELLE_IDENTIFIER=\"\",ISABELLE_IDENTIFIER=\"$DISTNAME\",g" lib/scripts/getsettings 168perl -pi -e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template 169perl -pi -e "s,repository version,$DISTVERSION,g" \ 170 src/Pure/System/distribution.ML src/Pure/System/distribution.scala lib/Tools/version 171perl -pi -e "s,some repository version of Isabelle,$DISTVERSION,g" README 172 173mkdir -p contrib 174cat >contrib/README <<EOF 175This directory contains add-on components that contribute to the main 176Isabelle distribution. Separate licensing conditions apply, see each 177directory individually. 178EOF 179 180 181# prepare dist for release 182 183echo "### Preparing distribution $DISTNAME" 184 185find . "(" -name \*.thy -o -name \*.ML -o -name \*.scala ")" -print | xargs chmod -f -x 186find . -print | xargs chmod -f u+rw 187 188export CLASSPATH="$ISABELLE_CLASSPATH" 189 190./Admin/build all || fail "Failed to build distribution" 191 192./bin/isabelle jedit -b || fail "Failed to build Isabelle/jEdit" 193 194cp -a src src.orig 195env ISABELLE_IDENTIFIER="${DISTNAME}-build" \ 196 ./bin/isabelle build_doc $JOBS -s -a || fail "Failed to build documentation" 197rm -rf src 198mv src.orig src 199 200./bin/isabelle news 201 202rm -rf Admin browser_info heaps 203 204rmdir "$USER_HOME/.isabelle/${DISTNAME}-build" 205rmdir "$USER_HOME/.isabelle/${DISTNAME}" 206 207 208# create archive 209 210#GNU tar (notably on Mac OS X) 211type -p gnutar >/dev/null && function tar() { gnutar "$@"; } 212 213echo "### Creating archive" 214 215cd "$DISTBASE" 216 217echo "$DISTBASE/$DISTNAME.tar.gz" > "$DISTPREFIX/ISABELLE_DIST" 218echo "$IDENT" > "$DISTPREFIX/ISABELLE_IDENT" 219 220chown -R "$LOGNAME" "$DISTNAME" 221chmod -R g=o "$DISTNAME" 222chmod -R u+w "$DISTNAME" 223find "$DISTNAME" -type f "(" -name '*.scala' -o -name '*.ML' -o -name '*.thy' ")" -print | xargs chmod -f u-w 224 225echo "$DISTBASE/$DISTNAME.tar.gz" 226tar -c -z -f "$DISTNAME.tar.gz" "$DISTNAME" 227[ "$?" = 0 ] || exit "$?" 228 229 230# cleanup dist 231 232mv "$DISTNAME" "${DISTNAME}-old" 233mkdir "$DISTNAME" 234 235mv "${DISTNAME}-old/README" "${DISTNAME}-old/NEWS" "${DISTNAME}-old/ANNOUNCE" \ 236 "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" "$DISTNAME" 237mkdir "$DISTNAME/doc" 238mv "${DISTNAME}-old/doc/"*.pdf \ 239 "${DISTNAME}-old/doc/"*.html \ 240 "${DISTNAME}-old/doc/"*.css \ 241 "${DISTNAME}-old/doc/fonts" \ 242 "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc" 243 244rm -f Isabelle && ln -sf "$DISTNAME" Isabelle 245 246rm -rf "${DISTNAME}-old" 247