Admin/Release/makedist
author wenzelm
Tue Aug 14 10:44:03 2012 +0200 (2012-08-14)
changeset 48790 6e739225dd8a
parent 48606 4b6c90e121b1
child 48972 196520d51afd
permissions -rwxr-xr-x
always retain doc-src (as regular component);
     1 #!/usr/bin/env bash
     2 #
     3 # makedist -- make Isabelle source distribution
     4 
     5 ## global settings
     6 
     7 REPOS_NAME="isabelle"
     8 REPOS="${REPOS:-http://isabelle.in.tum.de/repos/${REPOS_NAME}}"
     9 DISTPREFIX="${DISTPREFIX:-$HOME/tmp/isadist}"
    10 
    11 umask 022
    12 
    13 
    14 ## diagnostics
    15 
    16 PRG="$(basename "$0")"
    17 THIS="$(cd $(dirname "$0"); pwd)"
    18 
    19 function usage()
    20 {
    21   cat <<EOF
    22 
    23 Usage: $PRG [OPTIONS] [VERSION]
    24 
    25   Options are:
    26     -j JEDIT_BUILD     build Isabelle/jEdit via given jedit_build component
    27     -r RELEASE         proper release with name"
    28 
    29   Make Isabelle distribution from the main Mercurial repository at TUM.
    30 
    31   VERSION identifies the snapshot, using usual Mercurial terminology;
    32   the default is RELEASE if given, otherwise "tip".
    33 
    34 EOF
    35   exit 1
    36 }
    37 
    38 function fail()
    39 {
    40   echo "$1" >&2
    41   exit 2
    42 }
    43 
    44 
    45 ## process command line
    46 
    47 # options
    48 
    49 RELEASE=""
    50 ISABELLE_JEDIT_BUILD_HOME=""
    51 
    52 while getopts "j:r:" OPT
    53 do
    54   case "$OPT" in
    55     j)
    56       ISABELLE_JEDIT_BUILD_HOME="$OPTARG"
    57       ;;
    58     r)
    59       RELEASE="$OPTARG"
    60       ;;
    61     \?)
    62       usage
    63       ;;
    64   esac
    65 done
    66 
    67 shift $(($OPTIND - 1))
    68 
    69 
    70 # args
    71 
    72 VERSION=""
    73 [ "$#" -gt 0 ] && { VERSION="$1"; shift; }
    74 [ -z "$VERSION" ] && VERSION="$RELEASE"
    75 [ -z "$VERSION" ] && VERSION="tip"
    76 
    77 [ "$#" -gt 0 ] && usage
    78 
    79 
    80 ## main
    81 
    82 # tmp
    83 
    84 TMP="tmp-$USER$$"
    85 function purge_tmp () { rm -rf "$DISTPREFIX/$TMP"; }
    86 
    87 
    88 # retrieve archive and resolve version identifier
    89 
    90 mkdir "$DISTPREFIX/$TMP" || fail "Failed to create fresh directory"
    91 cd "$DISTPREFIX/$TMP"
    92 
    93 echo "###"
    94 echo "### Retrieving Mercurial repository $VERSION"
    95 echo "###"
    96 
    97 if expr match "$REPOS" "https\?://" > /dev/null
    98 then
    99   { wget -q "$REPOS/archive/${VERSION}.tar.gz" -O- | tar -xzf -; } || \
   100     fail "Failed to retrieve $VERSION"
   101 else
   102   { hg --repository "$REPOS" archive --type tgz - | tar -xzf -; } || \
   103     fail "Failed to retrieve $VERSION"
   104 fi
   105 
   106 IDENT=$(echo * | sed "s/${REPOS_NAME}-//")
   107 
   108 rm -f "${REPOS_NAME}-${IDENT}/.hg_archival.txt"
   109 rm -f "${REPOS_NAME}-${IDENT}/.hgtags"
   110 rm -f "${REPOS_NAME}-${IDENT}/.hgignore"
   111 rm -f "${REPOS_NAME}-${IDENT}/README_REPOSITORY"
   112 
   113 
   114 # dist name
   115 
   116 DATE=$(env LC_ALL=C date "+%d-%b-%Y")
   117 DISTDATE=$(env LC_ALL=C date "+%B %Y")
   118 
   119 if [ -z "$RELEASE" ]; then
   120   DISTNAME="Isabelle_$DATE"
   121   DISTVERSION="Isabelle repository snapshot $IDENT $DATE"
   122 else
   123   DISTNAME="$RELEASE"
   124   DISTVERSION="$DISTNAME: $DISTDATE"
   125 fi
   126 
   127 DISTBASE="$DISTPREFIX/dist-$DISTNAME"
   128 mkdir -p "$DISTBASE" || { purge_tmp; fail "Unable to create distribution base dir $DISTBASE!"; }
   129 [ -e "$DISTBASE/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/$DISTNAME already exists!"; }
   130 
   131 cd "$DISTBASE"
   132 mv "$DISTPREFIX/$TMP/${REPOS_NAME}-${IDENT}" "$DISTNAME"
   133 purge_tmp
   134 
   135 cd "$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME"
   136 
   137 
   138 # prepare dist for release
   139 
   140 echo "###"
   141 echo "### Preparing distribution $DISTNAME"
   142 echo "###"
   143 
   144 rm -f .hgignore
   145 find . "(" -name \*.thy -o -name \*.ML -o -name \*.scala ")" -perm +111 -print | xargs chmod -f -x
   146 find . -print | xargs chmod -f u+rw
   147 
   148 perl -pi -e 's/^(ISABELLE_SCALA_BUILD_OPTIONS=")/$1-optimise /,' etc/settings
   149 
   150 cp -a doc-src doc-src.orig
   151 
   152 ./Admin/build all || fail "Failed to build distribution"
   153 
   154 if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
   155   [ -d "$ISABELLE_JEDIT_BUILD_HOME" ] || fail "Bad jedit_build component directory: \"$ISABELLE_JEDIT_BUILD_HOME\""
   156   eval "$(fgrep ISABELLE_JEDIT_BUILD_VERSION "$ISABELLE_JEDIT_BUILD_HOME/etc/settings")"
   157   [ -n "$ISABELLE_JEDIT_BUILD_VERSION" ] || fail "Bad ISABELLE_JEDIT_BUILD_VERSION"
   158   export ISABELLE_JEDIT_BUILD_HOME ISABELLE_JEDIT_BUILD_VERSION
   159   ./bin/isabelle jedit -b || fail "Failed to build Isabelle/jEdit"
   160 fi
   161 
   162 rm -rf Admin
   163 
   164 MOVE=$(find doc-src \( -type f -a -not -type l -a -not -name isabelle_isar.pdf -a -not -name pghead.pdf -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps -o -name \*.pdf \) -a -print \) | grep -v 'gfx/.*pdf')
   165 mv -f $MOVE doc
   166 rm doc/Isa-logics.eps
   167 rm doc/adaptation.dvi doc/adaptation.pdf doc/architecture.dvi doc/architecture.pdf
   168 rm -rf doc-src
   169 
   170 mv doc-src.orig doc-src
   171 
   172 mkdir -p contrib
   173 cat >contrib/README <<EOF
   174 This directory contains add-on components that contribute to the main
   175 Isabelle distribution.  Separate licensing conditions apply, see each
   176 directory individually.
   177 EOF
   178 
   179 cp doc/isabelle*.eps lib/logo
   180 
   181 if [ -z "$RELEASE" ]; then
   182   {
   183     echo
   184     echo "IMPORTANT NOTE"
   185     echo "=============="
   186     echo
   187     echo "This is an unofficial snapshot of Isabelle, created by $LOGNAME $DATE."
   188     echo "See $REPOS/log/$IDENT for details."
   189     echo
   190   } >ANNOUNCE
   191 else
   192   perl -pi -e "s,val is_official = false,val is_official = true,g" src/Pure/ROOT.ML
   193 fi
   194 
   195 perl -pi -e "s,val changelog = \"\",val changelog = \"$REPOS/log/$IDENT\",g" src/Pure/ROOT.ML
   196 perl -pi -e "s,ISABELLE_ID=\"\",ISABELLE_ID=\"$IDENT\",g" lib/scripts/getsettings
   197 perl -pi -e "s,ISABELLE_IDENTIFIER=\"\",ISABELLE_IDENTIFIER=\"$DISTNAME\",g" lib/scripts/getsettings
   198 perl -pi -e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template
   199 perl -pi -e "s,unidentified repository version,$DISTVERSION,g" src/Pure/ROOT.ML lib/Tools/version
   200 perl -pi -e "s,some unidentified repository version of Isabelle,$DISTVERSION,g" README
   201 
   202 
   203 # create archive
   204 
   205 echo "###"
   206 echo "### Creating archive ..."
   207 echo "###"
   208 
   209 cd "$DISTBASE"
   210 
   211 echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST
   212 echo "$IDENT" >../ISABELLE_IDENT
   213 
   214 chown -R "$LOGNAME" "$DISTNAME"
   215 chmod -R u+w "$DISTNAME"
   216 chmod -R g=o "$DISTNAME"
   217 chgrp -R isabelle "$DISTNAME"
   218 
   219 echo "$DISTNAME.tar.gz"
   220 tar -czf "$DISTNAME.tar.gz" "$DISTNAME"
   221 
   222 
   223 # cleanup dist
   224 
   225 mv "$DISTNAME" "${DISTNAME}-old"
   226 mkdir "$DISTNAME"
   227 
   228 mv "${DISTNAME}-old/README" "${DISTNAME}-old/NEWS" "${DISTNAME}-old/ANNOUNCE" \
   229   "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" "$DISTNAME"
   230 mkdir "$DISTNAME/doc"
   231 mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc"
   232 
   233 rm -f Isabelle && ln -sf "$DISTNAME" Isabelle
   234 
   235 chgrp -R isabelle "$DISTNAME"
   236 
   237 rm -rf "${DISTNAME}-old"
   238 
   239 echo "DONE"