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