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