Admin/makedist
author wenzelm
Fri Nov 27 22:38:22 2009 +0100 (2009-11-27)
changeset 33909 24a9d433eb7f
parent 33899 07ab63b320dd
child 33910 bae240a8bfe9
permissions -rwxr-xr-x
more abstract handling of repository name;
     1 #!/usr/bin/env bash
     2 #
     3 # makedist -- make Isabelle source distribution
     4 
     5 ## global settings
     6 
     7 REPOS_NAME="isabelle-release"
     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     -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 
    51 while getopts "r:" OPT
    52 do
    53   case "$OPT" in
    54     r)
    55       RELEASE="$OPTARG"
    56       ;;
    57     \?)
    58       usage
    59       ;;
    60   esac
    61 done
    62 
    63 shift $(($OPTIND - 1))
    64 
    65 
    66 # args
    67 
    68 VERSION=""
    69 [ "$#" -gt 0 ] && { VERSION="$1"; shift; }
    70 [ -z "$VERSION" ] && VERSION="$RELEASE"
    71 [ -z "$VERSION" ] && VERSION="tip"
    72 
    73 [ "$#" -gt 0 ] && usage
    74 
    75 
    76 ## main
    77 
    78 # tmp
    79 
    80 TMP="tmp-$USER$$"
    81 function purge_tmp () { rm -rf "$DISTPREFIX/$TMP"; }
    82 
    83 
    84 # retrieve archive and resolve version identifier
    85 
    86 mkdir "$DISTPREFIX/$TMP" || fail "Failed to create fresh directory"
    87 cd "$DISTPREFIX/$TMP"
    88 
    89 echo "###"
    90 echo "### Retrieving Mercurial repository $VERSION"
    91 echo "###"
    92 
    93 { wget -q "$REPOS/archive/${VERSION}.tar.gz" -O- | tar -xzf -; } || \
    94   fail "Failed to retrieve $VERSION"
    95 
    96 IDENT=$(echo * | sed 's/${REPOS_NAME}-//')
    97 
    98 rm -f "${REPOS_NAME}-${IDENT}/.hg_archival.txt"
    99 rm -f "${REPOS_NAME}-${IDENT}/.hgtags"
   100 rm -f "${REPOS_NAME}-${IDENT}/.hgignore"
   101 rm -f "${REPOS_NAME}-${IDENT}/README_REPOSITORY"
   102 
   103 
   104 # dist name
   105 
   106 DATE=$(env LC_ALL=C date "+%d-%b-%Y")
   107 DISTDATE=$(env LC_ALL=C date "+%B %Y")
   108 
   109 if [ -z "$RELEASE" ]; then
   110   DISTNAME="Isabelle_$DATE"
   111   DISTVERSION="Isabelle repository snapshot $IDENT ($DATE)"
   112 else
   113   DISTNAME="$RELEASE"
   114   DISTVERSION="$DISTNAME: $DISTDATE"
   115 fi
   116 
   117 DISTBASE="$DISTPREFIX/dist-$DISTNAME"
   118 mkdir -p "$DISTBASE" || { purge_tmp; fail "Unable to create distribution base dir $DISTBASE!"; }
   119 [ -e "$DISTBASE/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/$DISTNAME already exists!"; }
   120 
   121 cd "$DISTBASE"
   122 mv "$DISTPREFIX/$TMP/${REPOS_NAME}-${IDENT}" "$DISTNAME"
   123 purge_tmp
   124 
   125 cd "$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME"
   126 
   127 
   128 # prepare dist for release
   129 
   130 echo "###"
   131 echo "### Preparing distribution $DISTNAME"
   132 echo "###"
   133 
   134 rm -f .hgignore
   135 find . "(" -name \*.thy -o -name \*.ML ")" -perm +111 -print | xargs chmod -f -x
   136 find . -print | xargs chmod -f u+rw
   137 
   138 ./Admin/build all || fail "Failed to build distribution"
   139 rm -rf Admin
   140 
   141 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')
   142 mv -f $MOVE doc
   143 rm doc/Isa-logics.eps
   144 rm doc/adaptation.dvi doc/adaptation.pdf doc/architecture.dvi doc/architecture.pdf
   145 rm -rf doc-src
   146 
   147 mkdir -p contrib
   148 
   149 cp doc/isabelle*.eps lib/logo
   150 
   151 rm Isabelle Isabelle.exe
   152 
   153 
   154 if [ -z "$RELEASE" ]; then
   155   {
   156     echo
   157     echo "IMPORTANT NOTE"
   158     echo "=============="
   159     echo
   160     echo "This is an unofficial snapshot of Isabelle, created by $LOGNAME $DATE."
   161     echo "See $REPOS/log/$IDENT for details."
   162     echo
   163   } >ANNOUNCE
   164 else
   165   perl -pi -e "s,val is_official = false,val is_official = true,g" src/Pure/ROOT.ML
   166 fi
   167 
   168 perl -pi -e "s,val changelog = \"\",val changelog = \"$REPOS/log/$IDENT\",g" src/Pure/ROOT.ML
   169 perl -pi -e "s,ISABELLE_IDENTIFIER=\"\",ISABELLE_IDENTIFIER=\"$DISTNAME\",g" lib/scripts/getsettings
   170 perl -pi -e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template
   171 perl -pi -e "s,unidentified repository version,$DISTVERSION,g" src/Pure/ROOT.ML lib/Tools/version
   172 perl -pi -e "s,some unidentified repository version of Isabelle,$DISTVERSION,g" README
   173 
   174 
   175 # create archives
   176 
   177 echo "###"
   178 echo "### Creating archives ..."
   179 echo "###"
   180 
   181 cd "$DISTBASE"
   182 
   183 echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST
   184 echo "$IDENT" >../ISABELLE_IDENT
   185 
   186 rm -f Isabelle
   187 ln -s "$DISTNAME" Isabelle
   188 
   189 chown -R "$LOGNAME" "$DISTNAME"
   190 chmod -R u+w "$DISTNAME"
   191 chmod -R g=o "$DISTNAME"
   192 chgrp -R isabelle "$DISTNAME" Isabelle
   193 
   194 echo "$DISTNAME.tar.gz"
   195 tar -czf "$DISTNAME.tar.gz" Isabelle "$DISTNAME"
   196 
   197 
   198 # cleanup dist
   199 
   200 mv "$DISTNAME" "${DISTNAME}-old"
   201 mkdir "$DISTNAME"
   202 
   203 mv "${DISTNAME}-old/README" "${DISTNAME}-old/INSTALL" "${DISTNAME}-old/NEWS" \
   204   "${DISTNAME}-old/ANNOUNCE" "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" \
   205   "$DISTNAME"
   206 mkdir "$DISTNAME/doc"
   207 mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc"
   208 
   209 chgrp -R isabelle "$DISTNAME"
   210 
   211 rm -rf "${DISTNAME}-old"
   212